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

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 } )