Metamath Proof Explorer

Theorem axrepndlem2

Description: Lemma for the Axiom of Replacement with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 2-Jan-2002) (Proof shortened by Mario Carneiro, 6-Dec-2016) (New usage is discouraged.)

Ref Expression
Assertion axrepndlem2 $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → ∃ x ∃ y ∀ z φ → z = y → ∀ z z ∈ x ↔ ∃ x x ∈ y ∧ ∀ y φ$

Proof

Step Hyp Ref Expression
1 axrepndlem1 $⊢ ¬ ∀ y y = z → ∃ w ∃ y ∀ z w x φ → z = y → ∀ z z ∈ w ↔ ∃ w w ∈ y ∧ ∀ y w x φ$
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 nfnae $⊢ Ⅎ z ¬ ∀ x x = y$
9 nfnae $⊢ Ⅎ z ¬ ∀ x x = z$
10 8 9 nfan $⊢ Ⅎ z ¬ ∀ x x = y ∧ ¬ ∀ x x = z$
11 nfs1v $⊢ Ⅎ x w x φ$
12 11 a1i $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x w x φ$
13 nfcvf $⊢ ¬ ∀ x x = z → Ⅎ _ x z$
14 13 adantl $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ _ x z$
15 nfcvf $⊢ ¬ ∀ x x = y → Ⅎ _ x y$
16 15 adantr $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ _ x y$
17 14 16 nfeqd $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x z = y$
18 12 17 nfimd $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x w x φ → z = y$
19 10 18 nfald $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x ∀ z w x φ → z = y$
20 7 19 nfexd $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x ∃ y ∀ z w x φ → z = y$
21 nfcvd $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ _ x w$
22 14 21 nfeld $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x z ∈ w$
23 nfv $⊢ Ⅎ w ¬ ∀ x x = y ∧ ¬ ∀ x x = z$
24 21 16 nfeld $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x w ∈ y$
25 7 12 nfald $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x ∀ y w x φ$
26 24 25 nfand $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x w ∈ y ∧ ∀ y w x φ$
27 23 26 nfexd $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x ∃ w w ∈ y ∧ ∀ y w x φ$
28 22 27 nfbid $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x z ∈ w ↔ ∃ w w ∈ y ∧ ∀ y w x φ$
29 10 28 nfald $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x ∀ z z ∈ w ↔ ∃ w w ∈ y ∧ ∀ y w x φ$
30 20 29 nfimd $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x ∃ y ∀ z w x φ → z = y → ∀ z z ∈ w ↔ ∃ w w ∈ y ∧ ∀ y w x φ$
31 nfcvd $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ _ y w$
32 nfcvf2 $⊢ ¬ ∀ x x = y → Ⅎ _ y x$
33 32 adantr $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ _ y x$
34 31 33 nfeqd $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ y w = x$
35 7 34 nfan1 $⊢ Ⅎ y ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x$
36 nfcvd $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ _ z w$
37 nfcvf2 $⊢ ¬ ∀ x x = z → Ⅎ _ z x$
38 37 adantl $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ _ z x$
39 36 38 nfeqd $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ z w = x$
40 10 39 nfan1 $⊢ Ⅎ z ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x$
41 sbequ12r $⊢ w = x → w x φ ↔ φ$
42 41 imbi1d $⊢ w = x → w x φ → z = y ↔ φ → z = y$
43 42 adantl $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → w x φ → z = y ↔ φ → z = y$
44 40 43 albid $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → ∀ z w x φ → z = y ↔ ∀ z φ → z = y$
45 35 44 exbid $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → ∃ y ∀ z w x φ → z = y ↔ ∃ y ∀ z φ → z = y$
46 elequ2 $⊢ w = x → z ∈ w ↔ z ∈ x$
47 46 adantl $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → z ∈ w ↔ z ∈ x$
48 elequ1 $⊢ w = x → w ∈ y ↔ x ∈ y$
49 48 adantl $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → w ∈ y ↔ x ∈ y$
50 41 adantl $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → w x φ ↔ φ$
51 35 50 albid $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → ∀ y w x φ ↔ ∀ y φ$
52 49 51 anbi12d $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → w ∈ y ∧ ∀ y w x φ ↔ x ∈ y ∧ ∀ y φ$
53 52 ex $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → w = x → w ∈ y ∧ ∀ y w x φ ↔ x ∈ y ∧ ∀ y φ$
54 4 26 53 cbvexd $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → ∃ w w ∈ y ∧ ∀ y w x φ ↔ ∃ x x ∈ y ∧ ∀ y φ$
55 54 adantr $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → ∃ w w ∈ y ∧ ∀ y w x φ ↔ ∃ x x ∈ y ∧ ∀ y φ$
56 47 55 bibi12d $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → z ∈ w ↔ ∃ w w ∈ y ∧ ∀ y w x φ ↔ z ∈ x ↔ ∃ x x ∈ y ∧ ∀ y φ$
57 40 56 albid $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → ∀ z z ∈ w ↔ ∃ w w ∈ y ∧ ∀ y w x φ ↔ ∀ z z ∈ x ↔ ∃ x x ∈ y ∧ ∀ y φ$
58 45 57 imbi12d $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → ∃ y ∀ z w x φ → z = y → ∀ z z ∈ w ↔ ∃ w w ∈ y ∧ ∀ y w x φ ↔ ∃ y ∀ z φ → z = y → ∀ z z ∈ x ↔ ∃ x x ∈ y ∧ ∀ y φ$
59 58 ex $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → w = x → ∃ y ∀ z w x φ → z = y → ∀ z z ∈ w ↔ ∃ w w ∈ y ∧ ∀ y w x φ ↔ ∃ y ∀ z φ → z = y → ∀ z z ∈ x ↔ ∃ x x ∈ y ∧ ∀ y φ$
60 4 30 59 cbvexd $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → ∃ w ∃ y ∀ z w x φ → z = y → ∀ z z ∈ w ↔ ∃ w w ∈ y ∧ ∀ y w x φ ↔ ∃ x ∃ y ∀ z φ → z = y → ∀ z z ∈ x ↔ ∃ x x ∈ y ∧ ∀ y φ$
61 1 60 syl5ib $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → ¬ ∀ y y = z → ∃ x ∃ y ∀ z φ → z = y → ∀ z z ∈ x ↔ ∃ x x ∈ y ∧ ∀ y φ$
62 61 imp $⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → ∃ x ∃ y ∀ z φ → z = y → ∀ z z ∈ x ↔ ∃ x x ∈ y ∧ ∀ y φ$