Metamath Proof Explorer


Theorem ssralv

Description: Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006) Avoid axioms. (Revised by GG, 19-May-2025)

Ref Expression
Assertion ssralv A B x B φ x A φ

Proof

Step Hyp Ref Expression
1 df-ss A B x x A x B
2 imim1 x A x B x B φ x A φ
3 2 al2imi x x A x B x x B φ x x A φ
4 df-ral x B φ x x B φ
5 df-ral x A φ x x A φ
6 3 4 5 3imtr4g x x A x B x B φ x A φ
7 1 6 sylbi A B x B φ x A φ