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