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

Metamath Proof Explorer

Theorem abexex

Description: A condition where a class abstraction continues to exist after its wff is existentially quantified. (Contributed by NM, 4-Mar-2007)

Ref Expression
Hypotheses abexex.1 ⊢ 𝐴 ∈ V
abexex.2 ⊢ ( 𝜑 → 𝑥 ∈ 𝐴 )
abexex.3 ⊢ { 𝑦 ∣ 𝜑 } ∈ V
Assertion abexex { 𝑦 ∣ ∃ 𝑥 𝜑 } ∈ V

Proof

Step Hyp Ref Expression
1 abexex.1 ⊢ 𝐴 ∈ V
2 abexex.2 ⊢ ( 𝜑 → 𝑥 ∈ 𝐴 )
3 abexex.3 ⊢ { 𝑦 ∣ 𝜑 } ∈ V
4 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
5 2 pm4.71ri ⊢ ( 𝜑 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
6 5 exbii ⊢ ( ∃ 𝑥 𝜑 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
7 4 6 bitr4i ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 𝜑 )
8 7 abbii ⊢ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } = { 𝑦 ∣ ∃ 𝑥 𝜑 }
9 1 3 abrexex2 ⊢ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } ∈ V
10 8 9 eqeltrri ⊢ { 𝑦 ∣ ∃ 𝑥 𝜑 } ∈ V