Theorem rabss3d

Description: Subclass law for restricted abstraction. (Contributed by Thierry Arnoux, 25-Sep-2017)

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

Proof

Step	Hyp	Ref	Expression
1		rabss3d.1	$$⊢\left(\phi \wedge \left(x\in A\wedge \psi \right)\right)\to x\in B$$
2		nfv	$$⊢Ⅎx\phi$$
3		nfrab1	$$⊢\underset{\_}{Ⅎ}x\left\{x\in A|\psi \right\}$$
4		nfrab1	$$⊢\underset{\_}{Ⅎ}x\left\{x\in B|\psi \right\}$$
5		simprr	$$⊢\left(\phi \wedge \left(x\in A\wedge \psi \right)\right)\to \psi$$
6	1 5	jca	$$⊢\left(\phi \wedge \left(x\in A\wedge \psi \right)\right)\to \left(x\in B\wedge \psi \right)$$
7	6	ex	$$⊢\phi \to \left(\left(x\in A\wedge \psi \right)\to \left(x\in B\wedge \psi \right)\right)$$
8		rabid	$$⊢x\in \left\{x\in A|\psi \right\}\leftrightarrow \left(x\in A\wedge \psi \right)$$
9		rabid	$$⊢x\in \left\{x\in B|\psi \right\}\leftrightarrow \left(x\in B\wedge \psi \right)$$
10	7 8 9	3imtr4g	$$⊢\phi \to \left(x\in \left\{x\in A|\psi \right\}\to x\in \left\{x\in B|\psi \right\}\right)$$
11	2 3 4 10	ssrd	$$⊢\phi \to \left\{x\in A|\psi \right\}\subseteq \left\{x\in B|\psi \right\}$$