Theorem abeqinbi

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

	Ref	Expression
Hypotheses	abeqinbi.1	⊢ 𝐴 = ( 𝐵 ∩ 𝐶 )
	abeqinbi.2	⊢ 𝐵 = { 𝑥 ∣ 𝜑 }
	abeqinbi.3	⊢ ( 𝑥 ∈ 𝐶 → ( 𝜑 ↔ 𝜓 ) )
Assertion	abeqinbi	⊢ 𝐴 = { 𝑥 ∈ 𝐶 ∣ 𝜓 }

Proof

Step	Hyp	Ref	Expression
1		abeqinbi.1	⊢ 𝐴 = ( 𝐵 ∩ 𝐶 )
2		abeqinbi.2	⊢ 𝐵 = { 𝑥 ∣ 𝜑 }
3		abeqinbi.3	⊢ ( 𝑥 ∈ 𝐶 → ( 𝜑 ↔ 𝜓 ) )
4	1 2	abeqin	⊢ 𝐴 = { 𝑥 ∈ 𝐶 ∣ 𝜑 }
5	4 3	rabimbieq	⊢ 𝐴 = { 𝑥 ∈ 𝐶 ∣ 𝜓 }