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 ⊢ A = B ∩ C
abeqinbi.2 ⊢ B = x | φ
abeqinbi.3 ⊢ x ∈ C → φ ↔ ψ
Assertion abeqinbi ⊢ A = x ∈ C | ψ

Proof

Step Hyp Ref Expression
1 abeqinbi.1 ⊢ A = B ∩ C
2 abeqinbi.2 ⊢ B = x | φ
3 abeqinbi.3 ⊢ x ∈ C → φ ↔ ψ
4 1 2 abeqin ⊢ A = x ∈ C | φ
5 4 3 rabimbieq ⊢ A = x ∈ C | ψ