Theorem bj-inrab3

Description: Generalization of dfrab3ss , which it may shorten. (Contributed by BJ, 21-Apr-2019) (Revised by OpenAI, 7-Jul-2020)

	Ref	Expression
Assertion	bj-inrab3	$$⊢A\cap \left\{x\in B|\phi \right\}=\left\{x\in A|\phi \right\}\cap B$$

Proof

Step	Hyp	Ref	Expression
1		dfrab3	$$⊢\left\{x\in B|\phi \right\}=B\cap \left\{x|\phi \right\}$$
2	1	ineq2i	$$⊢A\cap \left\{x\in B|\phi \right\}=A\cap \left(B\cap \left\{x|\phi \right\}\right)$$
3		dfrab3	$$⊢\left\{x\in A|\phi \right\}=A\cap \left\{x|\phi \right\}$$
4	3	ineq2i	$$⊢B\cap \left\{x\in A|\phi \right\}=B\cap \left(A\cap \left\{x|\phi \right\}\right)$$
5		incom	$$⊢\left\{x\in A|\phi \right\}\cap B=B\cap \left\{x\in A|\phi \right\}$$
6		in12	$$⊢A\cap \left(B\cap \left\{x|\phi \right\}\right)=B\cap \left(A\cap \left\{x|\phi \right\}\right)$$
7	4 5 6	3eqtr4i	$$⊢\left\{x\in A|\phi \right\}\cap B=A\cap \left(B\cap \left\{x|\phi \right\}\right)$$
8	2 7	eqtr4i	$$⊢A\cap \left\{x\in B|\phi \right\}=\left\{x\in A|\phi \right\}\cap B$$