This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zfrepclf

Description: An inference based on the Axiom of Replacement. Typically, ph defines a function from x to y . (Contributed by NM, 26-Nov-1995)

Ref Expression
Hypotheses zfrepclf.1 ⊢ Ⅎ 𝑥 𝐴
zfrepclf.2 ⊢ 𝐴 ∈ V
zfrepclf.3 ⊢ ( 𝑥 ∈ 𝐴 → ∃ 𝑧 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑧 ) )
Assertion zfrepclf ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )

Proof

Step Hyp Ref Expression
1 zfrepclf.1 ⊢ Ⅎ 𝑥 𝐴
2 zfrepclf.2 ⊢ 𝐴 ∈ V
3 zfrepclf.3 ⊢ ( 𝑥 ∈ 𝐴 → ∃ 𝑧 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑧 ) )
4 1 nfeq2 ⊢ Ⅎ 𝑥 𝑣 = 𝐴
5 eleq2 ⊢ ( 𝑣 = 𝐴 → ( 𝑥 ∈ 𝑣 ↔ 𝑥 ∈ 𝐴 ) )
6 5 3 biimtrdi ⊢ ( 𝑣 = 𝐴 → ( 𝑥 ∈ 𝑣 → ∃ 𝑧 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑧 ) ) )
7 4 6 alrimi ⊢ ( 𝑣 = 𝐴 → ∀ 𝑥 ( 𝑥 ∈ 𝑣 → ∃ 𝑧 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑧 ) ) )
8 nfv ⊢ Ⅎ 𝑧 𝜑
9 8 axrep5 ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝑣 → ∃ 𝑧 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑧 ) ) → ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑣 ∧ 𝜑 ) ) )
10 7 9 syl ⊢ ( 𝑣 = 𝐴 → ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑣 ∧ 𝜑 ) ) )
11 5 anbi1d ⊢ ( 𝑣 = 𝐴 → ( ( 𝑥 ∈ 𝑣 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
12 4 11 exbid ⊢ ( 𝑣 = 𝐴 → ( ∃ 𝑥 ( 𝑥 ∈ 𝑣 ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
13 12 bibi2d ⊢ ( 𝑣 = 𝐴 → ( ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑣 ∧ 𝜑 ) ) ↔ ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ) )
14 13 albidv ⊢ ( 𝑣 = 𝐴 → ( ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑣 ∧ 𝜑 ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ) )
15 14 exbidv ⊢ ( 𝑣 = 𝐴 → ( ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑣 ∧ 𝜑 ) ) ↔ ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ) )
16 10 15 mpbid ⊢ ( 𝑣 = 𝐴 → ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
17 2 16 vtocle ⊢ ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )