Metamath Proof Explorer


Theorem ssralv

Description: Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006)

Ref Expression
Assertion ssralv ABxBφxAφ

Proof

Step Hyp Ref Expression
1 ssel ABxAxB
2 1 imim1d ABxBφxAφ
3 2 ralimdv2 ABxBφxAφ