Theorem dfrab3ss

Description: Restricted class abstraction with a common superset. (Contributed by Stefan O'Rear, 12-Sep-2015) (Proof shortened by Mario Carneiro, 8-Nov-2015)

	Ref	Expression
Assertion	dfrab3ss	$$⊢A\subseteq B\to \left\{x\in A|\phi \right\}=A\cap \left\{x\in B|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-ss	$$⊢A\subseteq B\leftrightarrow A\cap B=A$$
2		ineq1	$$⊢A\cap B=A\to \left(A\cap B\right)\cap \left\{x|\phi \right\}=A\cap \left\{x|\phi \right\}$$
3	2	eqcomd	$$⊢A\cap B=A\to A\cap \left\{x|\phi \right\}=\left(A\cap B\right)\cap \left\{x|\phi \right\}$$
4	1 3	sylbi	$$⊢A\subseteq B\to A\cap \left\{x|\phi \right\}=\left(A\cap B\right)\cap \left\{x|\phi \right\}$$
5		dfrab3	$$⊢\left\{x\in A|\phi \right\}=A\cap \left\{x|\phi \right\}$$
6		dfrab3	$$⊢\left\{x\in B|\phi \right\}=B\cap \left\{x|\phi \right\}$$
7	6	ineq2i	$$⊢A\cap \left\{x\in B|\phi \right\}=A\cap \left(B\cap \left\{x|\phi \right\}\right)$$
8		inass	$$⊢\left(A\cap B\right)\cap \left\{x|\phi \right\}=A\cap \left(B\cap \left\{x|\phi \right\}\right)$$
9	7 8	eqtr4i	$$⊢A\cap \left\{x\in B|\phi \right\}=\left(A\cap B\right)\cap \left\{x|\phi \right\}$$
10	4 5 9	3eqtr4g	$$⊢A\subseteq B\to \left\{x\in A|\phi \right\}=A\cap \left\{x\in B|\phi \right\}$$