Theorem abeqinbi

Description: Intersection with class abstraction and equivalent wff's. (Contributed by Peter Mazsa, 21-Jul-2021)

	Ref	Expression
Hypotheses	abeqinbi.1	|- A = ( B i^i C )
	abeqinbi.2	|- B = { x | ph }
	abeqinbi.3	|- ( x e. C -> ( ph <-> ps ) )
Assertion	abeqinbi	|- A = { x e. C | ps }

Proof

Step	Hyp	Ref	Expression
1		abeqinbi.1	|- A = ( B i^i C )
2		abeqinbi.2	|- B = { x | ph }
3		abeqinbi.3	|- ( x e. C -> ( ph <-> ps ) )
4	1 2	abeqin	|- A = { x e. C | ph }
5	4 3	rabimbieq	|- A = { x e. C | ps }