Metamath Proof Explorer

Theorem zfcndac

Description: Axiom of Choice ax-ac , reproved from conditionless ZFC axioms. (Contributed by NM, 15-Aug-2003) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion zfcndac ⊢ ∃ y ∀ z ∀ w z ∈ w ∧ w ∈ x → ∃ v ∀ u ∃ t u ∈ w ∧ w ∈ t ∧ u ∈ t ∧ t ∈ y ↔ u = v

Proof

Step Hyp Ref Expression
1 axacnd ⊢ ∃ y ∀ z ∀ w ∀ y z ∈ w ∧ w ∈ x → ∃ x ∀ z ∃ x z ∈ w ∧ w ∈ x ∧ z ∈ x ∧ x ∈ y ↔ z = x
2 19.3v ⊢ ∀ y z ∈ w ∧ w ∈ x ↔ z ∈ w ∧ w ∈ x
3 2 imbi1i ⊢ ∀ y z ∈ w ∧ w ∈ x → ∃ x ∀ z ∃ x z ∈ w ∧ w ∈ x ∧ z ∈ x ∧ x ∈ y ↔ z = x ↔ z ∈ w ∧ w ∈ x → ∃ x ∀ z ∃ x z ∈ w ∧ w ∈ x ∧ z ∈ x ∧ x ∈ y ↔ z = x
4 3 2albii ⊢ ∀ z ∀ w ∀ y z ∈ w ∧ w ∈ x → ∃ x ∀ z ∃ x z ∈ w ∧ w ∈ x ∧ z ∈ x ∧ x ∈ y ↔ z = x ↔ ∀ z ∀ w z ∈ w ∧ w ∈ x → ∃ x ∀ z ∃ x z ∈ w ∧ w ∈ x ∧ z ∈ x ∧ x ∈ y ↔ z = x
5 4 exbii ⊢ ∃ y ∀ z ∀ w ∀ y z ∈ w ∧ w ∈ x → ∃ x ∀ z ∃ x z ∈ w ∧ w ∈ x ∧ z ∈ x ∧ x ∈ y ↔ z = x ↔ ∃ y ∀ z ∀ w z ∈ w ∧ w ∈ x → ∃ x ∀ z ∃ x z ∈ w ∧ w ∈ x ∧ z ∈ x ∧ x ∈ y ↔ z = x
6 1 5 mpbi ⊢ ∃ y ∀ z ∀ w z ∈ w ∧ w ∈ x → ∃ x ∀ z ∃ x z ∈ w ∧ w ∈ x ∧ z ∈ x ∧ x ∈ y ↔ z = x
7 equequ2 ⊢ v = x → u = v ↔ u = x
8 7 bibi2d ⊢ v = x → ∃ t u ∈ w ∧ w ∈ t ∧ u ∈ t ∧ t ∈ y ↔ u = v ↔ ∃ t u ∈ w ∧ w ∈ t ∧ u ∈ t ∧ t ∈ y ↔ u = x
9 elequ2 ⊢ t = x → w ∈ t ↔ w ∈ x
10 9 anbi2d ⊢ t = x → u ∈ w ∧ w ∈ t ↔ u ∈ w ∧ w ∈ x
11 elequ2 ⊢ t = x → u ∈ t ↔ u ∈ x
12 elequ1 ⊢ t = x → t ∈ y ↔ x ∈ y
13 11 12 anbi12d ⊢ t = x → u ∈ t ∧ t ∈ y ↔ u ∈ x ∧ x ∈ y
14 10 13 anbi12d ⊢ t = x → u ∈ w ∧ w ∈ t ∧ u ∈ t ∧ t ∈ y ↔ u ∈ w ∧ w ∈ x ∧ u ∈ x ∧ x ∈ y
15 14 cbvexvw ⊢ ∃ t u ∈ w ∧ w ∈ t ∧ u ∈ t ∧ t ∈ y ↔ ∃ x u ∈ w ∧ w ∈ x ∧ u ∈ x ∧ x ∈ y
16 15 bibi1i ⊢ ∃ t u ∈ w ∧ w ∈ t ∧ u ∈ t ∧ t ∈ y ↔ u = x ↔ ∃ x u ∈ w ∧ w ∈ x ∧ u ∈ x ∧ x ∈ y ↔ u = x
17 8 16 bitrdi ⊢ v = x → ∃ t u ∈ w ∧ w ∈ t ∧ u ∈ t ∧ t ∈ y ↔ u = v ↔ ∃ x u ∈ w ∧ w ∈ x ∧ u ∈ x ∧ x ∈ y ↔ u = x
18 17 albidv ⊢ v = x → ∀ u ∃ t u ∈ w ∧ w ∈ t ∧ u ∈ t ∧ t ∈ y ↔ u = v ↔ ∀ u ∃ x u ∈ w ∧ w ∈ x ∧ u ∈ x ∧ x ∈ y ↔ u = x
19 elequ1 ⊢ u = z → u ∈ w ↔ z ∈ w
20 19 anbi1d ⊢ u = z → u ∈ w ∧ w ∈ x ↔ z ∈ w ∧ w ∈ x
21 elequ1 ⊢ u = z → u ∈ x ↔ z ∈ x
22 21 anbi1d ⊢ u = z → u ∈ x ∧ x ∈ y ↔ z ∈ x ∧ x ∈ y
23 20 22 anbi12d ⊢ u = z → u ∈ w ∧ w ∈ x ∧ u ∈ x ∧ x ∈ y ↔ z ∈ w ∧ w ∈ x ∧ z ∈ x ∧ x ∈ y
24 23 exbidv ⊢ u = z → ∃ x u ∈ w ∧ w ∈ x ∧ u ∈ x ∧ x ∈ y ↔ ∃ x z ∈ w ∧ w ∈ x ∧ z ∈ x ∧ x ∈ y
25 equequ1 ⊢ u = z → u = x ↔ z = x
26 24 25 bibi12d ⊢ u = z → ∃ x u ∈ w ∧ w ∈ x ∧ u ∈ x ∧ x ∈ y ↔ u = x ↔ ∃ x z ∈ w ∧ w ∈ x ∧ z ∈ x ∧ x ∈ y ↔ z = x
27 26 cbvalvw ⊢ ∀ u ∃ x u ∈ w ∧ w ∈ x ∧ u ∈ x ∧ x ∈ y ↔ u = x ↔ ∀ z ∃ x z ∈ w ∧ w ∈ x ∧ z ∈ x ∧ x ∈ y ↔ z = x
28 18 27 bitrdi ⊢ v = x → ∀ u ∃ t u ∈ w ∧ w ∈ t ∧ u ∈ t ∧ t ∈ y ↔ u = v ↔ ∀ z ∃ x z ∈ w ∧ w ∈ x ∧ z ∈ x ∧ x ∈ y ↔ z = x
29 28 cbvexvw ⊢ ∃ v ∀ u ∃ t u ∈ w ∧ w ∈ t ∧ u ∈ t ∧ t ∈ y ↔ u = v ↔ ∃ x ∀ z ∃ x z ∈ w ∧ w ∈ x ∧ z ∈ x ∧ x ∈ y ↔ z = x
30 29 imbi2i ⊢ z ∈ w ∧ w ∈ x → ∃ v ∀ u ∃ t u ∈ w ∧ w ∈ t ∧ u ∈ t ∧ t ∈ y ↔ u = v ↔ z ∈ w ∧ w ∈ x → ∃ x ∀ z ∃ x z ∈ w ∧ w ∈ x ∧ z ∈ x ∧ x ∈ y ↔ z = x
31 30 2albii ⊢ ∀ z ∀ w z ∈ w ∧ w ∈ x → ∃ v ∀ u ∃ t u ∈ w ∧ w ∈ t ∧ u ∈ t ∧ t ∈ y ↔ u = v ↔ ∀ z ∀ w z ∈ w ∧ w ∈ x → ∃ x ∀ z ∃ x z ∈ w ∧ w ∈ x ∧ z ∈ x ∧ x ∈ y ↔ z = x
32 31 exbii ⊢ ∃ y ∀ z ∀ w z ∈ w ∧ w ∈ x → ∃ v ∀ u ∃ t u ∈ w ∧ w ∈ t ∧ u ∈ t ∧ t ∈ y ↔ u = v ↔ ∃ y ∀ z ∀ w z ∈ w ∧ w ∈ x → ∃ x ∀ z ∃ x z ∈ w ∧ w ∈ x ∧ z ∈ x ∧ x ∈ y ↔ z = x
33 6 32 mpbir ⊢ ∃ y ∀ z ∀ w z ∈ w ∧ w ∈ x → ∃ v ∀ u ∃ t u ∈ w ∧ w ∈ t ∧ u ∈ t ∧ t ∈ y ↔ u = v