Theorem abeqin

Description: Intersection with class abstraction. (Contributed by Peter Mazsa, 21-Jul-2021)

	Ref	Expression
Hypotheses	abeqin.1	$$⊢A=B\cap C$$
	abeqin.2	$$⊢B=\left\{x|\phi \right\}$$
Assertion	abeqin	$$⊢A=\left\{x\in C|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		abeqin.1	$$⊢A=B\cap C$$
2		abeqin.2	$$⊢B=\left\{x|\phi \right\}$$
3	2	ineq1i	$$⊢B\cap C=\left\{x|\phi \right\}\cap C$$
4		dfrab2	$$⊢\left\{x\in C|\phi \right\}=\left\{x|\phi \right\}\cap C$$
5	3 1 4	3eqtr4i	$$⊢A=\left\{x\in C|\phi \right\}$$