ac2

Description: Axiom of Choice equivalent. By using restricted quantifiers, we can express the Axiom of Choice with a single explicit conjunction. (If you want to figure it out, the rewritten equivalent ac3 is easier to understand.) Note: aceq0 shows the logical equivalence to ax-ac . (New usage is discouraged.) (Contributed by NM, 18-Jul-1996)

		Ref	Expression
	Assertion	ac2	$⊢ \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		ax-ac	$⊢ \exists y \forall z \forall w ((z \in w \land w \in x) \to \exists v \forall u (\exists t ((u \in w \land w \in t) \land (u \in t \land t \in y)) \leftrightarrow u = v))$
2		aceq0	$⊢ \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 \forall w ((z \in w \land w \in x) \to \exists v \forall u (\exists t ((u \in w \land w \in t) \land (u \in t \land t \in y)) \leftrightarrow u = v))$
3	1 2	mpbir	$⊢ \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 ac2

Proof