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∀yz∈x↔∃x∀zx∈y∧∀yφ

Proof

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