Metamath Proof Explorer

Theorem axrepnd

Description: A version of 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) (New usage is discouraged.)

Ref Expression
Assertion axrepnd ⊢ ∃ x ∃ y ∀ z φ → z = y → ∀ z ∀ y z ∈ x ↔ ∃ x ∀ z x ∈ y ∧ ∀ y φ

Proof

Step Hyp Ref Expression
1 axrepndlem2 ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → ∃ x ∃ y ∀ z φ → z = y → ∀ z z ∈ x ↔ ∃ x x ∈ y ∧ ∀ y φ
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 ⊢ Ⅎ x ¬ ∀ y y = z
6 4 5 nfan ⊢ Ⅎ x ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ ¬ ∀ y y = z
7 nfnae ⊢ Ⅎ z ¬ ∀ x x = y
8 nfnae ⊢ Ⅎ z ¬ ∀ x x = z
9 7 8 nfan ⊢ Ⅎ z ¬ ∀ x x = y ∧ ¬ ∀ x x = z
10 nfnae ⊢ Ⅎ z ¬ ∀ y y = z
11 9 10 nfan ⊢ Ⅎ z ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ ¬ ∀ y y = z
12 nfcvf ⊢ ¬ ∀ y y = z → Ⅎ _ y z
13 12 adantl ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → Ⅎ _ y z
14 nfcvf2 ⊢ ¬ ∀ x x = y → Ⅎ _ y x
15 14 ad2antrr ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → Ⅎ _ y x
16 13 15 nfeld ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → Ⅎ y z ∈ x
17 16 nf5rd ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → z ∈ x → ∀ y z ∈ x
18 sp ⊢ ∀ y z ∈ x → z ∈ x
19 17 18 impbid1 ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → z ∈ x ↔ ∀ y z ∈ x
20 nfcvf2 ⊢ ¬ ∀ x x = z → Ⅎ _ z x
21 20 ad2antlr ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → Ⅎ _ z x
22 nfcvf2 ⊢ ¬ ∀ y y = z → Ⅎ _ z y
23 22 adantl ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → Ⅎ _ z y
24 21 23 nfeld ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → Ⅎ z x ∈ y
25 24 nf5rd ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → x ∈ y → ∀ z x ∈ y
26 sp ⊢ ∀ z x ∈ y → x ∈ y
27 25 26 impbid1 ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → x ∈ y ↔ ∀ z x ∈ y
28 27 anbi1d ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → x ∈ y ∧ ∀ y φ ↔ ∀ z x ∈ y ∧ ∀ y φ
29 6 28 exbid ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → ∃ x x ∈ y ∧ ∀ y φ ↔ ∃ x ∀ z x ∈ y ∧ ∀ y φ
30 19 29 bibi12d ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → z ∈ x ↔ ∃ x x ∈ y ∧ ∀ y φ ↔ ∀ y z ∈ x ↔ ∃ x ∀ z x ∈ y ∧ ∀ y φ
31 11 30 albid ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → ∀ z z ∈ x ↔ ∃ x x ∈ y ∧ ∀ y φ ↔ ∀ z ∀ y z ∈ x ↔ ∃ x ∀ z x ∈ y ∧ ∀ y φ
32 31 imbi2d ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → ∃ y ∀ z φ → z = y → ∀ z z ∈ x ↔ ∃ x x ∈ y ∧ ∀ y φ ↔ ∃ y ∀ z φ → z = y → ∀ z ∀ y z ∈ x ↔ ∃ x ∀ z x ∈ y ∧ ∀ y φ
33 6 32 exbid ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → ∃ x ∃ y ∀ z φ → z = y → ∀ z z ∈ x ↔ ∃ x x ∈ y ∧ ∀ y φ ↔ ∃ x ∃ y ∀ z φ → z = y → ∀ z ∀ y z ∈ x ↔ ∃ x ∀ z x ∈ y ∧ ∀ y φ
34 1 33 mpbid ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → ∃ x ∃ y ∀ z φ → z = y → ∀ z ∀ y z ∈ x ↔ ∃ x ∀ z x ∈ y ∧ ∀ y φ
35 34 exp31 ⊢ ¬ ∀ x x = y → ¬ ∀ x x = z → ¬ ∀ y y = z → ∃ x ∃ y ∀ z φ → z = y → ∀ z ∀ y z ∈ x ↔ ∃ x ∀ z x ∈ y ∧ ∀ y φ
36 nfae ⊢ Ⅎ z ∀ x x = y
37 nd2 ⊢ ∀ y y = x → ¬ ∀ y z ∈ x
38 37 aecoms ⊢ ∀ x x = y → ¬ ∀ y z ∈ x
39 nfae ⊢ Ⅎ x ∀ x x = y
40 nd3 ⊢ ∀ x x = y → ¬ ∀ z x ∈ y
41 40 intnanrd ⊢ ∀ x x = y → ¬ ∀ z x ∈ y ∧ ∀ y φ
42 39 41 nexd ⊢ ∀ x x = y → ¬ ∃ x ∀ z x ∈ y ∧ ∀ y φ
43 38 42 2falsed ⊢ ∀ x x = y → ∀ y z ∈ x ↔ ∃ x ∀ z x ∈ y ∧ ∀ y φ
44 36 43 alrimi ⊢ ∀ x x = y → ∀ z ∀ y z ∈ x ↔ ∃ x ∀ z x ∈ y ∧ ∀ y φ
45 44 a1d ⊢ ∀ x x = y → ∃ y ∀ z φ → z = y → ∀ z ∀ y z ∈ x ↔ ∃ x ∀ z x ∈ y ∧ ∀ y φ
46 45 19.8ad ⊢ ∀ x x = y → ∃ x ∃ y ∀ z φ → z = y → ∀ z ∀ y z ∈ x ↔ ∃ x ∀ z x ∈ y ∧ ∀ y φ
47 nfae ⊢ Ⅎ z ∀ x x = z
48 nd4 ⊢ ∀ x x = z → ¬ ∀ y z ∈ x
49 nfae ⊢ Ⅎ x ∀ x x = z
50 nd1 ⊢ ∀ z z = x → ¬ ∀ z x ∈ y
51 50 aecoms ⊢ ∀ x x = z → ¬ ∀ z x ∈ y
52 51 intnanrd ⊢ ∀ x x = z → ¬ ∀ z x ∈ y ∧ ∀ y φ
53 49 52 nexd ⊢ ∀ x x = z → ¬ ∃ x ∀ z x ∈ y ∧ ∀ y φ
54 48 53 2falsed ⊢ ∀ x x = z → ∀ y z ∈ x ↔ ∃ x ∀ z x ∈ y ∧ ∀ y φ
55 47 54 alrimi ⊢ ∀ x x = z → ∀ z ∀ y z ∈ x ↔ ∃ x ∀ z x ∈ y ∧ ∀ y φ
56 55 a1d ⊢ ∀ x x = z → ∃ y ∀ z φ → z = y → ∀ z ∀ y z ∈ x ↔ ∃ x ∀ z x ∈ y ∧ ∀ y φ
57 56 19.8ad ⊢ ∀ x x = z → ∃ x ∃ y ∀ z φ → z = y → ∀ z ∀ y z ∈ x ↔ ∃ x ∀ z x ∈ y ∧ ∀ y φ
58 nfae ⊢ Ⅎ z ∀ y y = z
59 nd1 ⊢ ∀ y y = z → ¬ ∀ y z ∈ x
60 nfae ⊢ Ⅎ x ∀ y y = z
61 nd2 ⊢ ∀ z z = y → ¬ ∀ z x ∈ y
62 61 aecoms ⊢ ∀ y y = z → ¬ ∀ z x ∈ y
63 62 intnanrd ⊢ ∀ y y = z → ¬ ∀ z x ∈ y ∧ ∀ y φ
64 60 63 nexd ⊢ ∀ y y = z → ¬ ∃ x ∀ z x ∈ y ∧ ∀ y φ
65 59 64 2falsed ⊢ ∀ y y = z → ∀ y z ∈ x ↔ ∃ x ∀ z x ∈ y ∧ ∀ y φ
66 58 65 alrimi ⊢ ∀ y y = z → ∀ z ∀ y z ∈ x ↔ ∃ x ∀ z x ∈ y ∧ ∀ y φ
67 66 a1d ⊢ ∀ y y = z → ∃ y ∀ z φ → z = y → ∀ z ∀ y z ∈ x ↔ ∃ x ∀ z x ∈ y ∧ ∀ y φ
68 67 19.8ad ⊢ ∀ y y = z → ∃ x ∃ y ∀ z φ → z = y → ∀ z ∀ y z ∈ x ↔ ∃ x ∀ z x ∈ y ∧ ∀ y φ
69 35 46 57 68 pm2.61iii ⊢ ∃ x ∃ y ∀ z φ → z = y → ∀ z ∀ y z ∈ x ↔ ∃ x ∀ z x ∈ y ∧ ∀ y φ