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
|- ( A e. V -> { x e. A | ph } e. _V )

Proof

Step Hyp Ref Expression
1 ssrab2
 |-  { x e. A | ph } C_ A
2 ssexg
 |-  ( ( { x e. A | ph } C_ A /\ A e. V ) -> { x e. A | ph } e. _V )
3 1 2 mpan
 |-  ( A e. V -> { x e. A | ph } e. _V )