Metamath Proof Explorer

Theorem axunnd

Description: A version of the Axiom of Union with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 2-Jan-2002) (New usage is discouraged.)

Ref Expression
Assertion axunnd ⊢ ∃ x ∀ y ∃ x y ∈ x ∧ x ∈ z → y ∈ x

Proof

Step Hyp Ref Expression
1 axunndlem1 ⊢ ∃ w ∀ y ∃ w y ∈ w ∧ w ∈ z → y ∈ w
2 nfnae ⊢ Ⅎ x ¬ ∀ x x = y
3 nfnae ⊢ Ⅎ x ¬ ∀ x x = z
4 2 3 nfan ⊢ Ⅎ x ¬ ∀ x x = y ∧ ¬ ∀ x x = z
5 nfnae ⊢ Ⅎ y ¬ ∀ x x = y
6 nfnae ⊢ Ⅎ y ¬ ∀ x x = z
7 5 6 nfan ⊢ Ⅎ y ¬ ∀ x x = y ∧ ¬ ∀ x x = z
8 nfv ⊢ Ⅎ w ¬ ∀ x x = y ∧ ¬ ∀ x x = z
9 nfcvf ⊢ ¬ ∀ x x = y → Ⅎ _ x y
10 9 adantr ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ _ x y
11 nfcvd ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ _ x w
12 10 11 nfeld ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x y ∈ w
13 nfcvf ⊢ ¬ ∀ x x = z → Ⅎ _ x z
14 13 adantl ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ _ x z
15 11 14 nfeld ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x w ∈ z
16 12 15 nfand ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x y ∈ w ∧ w ∈ z
17 8 16 nfexd ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x ∃ w y ∈ w ∧ w ∈ z
18 17 12 nfimd ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x ∃ w y ∈ w ∧ w ∈ z → y ∈ w
19 7 18 nfald ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x ∀ y ∃ w y ∈ w ∧ w ∈ z → y ∈ w
20 nfcvd ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ _ y w
21 nfcvf2 ⊢ ¬ ∀ x x = y → Ⅎ _ y x
22 21 adantr ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ _ y x
23 20 22 nfeqd ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ y w = x
24 7 23 nfan1 ⊢ Ⅎ y ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x
25 elequ2 ⊢ w = x → y ∈ w ↔ y ∈ x
26 elequ1 ⊢ w = x → w ∈ z ↔ x ∈ z
27 25 26 anbi12d ⊢ w = x → y ∈ w ∧ w ∈ z ↔ y ∈ x ∧ x ∈ z
28 27 a1i ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → w = x → y ∈ w ∧ w ∈ z ↔ y ∈ x ∧ x ∈ z
29 4 16 28 cbvexd ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → ∃ w y ∈ w ∧ w ∈ z ↔ ∃ x y ∈ x ∧ x ∈ z
30 29 adantr ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → ∃ w y ∈ w ∧ w ∈ z ↔ ∃ x y ∈ x ∧ x ∈ z
31 25 adantl ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → y ∈ w ↔ y ∈ x
32 30 31 imbi12d ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → ∃ w y ∈ w ∧ w ∈ z → y ∈ w ↔ ∃ x y ∈ x ∧ x ∈ z → y ∈ x
33 24 32 albid ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → ∀ y ∃ w y ∈ w ∧ w ∈ z → y ∈ w ↔ ∀ y ∃ x y ∈ x ∧ x ∈ z → y ∈ x
34 33 ex ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → w = x → ∀ y ∃ w y ∈ w ∧ w ∈ z → y ∈ w ↔ ∀ y ∃ x y ∈ x ∧ x ∈ z → y ∈ x
35 4 19 34 cbvexd ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → ∃ w ∀ y ∃ w y ∈ w ∧ w ∈ z → y ∈ w ↔ ∃ x ∀ y ∃ x y ∈ x ∧ x ∈ z → y ∈ x
36 1 35 mpbii ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → ∃ x ∀ y ∃ x y ∈ x ∧ x ∈ z → y ∈ x
37 36 ex ⊢ ¬ ∀ x x = y → ¬ ∀ x x = z → ∃ x ∀ y ∃ x y ∈ x ∧ x ∈ z → y ∈ x
38 nfae ⊢ Ⅎ y ∀ x x = y
39 nfae ⊢ Ⅎ x ∀ x x = y
40 elirrv ⊢ ¬ y ∈ y
41 elequ2 ⊢ x = y → y ∈ x ↔ y ∈ y
42 40 41 mtbiri ⊢ x = y → ¬ y ∈ x
43 42 intnanrd ⊢ x = y → ¬ y ∈ x ∧ x ∈ z
44 43 sps ⊢ ∀ x x = y → ¬ y ∈ x ∧ x ∈ z
45 39 44 nexd ⊢ ∀ x x = y → ¬ ∃ x y ∈ x ∧ x ∈ z
46 45 pm2.21d ⊢ ∀ x x = y → ∃ x y ∈ x ∧ x ∈ z → y ∈ x
47 38 46 alrimi ⊢ ∀ x x = y → ∀ y ∃ x y ∈ x ∧ x ∈ z → y ∈ x
48 47 19.8ad ⊢ ∀ x x = y → ∃ x ∀ y ∃ x y ∈ x ∧ x ∈ z → y ∈ x
49 nfae ⊢ Ⅎ y ∀ x x = z
50 nfae ⊢ Ⅎ x ∀ x x = z
51 elirrv ⊢ ¬ z ∈ z
52 elequ1 ⊢ x = z → x ∈ z ↔ z ∈ z
53 51 52 mtbiri ⊢ x = z → ¬ x ∈ z
54 53 intnand ⊢ x = z → ¬ y ∈ x ∧ x ∈ z
55 54 sps ⊢ ∀ x x = z → ¬ y ∈ x ∧ x ∈ z
56 50 55 nexd ⊢ ∀ x x = z → ¬ ∃ x y ∈ x ∧ x ∈ z
57 56 pm2.21d ⊢ ∀ x x = z → ∃ x y ∈ x ∧ x ∈ z → y ∈ x
58 49 57 alrimi ⊢ ∀ x x = z → ∀ y ∃ x y ∈ x ∧ x ∈ z → y ∈ x
59 58 19.8ad ⊢ ∀ x x = z → ∃ x ∀ y ∃ x y ∈ x ∧ x ∈ z → y ∈ x
60 37 48 59 pm2.61ii ⊢ ∃ x ∀ y ∃ x y ∈ x ∧ x ∈ z → y ∈ x