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 ∃ 𝑥 ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( ∀ 𝑦 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( ∀ 𝑧 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) )

Proof

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