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

Metamath Proof Explorer

Theorem disjprsn

Description: The disjoint intersection of an unordered pair and a singleton. (Contributed by AV, 23-Jan-2021)

Ref Expression
Assertion disjprsn ⊢ A ≠ C ∧ B ≠ C → A B ∩ C = ∅

Proof

Step Hyp Ref Expression
1 dfsn2 ⊢ C = C C
2 1 ineq2i ⊢ A B ∩ C = A B ∩ C C
3 disjpr2 ⊢ A ≠ C ∧ B ≠ C ∧ A ≠ C ∧ B ≠ C → A B ∩ C C = ∅
4 3 anidms ⊢ A ≠ C ∧ B ≠ C → A B ∩ C C = ∅
5 2 4 eqtrid ⊢ A ≠ C ∧ B ≠ C → A B ∩ C = ∅