zfac

Description: Axiom of Choice expressed with the fewest number of different variables. The penultimate step shows the logical equivalence to ax-ac . (New usage is discouraged.) (Contributed by NM, 14-Aug-2003)

		Ref	Expression
	Assertion	zfac	$⊢ \exists x \forall y \forall z ((y \in z \land z \in w) \to \exists w \forall y (\exists w ((y \in z \land z \in w) \land (y \in w \land w \in x)) \leftrightarrow y = w))$

Proof

Step	Hyp	Ref	Expression
1		ax-ac	$⊢ \exists x \forall y \forall z ((y \in z \land z \in w) \to \exists v \forall u (\exists t ((u \in z \land z \in t) \land (u \in t \land t \in x)) \leftrightarrow u = v))$
2		equequ2	$⊢ v = w \to (u = v \leftrightarrow u = w)$
3	2	bibi2d	$⊢ v = w \to ((\exists t ((u \in z \land z \in t) \land (u \in t \land t \in x)) \leftrightarrow u = v) \leftrightarrow (\exists t ((u \in z \land z \in t) \land (u \in t \land t \in x)) \leftrightarrow u = w))$
4		elequ2	$⊢ t = w \to (z \in t \leftrightarrow z \in w)$
5	4	anbi2d	$⊢ t = w \to ((u \in z \land z \in t) \leftrightarrow (u \in z \land z \in w))$
6		elequ2	$⊢ t = w \to (u \in t \leftrightarrow u \in w)$
7		elequ1	$⊢ t = w \to (t \in x \leftrightarrow w \in x)$
8	6 7	anbi12d	$⊢ t = w \to ((u \in t \land t \in x) \leftrightarrow (u \in w \land w \in x))$
9	5 8	anbi12d	$⊢ t = w \to (((u \in z \land z \in t) \land (u \in t \land t \in x)) \leftrightarrow ((u \in z \land z \in w) \land (u \in w \land w \in x)))$
10	9	cbvexvw	$⊢ \exists t ((u \in z \land z \in t) \land (u \in t \land t \in x)) \leftrightarrow \exists w ((u \in z \land z \in w) \land (u \in w \land w \in x))$
11	10	bibi1i	$⊢ (\exists t ((u \in z \land z \in t) \land (u \in t \land t \in x)) \leftrightarrow u = w) \leftrightarrow (\exists w ((u \in z \land z \in w) \land (u \in w \land w \in x)) \leftrightarrow u = w)$
12	3 11	bitrdi	$⊢ v = w \to ((\exists t ((u \in z \land z \in t) \land (u \in t \land t \in x)) \leftrightarrow u = v) \leftrightarrow (\exists w ((u \in z \land z \in w) \land (u \in w \land w \in x)) \leftrightarrow u = w))$
13	12	albidv	$⊢ v = w \to (\forall u (\exists t ((u \in z \land z \in t) \land (u \in t \land t \in x)) \leftrightarrow u = v) \leftrightarrow \forall u (\exists w ((u \in z \land z \in w) \land (u \in w \land w \in x)) \leftrightarrow u = w))$
14		elequ1	$⊢ u = y \to (u \in z \leftrightarrow y \in z)$
15	14	anbi1d	$⊢ u = y \to ((u \in z \land z \in w) \leftrightarrow (y \in z \land z \in w))$
16		elequ1	$⊢ u = y \to (u \in w \leftrightarrow y \in w)$
17	16	anbi1d	$⊢ u = y \to ((u \in w \land w \in x) \leftrightarrow (y \in w \land w \in x))$
18	15 17	anbi12d	$⊢ u = y \to (((u \in z \land z \in w) \land (u \in w \land w \in x)) \leftrightarrow ((y \in z \land z \in w) \land (y \in w \land w \in x)))$
19	18	exbidv	$⊢ u = y \to (\exists w ((u \in z \land z \in w) \land (u \in w \land w \in x)) \leftrightarrow \exists w ((y \in z \land z \in w) \land (y \in w \land w \in x)))$
20		equequ1	$⊢ u = y \to (u = w \leftrightarrow y = w)$
21	19 20	bibi12d	$⊢ u = y \to ((\exists w ((u \in z \land z \in w) \land (u \in w \land w \in x)) \leftrightarrow u = w) \leftrightarrow (\exists w ((y \in z \land z \in w) \land (y \in w \land w \in x)) \leftrightarrow y = w))$
22	21	cbvalvw	$⊢ \forall u (\exists w ((u \in z \land z \in w) \land (u \in w \land w \in x)) \leftrightarrow u = w) \leftrightarrow \forall y (\exists w ((y \in z \land z \in w) \land (y \in w \land w \in x)) \leftrightarrow y = w)$
23	13 22	bitrdi	$⊢ v = w \to (\forall u (\exists t ((u \in z \land z \in t) \land (u \in t \land t \in x)) \leftrightarrow u = v) \leftrightarrow \forall y (\exists w ((y \in z \land z \in w) \land (y \in w \land w \in x)) \leftrightarrow y = w))$
24	23	cbvexvw	$⊢ \exists v \forall u (\exists t ((u \in z \land z \in t) \land (u \in t \land t \in x)) \leftrightarrow u = v) \leftrightarrow \exists w \forall y (\exists w ((y \in z \land z \in w) \land (y \in w \land w \in x)) \leftrightarrow y = w)$
25	24	imbi2i	$⊢ ((y \in z \land z \in w) \to \exists v \forall u (\exists t ((u \in z \land z \in t) \land (u \in t \land t \in x)) \leftrightarrow u = v)) \leftrightarrow ((y \in z \land z \in w) \to \exists w \forall y (\exists w ((y \in z \land z \in w) \land (y \in w \land w \in x)) \leftrightarrow y = w))$
26	25	2albii	$⊢ \forall y \forall z ((y \in z \land z \in w) \to \exists v \forall u (\exists t ((u \in z \land z \in t) \land (u \in t \land t \in x)) \leftrightarrow u = v)) \leftrightarrow \forall y \forall z ((y \in z \land z \in w) \to \exists w \forall y (\exists w ((y \in z \land z \in w) \land (y \in w \land w \in x)) \leftrightarrow y = w))$
27	26	exbii	$⊢ \exists x \forall y \forall z ((y \in z \land z \in w) \to \exists v \forall u (\exists t ((u \in z \land z \in t) \land (u \in t \land t \in x)) \leftrightarrow u = v)) \leftrightarrow \exists x \forall y \forall z ((y \in z \land z \in w) \to \exists w \forall y (\exists w ((y \in z \land z \in w) \land (y \in w \land w \in x)) \leftrightarrow y = w))$
28	1 27	mpbi	$⊢ \exists x \forall y \forall z ((y \in z \land z \in w) \to \exists w \forall y (\exists w ((y \in z \land z \in w) \land (y \in w \land w \in x)) \leftrightarrow y = w))$

Metamath Proof Explorer

Theorem zfac

Proof