HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
GIF version
Theorem axacnd 3758
Description: A version of the Axiom of Choice with no distinct variable conditions.
Assertion
Ref Expression
axacnd ⊢ ∃x∀y∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w))
Proof of Theorem axacnd
StepHypRef Expression
1 axacndlem5 3757 . . . 4 ⊢ ∃x∀y∀v(∀x(y ∈ v ∧ v ∈ w) → ∃w∀y(∃w((y ∈ v ∧ v ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w))
2 eq6 826 . . . . . 6 ⊢ (¬ ∀z z = x → ∀x ¬ ∀z z = x)
3 eq6 826 . . . . . . 7 ⊢ (¬ ∀z z = y → ∀x ¬ ∀z z = y)
4 eq6 826 . . . . . . 7 ⊢ (¬ ∀z z = w → ∀x ¬ ∀z z = w)
53, 4hban 704 . . . . . 6 ⊢ ((¬ ∀z z = y ∧ ¬ ∀z z = w) → ∀x(¬ ∀z z = y ∧ ¬ ∀z z = w))
62, 5hban 704 . . . . 5 ⊢ ((¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)) → ∀x(¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)))
7 eq6 826 . . . . . . 7 ⊢ (¬ ∀z z = x → ∀y ¬ ∀z z = x)
8 eq6 826 . . . . . . . 8 ⊢ (¬ ∀z z = y → ∀y ¬ ∀z z = y)
9 eq6 826 . . . . . . . 8 ⊢ (¬ ∀z z = w → ∀y ¬ ∀z z = w)
108, 9hban 704 . . . . . . 7 ⊢ ((¬ ∀z z = y ∧ ¬ ∀z z = w) → ∀y(¬ ∀z z = y ∧ ¬ ∀z z = w))
117, 10hban 704 . . . . . 6 ⊢ ((¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)) → ∀y(¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)))
12 eq6 826 . . . . . . . 8 ⊢ (¬ ∀z z = x → ∀z ¬ ∀z z = x)
13 eq6 826 . . . . . . . . 9 ⊢ (¬ ∀z z = y → ∀z ¬ ∀z z = y)
14 eq6 826 . . . . . . . . 9 ⊢ (¬ ∀z z = w → ∀z ¬ ∀z z = w)
1513, 14hban 704 . . . . . . . 8 ⊢ ((¬ ∀z z = y ∧ ¬ ∀z z = w) → ∀z(¬ ∀z z = y ∧ ¬ ∀z z = w))
1612, 15hban 704 . . . . . . 7 ⊢ ((¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)) → ∀z(¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)))
17 ddeel1 1003 . . . . . . . . . . 11 ⊢ (¬ ∀z z = y → (y ∈ v → ∀z y ∈ v))
1817ad2antrl 322 . . . . . . . . . 10 ⊢ ((¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)) → (y ∈ v → ∀z y ∈ v))
19 ddeel2 1004 . . . . . . . . . . 11 ⊢ (¬ ∀z z = w → (v ∈ w → ∀z v ∈ w))
2019ad2antrr 323 . . . . . . . . . 10 ⊢ ((¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)) → (v ∈ w → ∀z v ∈ w))
2118, 20hband 788 . . . . . . . . 9 ⊢ ((¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)) → ((y ∈ v ∧ v ∈ w) → ∀z(y ∈ v ∧ v ∈ w)))
226, 21hbald 790 . . . . . . . 8 ⊢ ((¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)) → (∀x(y ∈ v ∧ v ∈ w) → ∀z∀x(y ∈ v ∧ v ∈ w)))
23 eq6 826 . . . . . . . . . 10 ⊢ (¬ ∀z z = x → ∀w ¬ ∀z z = x)
24 eq6 826 . . . . . . . . . . 11 ⊢ (¬ ∀z z = y → ∀w ¬ ∀z z = y)
25 eq6 826 . . . . . . . . . . 11 ⊢ (¬ ∀z z = w → ∀w ¬ ∀z z = w)
2624, 25hban 704 . . . . . . . . . 10 ⊢ ((¬ ∀z z = y ∧ ¬ ∀z z = w) → ∀w(¬ ∀z z = y ∧ ¬ ∀z z = w))
2723, 26hban 704 . . . . . . . . 9 ⊢ ((¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)) → ∀w(¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)))
28 ax15 1006 . . . . . . . . . . . . . . . 16 ⊢ (¬ ∀z z = y → (¬ ∀z z = w → (y ∈ w → ∀z y ∈ w)))
2928imp 277 . . . . . . . . . . . . . . 15 ⊢ ((¬ ∀z z = y ∧ ¬ ∀z z = w) → (y ∈ w → ∀z y ∈ w))
3029adantl 305 . . . . . . . . . . . . . 14 ⊢ ((¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)) → (y ∈ w → ∀z y ∈ w))
31 ax15 1006 . . . . . . . . . . . . . . . . 17 ⊢ (¬ ∀z z = w → (¬ ∀z z = x → (w ∈ x → ∀z w ∈ x)))
3231com12 13 . . . . . . . . . . . . . . . 16 ⊢ (¬ ∀z z = x → (¬ ∀z z = w → (w ∈ x → ∀z w ∈ x)))
3332imp 277 . . . . . . . . . . . . . . 15 ⊢ ((¬ ∀z z = x ∧ ¬ ∀z z = w) → (w ∈ x → ∀z w ∈ x))
3433adantrl 311 . . . . . . . . . . . . . 14 ⊢ ((¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)) → (w ∈ x → ∀z w ∈ x))
3530, 34hband 788 . . . . . . . . . . . . 13 ⊢ ((¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)) → ((y ∈ w ∧ w ∈ x) → ∀z(y ∈ w ∧ w ∈ x)))
3621, 35hband 788 . . . . . . . . . . . 12 ⊢ ((¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)) → (((y ∈ v ∧ v ∈ w) ∧ (y ∈ w ∧ w ∈ x)) → ∀z((y ∈ v ∧ v ∈ w) ∧ (y ∈ w ∧ w ∈ x))))
3727, 36hbexd 791 . . . . . . . . . . 11 ⊢ ((¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)) → (∃w((y ∈ v ∧ v ∈ w) ∧ (y ∈ w ∧ w ∈ x)) → ∀z∃w((y ∈ v ∧ v ∈ w) ∧ (y ∈ w ∧ w ∈ x))))
38 ax-12 802 . . . . . . . . . . . . 13 ⊢ (¬ ∀z z = y → (¬ ∀z z = w → (y = w → ∀z y = w)))
3938imp 277 . . . . . . . . . . . 12 ⊢ ((¬ ∀z z = y ∧ ¬ ∀z z = w) → (y = w → ∀z y = w))
4039adantl 305 . . . . . . . . . . 11 ⊢ ((¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)) → (y = w → ∀z y = w))
4116, 37, 40hbbid 789 . . . . . . . . . 10 ⊢ ((¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)) → ((∃w((y ∈ v ∧ v ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w) → ∀z(∃w((y ∈ v ∧ v ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
4211, 41hbald 790 . . . . . . . . 9 ⊢ ((¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)) → (∀y(∃w((y ∈ v ∧ v ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w) → ∀z∀y(∃w((y ∈ v ∧ v ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
4327, 42hbexd 791 . . . . . . . 8 ⊢ ((¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)) → (∃w∀y(∃w((y ∈ v ∧ v ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w) → ∀z∃w∀y(∃w((y ∈ v ∧ v ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
4416, 22, 43hbimd 787 . . . . . . 7 ⊢ ((¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)) → ((∀x(y ∈ v ∧ v ∈ w) → ∃w∀y(∃w((y ∈ v ∧ v ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)) → ∀z(∀x(y ∈ v ∧ v ∈ w) → ∃w∀y(∃w((y ∈ v ∧ v ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w))))
45 nd5 3736 . . . . . . . . . . . 12 ⊢ (¬ ∀z z = x → (v = z → ∀x v = z))
4645imdistani 340 . . . . . . . . . . 11 ⊢ ((¬ ∀z z = x ∧ v = z) → (¬ ∀z z = x ∧ ∀x v = z))
47 hba1 698 . . . . . . . . . . . . 13 ⊢ (∀x v = z → ∀x∀x v = z)
48 a14b 820 . . . . . . . . . . . . . . 15 ⊢ (v = z → (y ∈ v ↔ y ∈ z))
49 a13b 819 . . . . . . . . . . . . . . 15 ⊢ (v = z → (v ∈ w ↔ z ∈ w))
5048, 49anbi12d 476 . . . . . . . . . . . . . 14 ⊢ (v = z → ((y ∈ v ∧ v ∈ w) ↔ (y ∈ z ∧ z ∈ w)))
5150a4s 682 . . . . . . . . . . . . 13 ⊢ (∀x v = z → ((y ∈ v ∧ v ∈ w) ↔ (y ∈ z ∧ z ∈ w)))
5247, 51biald 782 . . . . . . . . . . . 12 ⊢ (∀x v = z → (∀x(y ∈ v ∧ v ∈ w) ↔ ∀x(y ∈ z ∧ z ∈ w)))
5352adantl 305 . . . . . . . . . . 11 ⊢ ((¬ ∀z z = x ∧ ∀x v = z) → (∀x(y ∈ v ∧ v ∈ w) ↔ ∀x(y ∈ z ∧ z ∈ w)))
5446, 53syl 12 . . . . . . . . . 10 ⊢ ((¬ ∀z z = x ∧ v = z) → (∀x(y ∈ v ∧ v ∈ w) ↔ ∀x(y ∈ z ∧ z ∈ w)))
5554adantlr 310 . . . . . . . . 9 ⊢ (((¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)) ∧ v = z) → (∀x(y ∈ v ∧ v ∈ w) ↔ ∀x(y ∈ z ∧ z ∈ w)))
56 nd5 3736 . . . . . . . . . . . . 13 ⊢ (¬ ∀z z = y → (v = z → ∀y v = z))
57 nd5 3736 . . . . . . . . . . . . . 14 ⊢ (¬ ∀z z = w → (v = z → ∀w v = z))
589, 57hbald 790 . . . . . . . . . . . . 13 ⊢ (¬ ∀z z = w → (∀y v = z → ∀w∀y v = z))
5956, 58sylan9 359 . . . . . . . . . . . 12 ⊢ ((¬ ∀z z = y ∧ ¬ ∀z z = w) → (v = z → ∀w∀y v = z))
6059imdistani 340 . . . . . . . . . . 11 ⊢ (((¬ ∀z z = y ∧ ¬ ∀z z = w) ∧ v = z) → ((¬ ∀z z = y ∧ ¬ ∀z z = w) ∧ ∀w∀y v = z))
61 hba1 698 . . . . . . . . . . . . 13 ⊢ (∀w∀y v = z → ∀w∀w∀y v = z)
62 hba1 698 . . . . . . . . . . . . . . 15 ⊢ (∀y v = z → ∀y∀y v = z)
6362hbal 700 . . . . . . . . . . . . . 14 ⊢ (∀w∀y v = z → ∀y∀w∀y v = z)
6450a4s 682 . . . . . . . . . . . . . . . . . 18 ⊢ (∀y v = z → ((y ∈ v ∧ v ∈ w) ↔ (y ∈ z ∧ z ∈ w)))
6564a4s 682 . . . . . . . . . . . . . . . . 17 ⊢ (∀w∀y v = z → ((y ∈ v ∧ v ∈ w) ↔ (y ∈ z ∧ z ∈ w)))
6665anbi1d 469 . . . . . . . . . . . . . . . 16 ⊢ (∀w∀y v = z → (((y ∈ v ∧ v ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ ((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x))))
6761, 66biexd 783 . . . . . . . . . . . . . . 15 ⊢ (∀w∀y v = z → (∃w((y ∈ v ∧ v ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ ∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x))))
6867bibi1d 471 . . . . . . . . . . . . . 14 ⊢ (∀w∀y v = z → ((∃w((y ∈ v ∧ v ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w) ↔ (∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
6963, 68biald 782 . . . . . . . . . . . . 13 ⊢ (∀w∀y v = z → (∀y(∃w((y ∈ v ∧ v ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w) ↔ ∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
7061, 69biexd 783 . . . . . . . . . . . 12 ⊢ (∀w∀y v = z → (∃w∀y(∃w((y ∈ v ∧ v ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w) ↔ ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
7170adantl 305 . . . . . . . . . . 11 ⊢ (((¬ ∀z z = y ∧ ¬ ∀z z = w) ∧ ∀w∀y v = z) → (∃w∀y(∃w((y ∈ v ∧ v ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w) ↔ ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
7260, 71syl 12 . . . . . . . . . 10 ⊢ (((¬ ∀z z = y ∧ ¬ ∀z z = w) ∧ v = z) → (∃w∀y(∃w((y ∈ v ∧ v ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w) ↔ ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
7372adantll 309 . . . . . . . . 9 ⊢ (((¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)) ∧ v = z) → (∃w∀y(∃w((y ∈ v ∧ v ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w) ↔ ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
7455, 73imbi12d 474 . . . . . . . 8 ⊢ (((¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)) ∧ v = z) → ((∀x(y ∈ v ∧ v ∈ w) → ∃w∀y(∃w((y ∈ v ∧ v ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)) ↔ (∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w))))
7574exp 291 . . . . . . 7 ⊢ ((¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)) → (v = z → ((∀x(y ∈ v ∧ v ∈ w) → ∃w∀y(∃w((y ∈ v ∧ v ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)) ↔ (∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))))
7616, 44, 75cbvald 977 . . . . . 6 ⊢ ((¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)) → (∀v(∀x(y ∈ v ∧ v ∈ w) → ∃w∀y(∃w((y ∈ v ∧ v ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)) ↔ ∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w))))
7711, 76biald 782 . . . . 5 ⊢ ((¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)) → (∀y∀v(∀x(y ∈ v ∧ v ∈ w) → ∃w∀y(∃w((y ∈ v ∧ v ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)) ↔ ∀y∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w))))
786, 77biexd 783 . . . 4 ⊢ ((¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)) → (∃x∀y∀v(∀x(y ∈ v ∧ v ∈ w) → ∃w∀y(∃w((y ∈ v ∧ v ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)) ↔ ∃x∀y∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w))))
791, 78mpbii 168 . . 3 ⊢ ((¬ ∀z z = x ∧ (¬ ∀z z = y ∧ ¬ ∀z z = w)) → ∃x∀y∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
8079exp32 294 . 2 ⊢ (¬ ∀z z = x → (¬ ∀z z = y → (¬ ∀z z = w → ∃x∀y∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))))
81 axacndlem2 3754 . . 3 ⊢ (∀x x = z → ∃x∀y∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
8281eq4s 822 . 2 ⊢ (∀z z = x → ∃x∀y∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
83 axacndlem3 3755 . . 3 ⊢ (∀y y = z → ∃x∀y∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
8483eq4s 822 . 2 ⊢ (∀z z = y → ∃x∀y∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
85 eq5 824 . . . 4 ⊢ (∀z z = w → ∀y∀z z = w)
86 nd3 3734 . . . . . . 7 ⊢ (∀z z = w → ¬ ∀x z ∈ w)
8786pm2.21d 74 . . . . . 6 ⊢ (∀z z = w → (∀x z ∈ w → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
88 pm3.27 260 . . . . . . 7 ⊢ ((y ∈ z ∧ z ∈ w) → z ∈ w)
898819.20i 691 . . . . . 6 ⊢ (∀x(y ∈ z ∧ z ∈ w) → ∀x z ∈ w)
9087, 89syl5 22 . . . . 5 ⊢ (∀z z = w → (∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
9190a5i 687 . . . 4 ⊢ (∀z z = w → ∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
9285, 9119.21ai 740 . . 3 ⊢ (∀z z = w → ∀y∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
93 19.8a 712 . . 3 ⊢ (∀y∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)) → ∃x∀y∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
9492, 93syl 12 . 2 ⊢ (∀z z = w → ∃x∀y∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
9580, 82, 84, 94pm2.61iii 114 1 ⊢ ∃x∀y∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w))
Colors of variables: wff set class
Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672  ∃wex 678   = weq 797   ∈ wel 803
This theorem is referenced by:  zfcndac 3765
This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-pow 1077  ax-reg 1078  ax-ac 1080
This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-br 2063  df-opab 2098  df-eprel 2122  df-fr 2169
metamath.org