Metamath Proof Explorer


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