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\cap C$$
	abeqinbi.2	$$⊢B=\left\{x|\phi \right\}$$
	abeqinbi.3	$$⊢x\in C\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	abeqinbi	$$⊢A=\left\{x\in C|\psi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		abeqinbi.1	$$⊢A=B\cap C$$
2		abeqinbi.2	$$⊢B=\left\{x|\phi \right\}$$
3		abeqinbi.3	$$⊢x\in C\to \left(\phi \leftrightarrow \psi \right)$$
4	1 2	abeqin	$$⊢A=\left\{x\in C|\phi \right\}$$
5	4 3	rabimbieq	$$⊢A=\left\{x\in C|\psi \right\}$$