aceq2

Description: Equivalence of two versions of the Axiom of Choice. The proof uses neither AC nor the Axiom of Regularity. (Contributed by NM, 5-Apr-2004)

		Ref	Expression
	Assertion	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))$

Proof

Step	Hyp	Ref	Expression
1		df-ral	$⊢ \forall t \in z \exists! v \in z \exists u \in y (z \in u \land v \in u) \leftrightarrow \forall t (t \in z \to \exists! v \in z \exists u \in y (z \in u \land v \in u))$
2		19.23v	$⊢ \forall t (t \in z \to \exists! v \in z \exists u \in y (z \in u \land v \in u)) \leftrightarrow (\exists t t \in z \to \exists! v \in z \exists u \in y (z \in u \land v \in u))$
3	1 2	bitri	$⊢ \forall t \in z \exists! v \in z \exists u \in y (z \in u \land v \in u) \leftrightarrow (\exists t t \in z \to \exists! v \in z \exists u \in y (z \in u \land v \in u))$
4		biidd	$⊢ w = t \to (\exists! v \in z \exists u \in y (z \in u \land v \in u) \leftrightarrow \exists! v \in z \exists u \in y (z \in u \land v \in u))$
5	4	cbvralvw	$⊢ \forall w \in z \exists! v \in z \exists u \in y (z \in u \land v \in u) \leftrightarrow \forall t \in z \exists! v \in z \exists u \in y (z \in u \land v \in u)$
6		n0	$⊢ z \neq \emptyset \leftrightarrow \exists t t \in z$
7		elequ2	$⊢ v = u \to (z \in v \leftrightarrow z \in u)$
8		elequ2	$⊢ v = u \to (w \in v \leftrightarrow w \in u)$
9	7 8	anbi12d	$⊢ v = u \to ((z \in v \land w \in v) \leftrightarrow (z \in u \land w \in u))$
10	9	cbvrexvw	$⊢ \exists v \in y (z \in v \land w \in v) \leftrightarrow \exists u \in y (z \in u \land w \in u)$
11	10	reubii	$⊢ \exists! w \in z \exists v \in y (z \in v \land w \in v) \leftrightarrow \exists! w \in z \exists u \in y (z \in u \land w \in u)$
12		elequ1	$⊢ w = v \to (w \in u \leftrightarrow v \in u)$
13	12	anbi2d	$⊢ w = v \to ((z \in u \land w \in u) \leftrightarrow (z \in u \land v \in u))$
14	13	rexbidv	$⊢ w = v \to (\exists u \in y (z \in u \land w \in u) \leftrightarrow \exists u \in y (z \in u \land v \in u))$
15	14	cbvreuvw	$⊢ \exists! w \in z \exists u \in y (z \in u \land w \in u) \leftrightarrow \exists! v \in z \exists u \in y (z \in u \land v \in u)$
16	11 15	bitri	$⊢ \exists! w \in z \exists v \in y (z \in v \land w \in v) \leftrightarrow \exists! v \in z \exists u \in y (z \in u \land v \in u)$
17	6 16	imbi12i	$⊢ (z \neq \emptyset \to \exists! w \in z \exists v \in y (z \in v \land w \in v)) \leftrightarrow (\exists t t \in z \to \exists! v \in z \exists u \in y (z \in u \land v \in u))$
18	3 5 17	3bitr4i	$⊢ \forall w \in z \exists! v \in z \exists u \in y (z \in u \land v \in u) \leftrightarrow (z \neq \emptyset \to \exists! w \in z \exists v \in y (z \in v \land w \in v))$
19	18	ralbii	$⊢ \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 z \in x (z \neq \emptyset \to \exists! w \in z \exists v \in y (z \in v \land w \in v))$
20	19	exbii	$⊢ \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))$

Metamath Proof Explorer

Theorem aceq2

Proof