Metamath Proof Explorer


Theorem axrep3

Description: Axiom of Replacement slightly strengthened from axrep2 ; w may occur free in ph . (Contributed by NM, 2-Jan-1997) Remove dependency on ax-13 . (Revised by BJ, 31-May-2019)

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

Proof

Step Hyp Ref Expression
1 nfe1 𝑦𝑦𝑧 ( 𝜑𝑧 = 𝑦 )
2 nfv 𝑦 𝑧𝑥
3 nfv 𝑦 𝑥𝑤
4 nfa1 𝑦𝑦 𝜑
5 3 4 nfan 𝑦 ( 𝑥𝑤 ∧ ∀ 𝑦 𝜑 )
6 5 nfex 𝑦𝑥 ( 𝑥𝑤 ∧ ∀ 𝑦 𝜑 )
7 2 6 nfbi 𝑦 ( 𝑧𝑥 ↔ ∃ 𝑥 ( 𝑥𝑤 ∧ ∀ 𝑦 𝜑 ) )
8 7 nfal 𝑦𝑧 ( 𝑧𝑥 ↔ ∃ 𝑥 ( 𝑥𝑤 ∧ ∀ 𝑦 𝜑 ) )
9 1 8 nfim 𝑦 ( ∃ 𝑦𝑧 ( 𝜑𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧𝑥 ↔ ∃ 𝑥 ( 𝑥𝑤 ∧ ∀ 𝑦 𝜑 ) ) )
10 9 nfex 𝑦𝑥 ( ∃ 𝑦𝑧 ( 𝜑𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧𝑥 ↔ ∃ 𝑥 ( 𝑥𝑤 ∧ ∀ 𝑦 𝜑 ) ) )
11 axreplem ( 𝑦 = 𝑤 → ( ∃ 𝑥 ( ∃ 𝑦𝑧 ( 𝜑𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧𝑥 ↔ ∃ 𝑥 ( 𝑥𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) ↔ ∃ 𝑥 ( ∃ 𝑦𝑧 ( 𝜑𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧𝑥 ↔ ∃ 𝑥 ( 𝑥𝑤 ∧ ∀ 𝑦 𝜑 ) ) ) ) )
12 axrep2 𝑥 ( ∃ 𝑦𝑧 ( 𝜑𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧𝑥 ↔ ∃ 𝑥 ( 𝑥𝑦 ∧ ∀ 𝑦 𝜑 ) ) )
13 10 11 12 chvarfv 𝑥 ( ∃ 𝑦𝑧 ( 𝜑𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧𝑥 ↔ ∃ 𝑥 ( 𝑥𝑤 ∧ ∀ 𝑦 𝜑 ) ) )