Theorem rabssd

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

	Ref	Expression
Hypotheses	rabssd.1	$$⊢Ⅎx\phi$$
	rabssd.2	$$⊢\underset{\_}{Ⅎ}xB$$
	rabssd.3	$$⊢\left(\phi \wedge x\in A\wedge \chi \right)\to x\in B$$
Assertion	rabssd	$$⊢\phi \to \left\{x\in A|\chi \right\}\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		rabssd.1	$$⊢Ⅎx\phi$$
2		rabssd.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		rabssd.3	$$⊢\left(\phi \wedge x\in A\wedge \chi \right)\to x\in B$$
4	3	3exp	$$⊢\phi \to \left(x\in A\to \left(\chi \to x\in B\right)\right)$$
5	1 4	ralrimi	$$⊢\phi \to \forall x\in A\left(\chi \to x\in B\right)$$
6	2	rabssf	$$⊢\left\{x\in A|\chi \right\}\subseteq B\leftrightarrow \forall x\in A\left(\chi \to x\in B\right)$$
7	5 6	sylibr	$$⊢\phi \to \left\{x\in A|\chi \right\}\subseteq B$$