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

Metamath Proof Explorer

Theorem ineqcom

Description: Two ways of expressing that two classes have a given intersection. This is often used when that given intersection is the empty set, in which case the statement displays two ways of expressing that two classes are disjoint (when C = (/) : ( ( A i^i B ) = (/) <-> ( B i^i A ) = (/) ) ). (Contributed by Peter Mazsa, 22-Mar-2017)

Ref Expression
Assertion ineqcom ⊢ A ∩ B = C ↔ B ∩ A = C

Proof

Step Hyp Ref Expression
1 incom ⊢ A ∩ B = B ∩ A
2 1 eqeq1i ⊢ A ∩ B = C ↔ B ∩ A = C