Theorem abexssex

Description: Existence of a class abstraction with an existentially quantified expression. Both x and y can be free in ph . (Contributed by NM, 29-Jul-2006)

	Ref	Expression
Hypotheses	abrexex2.1	⊢ 𝐴 ∈ V
	abrexex2.2	⊢ { 𝑦 ∣ 𝜑 } ∈ V
Assertion	abexssex	⊢ { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝜑 ) } ∈ V

Proof

Step	Hyp	Ref	Expression
1		abrexex2.1	⊢ 𝐴 ∈ V
2		abrexex2.2	⊢ { 𝑦 ∣ 𝜑 } ∈ V
3		df-rex	⊢ ( ∃ 𝑥 ∈ 𝒫 𝐴 𝜑 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝜑 ) )
4		velpw	⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
5	4	anbi1i	⊢ ( ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝜑 ) ↔ ( 𝑥 ⊆ 𝐴 ∧ 𝜑 ) )
6	5	exbii	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝜑 ) )
7	3 6	bitri	⊢ ( ∃ 𝑥 ∈ 𝒫 𝐴 𝜑 ↔ ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝜑 ) )
8	7	abbii	⊢ { 𝑦 ∣ ∃ 𝑥 ∈ 𝒫 𝐴 𝜑 } = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝜑 ) }
9	1	pwex	⊢ 𝒫 𝐴 ∈ V
10	9 2	abrexex2	⊢ { 𝑦 ∣ ∃ 𝑥 ∈ 𝒫 𝐴 𝜑 } ∈ V
11	8 10	eqeltrri	⊢ { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝜑 ) } ∈ V