Theorem uncpl1 ≪ | index | src | ≫

theorem uncpl1 (A: set): $ Compl A u. A == _V $;

Step	Hyp	Ref	Expression
1		eqstr	Compl A u. A == A u. Compl A -> A u. Compl A == _V -> Compl A u. A == _V
2		uncom	Compl A u. A == A u. Compl A
3	1, 2	ax_mp	A u. Compl A == _V -> Compl A u. A == _V
4		uncpl2	A u. Compl A == _V
5	3, 4	ax_mp	Compl A u. A == _V

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8)