axac2

Description: Derive ax-ac2 from ax-ac . (Contributed by NM, 19-Dec-2016) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	axac2	$⊢ \exists y \forall z \exists v \forall u ((y \in x \land (z \in y \to ((v \in x \land \neg y = v) \land z \in v))) \lor (\neg y \in x \land (z \in x \to ((v \in z \land v \in y) \land ((u \in z \land u \in y) \to u = v)))))$

Step	Hyp	Ref	Expression
1		dfac2a	$⊢ \forall x \exists y \forall z \in x (z \neq \emptyset \to \exists! v \in z \exists u \in y (z \in u \land v \in u)) \to CHOICE$
2		ac3	$⊢ \exists y \forall z \in x (z \neq \emptyset \to \exists! v \in z \exists u \in y (z \in u \land v \in u))$
3	1 2	mpg	$⊢ CHOICE$
4		dfackm	$⊢ CHOICE \leftrightarrow \forall x \exists y \forall z \exists v \forall u ((y \in x \land (z \in y \to ((v \in x \land \neg y = v) \land z \in v))) \lor (\neg y \in x \land (z \in x \to ((v \in z \land v \in y) \land ((u \in z \land u \in y) \to u = v)))))$
5	3 4	mpbi	$⊢ \forall x \exists y \forall z \exists v \forall u ((y \in x \land (z \in y \to ((v \in x \land \neg y = v) \land z \in v))) \lor (\neg y \in x \land (z \in x \to ((v \in z \land v \in y) \land ((u \in z \land u \in y) \to u = v)))))$
6	5	spi	$⊢ \exists y \forall z \exists v \forall u ((y \in x \land (z \in y \to ((v \in x \land \neg y = v) \land z \in v))) \lor (\neg y \in x \land (z \in x \to ((v \in z \land v \in y) \land ((u \in z \land u \in y) \to u = v)))))$

Metamath Proof Explorer