Metamath Proof Explorer


Theorem rabss

Description: Restricted class abstraction in a subclass relationship. (Contributed by NM, 16-Aug-2006)

Ref Expression
Assertion rabss x A | φ B x A φ x B

Proof

Step Hyp Ref Expression
1 df-rab x A | φ = x | x A φ
2 1 sseq1i x A | φ B x | x A φ B
3 abss x | x A φ B x x A φ x B
4 impexp x A φ x B x A φ x B
5 4 albii x x A φ x B x x A φ x B
6 df-ral x A φ x B x x A φ x B
7 5 6 bitr4i x x A φ x B x A φ x B
8 2 3 7 3bitri x A | φ B x A φ x B