Metamath Proof Explorer


Theorem ssrab2OLD

Description: Obsolete version of ssrab2 as of 8-Aug-2024. (Contributed by NM, 19-Mar-1997) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion ssrab2OLD xA|φA

Proof

Step Hyp Ref Expression
1 df-rab xA|φ=x|xAφ
2 ssab2 x|xAφA
3 1 2 eqsstri xA|φA