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