Metamath Proof Explorer


Theorem rabss3d

Description: Subclass law for restricted abstraction. (Contributed by Thierry Arnoux, 25-Sep-2017)

Ref Expression
Hypothesis rabss3d.1
|- ( ( ph /\ ( x e. A /\ ps ) ) -> x e. B )
Assertion rabss3d
|- ( ph -> { x e. A | ps } C_ { x e. B | ps } )

Proof

Step Hyp Ref Expression
1 rabss3d.1
 |-  ( ( ph /\ ( x e. A /\ ps ) ) -> x e. B )
2 nfv
 |-  F/ x ph
3 nfrab1
 |-  F/_ x { x e. A | ps }
4 nfrab1
 |-  F/_ x { x e. B | ps }
5 simprr
 |-  ( ( ph /\ ( x e. A /\ ps ) ) -> ps )
6 1 5 jca
 |-  ( ( ph /\ ( x e. A /\ ps ) ) -> ( x e. B /\ ps ) )
7 6 ex
 |-  ( ph -> ( ( x e. A /\ ps ) -> ( x e. B /\ ps ) ) )
8 rabid
 |-  ( x e. { x e. A | ps } <-> ( x e. A /\ ps ) )
9 rabid
 |-  ( x e. { x e. B | ps } <-> ( x e. B /\ ps ) )
10 7 8 9 3imtr4g
 |-  ( ph -> ( x e. { x e. A | ps } -> x e. { x e. B | ps } ) )
11 2 3 4 10 ssrd
 |-  ( ph -> { x e. A | ps } C_ { x e. B | ps } )