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

Metamath Proof Explorer

Theorem abeqin

Description: Intersection with class abstraction. (Contributed by Peter Mazsa, 21-Jul-2021)

Ref Expression
Hypotheses abeqin.1 ⊢ A = B ∩ C
abeqin.2 ⊢ B = x | φ
Assertion abeqin ⊢ A = x ∈ C | φ

Proof

Step Hyp Ref Expression
1 abeqin.1 ⊢ A = B ∩ C
2 abeqin.2 ⊢ B = x | φ
3 2 ineq1i ⊢ B ∩ C = x | φ ∩ C
4 dfrab2 ⊢ x ∈ C | φ = x | φ ∩ C
5 3 1 4 3eqtr4i ⊢ A = x ∈ C | φ