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

Metamath Proof Explorer

Theorem zfrep4

Description: A version of Replacement using class abstractions. (Contributed by NM, 26-Nov-1995)

Ref Expression
Hypotheses zfrep4.1 ⊢ { 𝑥 ∣ 𝜑 } ∈ V
zfrep4.2 ⊢ ( 𝜑 → ∃ 𝑧 ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) )
Assertion zfrep4 { 𝑦 ∣ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) } ∈ V

Proof

Step Hyp Ref Expression
1 zfrep4.1 ⊢ { 𝑥 ∣ 𝜑 } ∈ V
2 zfrep4.2 ⊢ ( 𝜑 → ∃ 𝑧 ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) )
3 abid ⊢ ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜑 )
4 3 anbi1i ⊢ ( ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝜓 ) ↔ ( 𝜑 ∧ 𝜓 ) )
5 4 exbii ⊢ ( ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝜓 ) ↔ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) )
6 5 abbii ⊢ { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝜓 ) } = { 𝑦 ∣ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) }
7 nfab1 ⊢ Ⅎ 𝑥 { 𝑥 ∣ 𝜑 }
8 3 2 sylbi ⊢ ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } → ∃ 𝑧 ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) )
9 7 1 8 zfrepclf ⊢ ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝜓 ) )
10 eqabb ⊢ ( 𝑧 = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝜓 ) } ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝜓 ) ) )
11 10 exbii ⊢ ( ∃ 𝑧 𝑧 = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝜓 ) } ↔ ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝜓 ) ) )
12 9 11 mpbir ⊢ ∃ 𝑧 𝑧 = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝜓 ) }
13 12 issetri ⊢ { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝜓 ) } ∈ V
14 6 13 eqeltrri ⊢ { 𝑦 ∣ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) } ∈ V