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 ⊢ 𝐴 = ( 𝐵 ∩ 𝐶 )
abeqin.2 ⊢ 𝐵 = { 𝑥 ∣ 𝜑 }
Assertion abeqin 𝐴 = { 𝑥 ∈ 𝐶 ∣ 𝜑 }

Proof

Step Hyp Ref Expression
1 abeqin.1 ⊢ 𝐴 = ( 𝐵 ∩ 𝐶 )
2 abeqin.2 ⊢ 𝐵 = { 𝑥 ∣ 𝜑 }
3 2 ineq1i ⊢ ( 𝐵 ∩ 𝐶 ) = ( { 𝑥 ∣ 𝜑 } ∩ 𝐶 )
4 dfrab2 ⊢ { 𝑥 ∈ 𝐶 ∣ 𝜑 } = ( { 𝑥 ∣ 𝜑 } ∩ 𝐶 )
5 3 1 4 3eqtr4i ⊢ 𝐴 = { 𝑥 ∈ 𝐶 ∣ 𝜑 }