Theorem abeqin

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

	Ref	Expression
Hypotheses	abeqin.1	|- A = ( B i^i C )
	abeqin.2	|- B = { x | ph }
Assertion	abeqin	|- A = { x e. C | ph }

Proof

Step	Hyp	Ref	Expression
1		abeqin.1	|- A = ( B i^i C )
2		abeqin.2	|- B = { x | ph }
3	2	ineq1i	|- ( B i^i C ) = ( { x | ph } i^i C )
4		dfrab2	|- { x e. C | ph } = ( { x | ph } i^i C )
5	3 1 4	3eqtr4i	|- A = { x e. C | ph }