Metamath Proof Explorer


Theorem rabexgOLD

Description: Obsolete proof of rabexg as of 24-Jul-2025). (Contributed by NM, 23-Oct-1999) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion rabexgOLD ( 𝐴𝑉 → { 𝑥𝐴𝜑 } ∈ V )

Proof

Step Hyp Ref Expression
1 ssrab2 { 𝑥𝐴𝜑 } ⊆ 𝐴
2 ssexg ( ( { 𝑥𝐴𝜑 } ⊆ 𝐴𝐴𝑉 ) → { 𝑥𝐴𝜑 } ∈ V )
3 1 2 mpan ( 𝐴𝑉 → { 𝑥𝐴𝜑 } ∈ V )