dfac7

Description: Equivalence of the Axiom of Choice (first form) of Enderton p. 49 and our Axiom of Choice (in the form of ac2 ). The proof does not depend on AC but does depend on the Axiom of Regularity. (Contributed by Mario Carneiro, 17-May-2015)

		Ref	Expression
	Assertion	dfac7	$⊢ CHOICE \leftrightarrow \forall x \exists y \forall z \in x \forall w \in z \exists! v \in z \exists u \in y (z \in u \land v \in u)$

Proof

Step	Hyp	Ref	Expression
1		dfac2	$⊢ CHOICE \leftrightarrow \forall x \exists y \forall z \in x (z \neq \emptyset \to \exists! w \in z \exists v \in y (z \in v \land w \in v))$
2		aceq2	$⊢ \exists y \forall z \in x \forall w \in z \exists! v \in z \exists u \in y (z \in u \land v \in u) \leftrightarrow \exists y \forall z \in x (z \neq \emptyset \to \exists! w \in z \exists v \in y (z \in v \land w \in v))$
3	2	albii	$⊢ \forall x \exists y \forall z \in x \forall w \in z \exists! v \in z \exists u \in y (z \in u \land v \in u) \leftrightarrow \forall x \exists y \forall z \in x (z \neq \emptyset \to \exists! w \in z \exists v \in y (z \in v \land w \in v))$
4	1 3	bitr4i	$⊢ CHOICE \leftrightarrow \forall x \exists y \forall z \in x \forall w \in z \exists! v \in z \exists u \in y (z \in u \land v \in u)$

Metamath Proof Explorer

Theorem dfac7

Proof