Metamath Proof Explorer

Theorem axunndlem1

Description: Lemma for 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 axunndlem1 ⊢ ∃ x ∀ y ∃ x y ∈ x ∧ x ∈ z → y ∈ x

Proof

Step Hyp Ref Expression
1 en2lp ⊢ ¬ y ∈ x ∧ x ∈ y
2 elequ2 ⊢ y = z → x ∈ y ↔ x ∈ z
3 2 anbi2d ⊢ y = z → y ∈ x ∧ x ∈ y ↔ y ∈ x ∧ x ∈ z
4 1 3 mtbii ⊢ y = z → ¬ y ∈ x ∧ x ∈ z
5 4 sps ⊢ ∀ y y = z → ¬ y ∈ x ∧ x ∈ z
6 5 nexdv ⊢ ∀ y y = z → ¬ ∃ x y ∈ x ∧ x ∈ z
7 6 pm2.21d ⊢ ∀ y y = z → ∃ x y ∈ x ∧ x ∈ z → y ∈ x
8 7 axc4i ⊢ ∀ y y = z → ∀ y ∃ x y ∈ x ∧ x ∈ z → y ∈ x
9 8 19.8ad ⊢ ∀ y y = z → ∃ x ∀ y ∃ x y ∈ x ∧ x ∈ z → y ∈ x
10 zfun ⊢ ∃ x ∀ w ∃ x w ∈ x ∧ x ∈ z → w ∈ x
11 nfnae ⊢ Ⅎ y ¬ ∀ y y = z
12 nfnae ⊢ Ⅎ x ¬ ∀ y y = z
13 nfvd ⊢ ¬ ∀ y y = z → Ⅎ y w ∈ x
14 nfcvf ⊢ ¬ ∀ y y = z → Ⅎ _ y z
15 14 nfcrd ⊢ ¬ ∀ y y = z → Ⅎ y x ∈ z
16 13 15 nfand ⊢ ¬ ∀ y y = z → Ⅎ y w ∈ x ∧ x ∈ z
17 12 16 nfexd ⊢ ¬ ∀ y y = z → Ⅎ y ∃ x w ∈ x ∧ x ∈ z
18 17 13 nfimd ⊢ ¬ ∀ y y = z → Ⅎ y ∃ x w ∈ x ∧ x ∈ z → w ∈ x
19 elequ1 ⊢ w = y → w ∈ x ↔ y ∈ x
20 19 anbi1d ⊢ w = y → w ∈ x ∧ x ∈ z ↔ y ∈ x ∧ x ∈ z
21 20 exbidv ⊢ w = y → ∃ x w ∈ x ∧ x ∈ z ↔ ∃ x y ∈ x ∧ x ∈ z
22 21 19 imbi12d ⊢ w = y → ∃ x w ∈ x ∧ x ∈ z → w ∈ x ↔ ∃ x y ∈ x ∧ x ∈ z → y ∈ x
23 22 a1i ⊢ ¬ ∀ y y = z → w = y → ∃ x w ∈ x ∧ x ∈ z → w ∈ x ↔ ∃ x y ∈ x ∧ x ∈ z → y ∈ x
24 11 18 23 cbvald ⊢ ¬ ∀ y y = z → ∀ w ∃ x w ∈ x ∧ x ∈ z → w ∈ x ↔ ∀ y ∃ x y ∈ x ∧ x ∈ z → y ∈ x
25 24 exbidv ⊢ ¬ ∀ y y = z → ∃ x ∀ w ∃ x w ∈ x ∧ x ∈ z → w ∈ x ↔ ∃ x ∀ y ∃ x y ∈ x ∧ x ∈ z → y ∈ x
26 10 25 mpbii ⊢ ¬ ∀ y y = z → ∃ x ∀ y ∃ x y ∈ x ∧ x ∈ z → y ∈ x
27 9 26 pm2.61i ⊢ ∃ x ∀ y ∃ x y ∈ x ∧ x ∈ z → y ∈ x