This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rabssrabd

Description: Subclass of a restricted class abstraction. (Contributed by AV, 4-Jun-2022)

Ref Expression
Hypotheses rabssrabd.1 
|- ( ph -> A C_ B )
rabssrabd.2 
|- ( ( ph /\ ps /\ x e. A ) -> ch )
Assertion rabssrabd 
|- ( ph -> { x e. A | ps } C_ { x e. B | ch } )

Proof

Step Hyp Ref Expression
1 rabssrabd.1 
 |-  ( ph -> A C_ B )
2 rabssrabd.2 
 |-  ( ( ph /\ ps /\ x e. A ) -> ch )
3 3anan32 
 |-  ( ( ph /\ ps /\ x e. A ) <-> ( ( ph /\ x e. A ) /\ ps ) )
4 3 2 sylbir 
 |-  ( ( ( ph /\ x e. A ) /\ ps ) -> ch )
5 4 ex 
 |-  ( ( ph /\ x e. A ) -> ( ps -> ch ) )
6 5 ss2rabdv 
 |-  ( ph -> { x e. A | ps } C_ { x e. A | ch } )
7 rabss2 
 |-  ( A C_ B -> { x e. A | ch } C_ { x e. B | ch } )
8 1 7 syl 
 |-  ( ph -> { x e. A | ch } C_ { x e. B | ch } )
9 6 8 sstrd 
 |-  ( ph -> { x e. A | ps } C_ { x e. B | ch } )