Theorem rabssrabd

Description: Subclass of a restricted class abstraction. (Contributed by AV, 4-Jun-2022)

	Ref	Expression
Hypotheses	rabssrabd.1	$$⊢\phi \to A\subseteq B$$
	rabssrabd.2	$$⊢\left(\phi \wedge \psi \wedge x\in A\right)\to \chi$$
Assertion	rabssrabd	$$⊢\phi \to \left\{x\in A|\psi \right\}\subseteq \left\{x\in B|\chi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		rabssrabd.1	$$⊢\phi \to A\subseteq B$$
2		rabssrabd.2	$$⊢\left(\phi \wedge \psi \wedge x\in A\right)\to \chi$$
3		3anan32	$$⊢\left(\phi \wedge \psi \wedge x\in A\right)\leftrightarrow \left(\left(\phi \wedge x\in A\right)\wedge \psi \right)$$
4	3 2	sylbir	$$⊢\left(\left(\phi \wedge x\in A\right)\wedge \psi \right)\to \chi$$
5	4	ex	$$⊢\left(\phi \wedge x\in A\right)\to \left(\psi \to \chi \right)$$
6	5	ss2rabdv	$$⊢\phi \to \left\{x\in A|\psi \right\}\subseteq \left\{x\in A|\chi \right\}$$
7		rabss2	$$⊢A\subseteq B\to \left\{x\in A|\chi \right\}\subseteq \left\{x\in B|\chi \right\}$$
8	1 7	syl	$$⊢\phi \to \left\{x\in A|\chi \right\}\subseteq \left\{x\in B|\chi \right\}$$
9	6 8	sstrd	$$⊢\phi \to \left\{x\in A|\psi \right\}\subseteq \left\{x\in B|\chi \right\}$$