Theorem rabssd

Description: Restricted class abstraction in a subclass relationship. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	rabssd.1	|- F/ x ph
	rabssd.2	|- F/_ x B
	rabssd.3	|- ( ( ph /\ x e. A /\ ch ) -> x e. B )
Assertion	rabssd	|- ( ph -> { x e. A | ch } C_ B )

Proof

Step	Hyp	Ref	Expression
1		rabssd.1	|- F/ x ph
2		rabssd.2	|- F/_ x B
3		rabssd.3	|- ( ( ph /\ x e. A /\ ch ) -> x e. B )
4	3	3exp	|- ( ph -> ( x e. A -> ( ch -> x e. B ) ) )
5	1 4	ralrimi	|- ( ph -> A. x e. A ( ch -> x e. B ) )
6	2	rabssf	|- ( { x e. A | ch } C_ B <-> A. x e. A ( ch -> x e. B ) )
7	5 6	sylibr	|- ( ph -> { x e. A | ch } C_ B )