Theorem ssrabdf

Description: Subclass of a restricted class abstraction (deduction form). (Contributed by Glauco Siliprandi, 5-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		ssrabdf.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		ssrabdf.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		ssrabdf.3	$$⊢Ⅎx\phi$$
4		ssrabdf.4	$$⊢\phi \to B\subseteq A$$
5		ssrabdf.5	$$⊢\left(\phi \wedge x\in B\right)\to \psi$$
6	3 5	ralrimia	$$⊢\phi \to \forall x\in B\psi$$
7	2 1	ssrabf	$$⊢B\subseteq \left\{x\in A|\psi \right\}\leftrightarrow \left(B\subseteq A\wedge \forall x\in B\psi \right)$$
8	4 6 7	sylanbrc	$$⊢\phi \to B\subseteq \left\{x\in A|\psi \right\}$$