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

Metamath Proof Explorer

Theorem zfrep3cl

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 zfrep3cl.1 ⊢ 𝐴 ∈ V
zfrep3cl.2 ⊢ ( 𝑥 ∈ 𝐴 → ∃ 𝑧 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑧 ) )
Assertion zfrep3cl ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )

Proof

Step Hyp Ref Expression
1 zfrep3cl.1 ⊢ 𝐴 ∈ V
2 zfrep3cl.2 ⊢ ( 𝑥 ∈ 𝐴 → ∃ 𝑧 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑧 ) )
3 nfcv ⊢ Ⅎ 𝑥 𝐴
4 3 1 2 zfrepclf ⊢ ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )