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