Theorem abrexex2

Description: Existence of an existentially restricted class abstraction. ph normally has free-variable parameters x and y . See also abrexex . (Contributed by NM, 12-Sep-2004)

	Ref	Expression
Hypotheses	abrexex2.1	⊢ 𝐴 ∈ V
	abrexex2.2	⊢ { 𝑦 ∣ 𝜑 } ∈ V
Assertion	abrexex2	⊢ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } ∈ V

Proof

Step	Hyp	Ref	Expression
1		abrexex2.1	⊢ 𝐴 ∈ V
2		abrexex2.2	⊢ { 𝑦 ∣ 𝜑 } ∈ V
3	2	rgenw	⊢ ∀ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } ∈ V
4		abrexex2g	⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } ∈ V ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } ∈ V )
5	1 3 4	mp2an	⊢ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } ∈ V