Metamath Proof Explorer


Theorem axrep4

Description: A more traditional version of the Axiom of Replacement. (Contributed by NM, 14-Aug-1994)

Ref Expression
Hypothesis axrep4.1 𝑧 𝜑
Assertion axrep4 ( ∀ 𝑥𝑧𝑦 ( 𝜑𝑦 = 𝑧 ) → ∃ 𝑧𝑦 ( 𝑦𝑧 ↔ ∃ 𝑥 ( 𝑥𝑤𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 axrep4.1 𝑧 𝜑
2 axrep3 𝑥 ( ∃ 𝑧𝑦 ( 𝜑𝑦 = 𝑧 ) → ∀ 𝑦 ( 𝑦𝑥 ↔ ∃ 𝑥 ( 𝑥𝑤 ∧ ∀ 𝑧 𝜑 ) ) )
3 2 19.35i ( ∀ 𝑥𝑧𝑦 ( 𝜑𝑦 = 𝑧 ) → ∃ 𝑥𝑦 ( 𝑦𝑥 ↔ ∃ 𝑥 ( 𝑥𝑤 ∧ ∀ 𝑧 𝜑 ) ) )
4 nfv 𝑧 𝑦𝑥
5 nfv 𝑧 𝑥𝑤
6 nfa1 𝑧𝑧 𝜑
7 5 6 nfan 𝑧 ( 𝑥𝑤 ∧ ∀ 𝑧 𝜑 )
8 7 nfex 𝑧𝑥 ( 𝑥𝑤 ∧ ∀ 𝑧 𝜑 )
9 4 8 nfbi 𝑧 ( 𝑦𝑥 ↔ ∃ 𝑥 ( 𝑥𝑤 ∧ ∀ 𝑧 𝜑 ) )
10 9 nfal 𝑧𝑦 ( 𝑦𝑥 ↔ ∃ 𝑥 ( 𝑥𝑤 ∧ ∀ 𝑧 𝜑 ) )
11 nfv 𝑥 𝑦𝑧
12 nfe1 𝑥𝑥 ( 𝑥𝑤𝜑 )
13 11 12 nfbi 𝑥 ( 𝑦𝑧 ↔ ∃ 𝑥 ( 𝑥𝑤𝜑 ) )
14 13 nfal 𝑥𝑦 ( 𝑦𝑧 ↔ ∃ 𝑥 ( 𝑥𝑤𝜑 ) )
15 elequ2 ( 𝑥 = 𝑧 → ( 𝑦𝑥𝑦𝑧 ) )
16 1 19.3 ( ∀ 𝑧 𝜑𝜑 )
17 16 anbi2i ( ( 𝑥𝑤 ∧ ∀ 𝑧 𝜑 ) ↔ ( 𝑥𝑤𝜑 ) )
18 17 exbii ( ∃ 𝑥 ( 𝑥𝑤 ∧ ∀ 𝑧 𝜑 ) ↔ ∃ 𝑥 ( 𝑥𝑤𝜑 ) )
19 18 a1i ( 𝑥 = 𝑧 → ( ∃ 𝑥 ( 𝑥𝑤 ∧ ∀ 𝑧 𝜑 ) ↔ ∃ 𝑥 ( 𝑥𝑤𝜑 ) ) )
20 15 19 bibi12d ( 𝑥 = 𝑧 → ( ( 𝑦𝑥 ↔ ∃ 𝑥 ( 𝑥𝑤 ∧ ∀ 𝑧 𝜑 ) ) ↔ ( 𝑦𝑧 ↔ ∃ 𝑥 ( 𝑥𝑤𝜑 ) ) ) )
21 20 albidv ( 𝑥 = 𝑧 → ( ∀ 𝑦 ( 𝑦𝑥 ↔ ∃ 𝑥 ( 𝑥𝑤 ∧ ∀ 𝑧 𝜑 ) ) ↔ ∀ 𝑦 ( 𝑦𝑧 ↔ ∃ 𝑥 ( 𝑥𝑤𝜑 ) ) ) )
22 10 14 21 cbvexv1 ( ∃ 𝑥𝑦 ( 𝑦𝑥 ↔ ∃ 𝑥 ( 𝑥𝑤 ∧ ∀ 𝑧 𝜑 ) ) ↔ ∃ 𝑧𝑦 ( 𝑦𝑧 ↔ ∃ 𝑥 ( 𝑥𝑤𝜑 ) ) )
23 3 22 sylib ( ∀ 𝑥𝑧𝑦 ( 𝜑𝑦 = 𝑧 ) → ∃ 𝑧𝑦 ( 𝑦𝑧 ↔ ∃ 𝑥 ( 𝑥𝑤𝜑 ) ) )