Metamath Proof Explorer


Theorem axrep2

Description: Axiom of Replacement expressed with the fewest number of different variables and without any restrictions on ph . (Contributed by NM, 15-Aug-2003) Remove dependency on ax-13 . (Revised by BJ, 31-May-2019)

Ref Expression
Assertion axrep2 𝑥 ( ∃ 𝑦𝑧 ( 𝜑𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧𝑥 ↔ ∃ 𝑥 ( 𝑥𝑦 ∧ ∀ 𝑦 𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 nfe1 𝑤𝑤𝑧 ( ∀ 𝑦 𝜑𝑧 = 𝑤 )
2 nfv 𝑤𝑧 ( 𝑧𝑥 ↔ ∃ 𝑥 ( 𝑥𝑦 ∧ ∀ 𝑦 𝜑 ) )
3 1 2 nfim 𝑤 ( ∃ 𝑤𝑧 ( ∀ 𝑦 𝜑𝑧 = 𝑤 ) → ∀ 𝑧 ( 𝑧𝑥 ↔ ∃ 𝑥 ( 𝑥𝑦 ∧ ∀ 𝑦 𝜑 ) ) )
4 3 nfex 𝑤𝑥 ( ∃ 𝑤𝑧 ( ∀ 𝑦 𝜑𝑧 = 𝑤 ) → ∀ 𝑧 ( 𝑧𝑥 ↔ ∃ 𝑥 ( 𝑥𝑦 ∧ ∀ 𝑦 𝜑 ) ) )
5 axreplem ( 𝑤 = 𝑦 → ( ∃ 𝑥 ( ∃ 𝑤𝑧 ( ∀ 𝑦 𝜑𝑧 = 𝑤 ) → ∀ 𝑧 ( 𝑧𝑥 ↔ ∃ 𝑥 ( 𝑥𝑤 ∧ ∀ 𝑦 𝜑 ) ) ) ↔ ∃ 𝑥 ( ∃ 𝑤𝑧 ( ∀ 𝑦 𝜑𝑧 = 𝑤 ) → ∀ 𝑧 ( 𝑧𝑥 ↔ ∃ 𝑥 ( 𝑥𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) ) )
6 axrep1 𝑥 ( ∃ 𝑤𝑧 ( ∀ 𝑦 𝜑𝑧 = 𝑤 ) → ∀ 𝑧 ( 𝑧𝑥 ↔ ∃ 𝑥 ( 𝑥𝑤 ∧ ∀ 𝑦 𝜑 ) ) )
7 4 5 6 chvarfv 𝑥 ( ∃ 𝑤𝑧 ( ∀ 𝑦 𝜑𝑧 = 𝑤 ) → ∀ 𝑧 ( 𝑧𝑥 ↔ ∃ 𝑥 ( 𝑥𝑦 ∧ ∀ 𝑦 𝜑 ) ) )
8 sp ( ∀ 𝑦 𝜑𝜑 )
9 8 imim1i ( ( 𝜑𝑧 = 𝑦 ) → ( ∀ 𝑦 𝜑𝑧 = 𝑦 ) )
10 9 alimi ( ∀ 𝑧 ( 𝜑𝑧 = 𝑦 ) → ∀ 𝑧 ( ∀ 𝑦 𝜑𝑧 = 𝑦 ) )
11 10 eximi ( ∃ 𝑦𝑧 ( 𝜑𝑧 = 𝑦 ) → ∃ 𝑦𝑧 ( ∀ 𝑦 𝜑𝑧 = 𝑦 ) )
12 nfv 𝑤𝑧 ( ∀ 𝑦 𝜑𝑧 = 𝑦 )
13 nfa1 𝑦𝑦 𝜑
14 nfv 𝑦 𝑧 = 𝑤
15 13 14 nfim 𝑦 ( ∀ 𝑦 𝜑𝑧 = 𝑤 )
16 15 nfal 𝑦𝑧 ( ∀ 𝑦 𝜑𝑧 = 𝑤 )
17 equequ2 ( 𝑦 = 𝑤 → ( 𝑧 = 𝑦𝑧 = 𝑤 ) )
18 17 imbi2d ( 𝑦 = 𝑤 → ( ( ∀ 𝑦 𝜑𝑧 = 𝑦 ) ↔ ( ∀ 𝑦 𝜑𝑧 = 𝑤 ) ) )
19 18 albidv ( 𝑦 = 𝑤 → ( ∀ 𝑧 ( ∀ 𝑦 𝜑𝑧 = 𝑦 ) ↔ ∀ 𝑧 ( ∀ 𝑦 𝜑𝑧 = 𝑤 ) ) )
20 12 16 19 cbvexv1 ( ∃ 𝑦𝑧 ( ∀ 𝑦 𝜑𝑧 = 𝑦 ) ↔ ∃ 𝑤𝑧 ( ∀ 𝑦 𝜑𝑧 = 𝑤 ) )
21 11 20 sylib ( ∃ 𝑦𝑧 ( 𝜑𝑧 = 𝑦 ) → ∃ 𝑤𝑧 ( ∀ 𝑦 𝜑𝑧 = 𝑤 ) )
22 21 imim1i ( ( ∃ 𝑤𝑧 ( ∀ 𝑦 𝜑𝑧 = 𝑤 ) → ∀ 𝑧 ( 𝑧𝑥 ↔ ∃ 𝑥 ( 𝑥𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) → ( ∃ 𝑦𝑧 ( 𝜑𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧𝑥 ↔ ∃ 𝑥 ( 𝑥𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) )
23 7 22 eximii 𝑥 ( ∃ 𝑦𝑧 ( 𝜑𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧𝑥 ↔ ∃ 𝑥 ( 𝑥𝑦 ∧ ∀ 𝑦 𝜑 ) ) )