Theorem ssrabf

Description: Subclass of a restricted class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	ssrabf.1	$$⊢\underset{\_}{Ⅎ}xB$$
	ssrabf.2	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	ssrabf	$$⊢B\subseteq \left\{x\in A|\phi \right\}\leftrightarrow \left(B\subseteq A\wedge \forall x\in B\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ssrabf.1	$$⊢\underset{\_}{Ⅎ}xB$$
2		ssrabf.2	$$⊢\underset{\_}{Ⅎ}xA$$
3		df-rab	$$⊢\left\{x\in A|\phi \right\}=\left\{x|\left(x\in A\wedge \phi \right)\right\}$$
4	3	sseq2i	$$⊢B\subseteq \left\{x\in A|\phi \right\}\leftrightarrow B\subseteq \left\{x|\left(x\in A\wedge \phi \right)\right\}$$
5	1	ssabf	$$⊢B\subseteq \left\{x|\left(x\in A\wedge \phi \right)\right\}\leftrightarrow \forall x\left(x\in B\to \left(x\in A\wedge \phi \right)\right)$$
6	1 2	dfss3f	$$⊢B\subseteq A\leftrightarrow \forall x\in Bx\in A$$
7	6	anbi1i	$$⊢\left(B\subseteq A\wedge \forall x\in B\phi \right)\leftrightarrow \left(\forall x\in Bx\in A\wedge \forall x\in B\phi \right)$$
8		r19.26	$$⊢\forall x\in B\left(x\in A\wedge \phi \right)\leftrightarrow \left(\forall x\in Bx\in A\wedge \forall x\in B\phi \right)$$
9		df-ral	$$⊢\forall x\in B\left(x\in A\wedge \phi \right)\leftrightarrow \forall x\left(x\in B\to \left(x\in A\wedge \phi \right)\right)$$
10	7 8 9	3bitr2ri	$$⊢\forall x\left(x\in B\to \left(x\in A\wedge \phi \right)\right)\leftrightarrow \left(B\subseteq A\wedge \forall x\in B\phi \right)$$
11	4 5 10	3bitri	$$⊢B\subseteq \left\{x\in A|\phi \right\}\leftrightarrow \left(B\subseteq A\wedge \forall x\in B\phi \right)$$