This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ 𝐴 = { 𝑥 ∈ 𝐶 ∣ 𝜓 }