Metamath Proof Explorer


Theorem disjcsn

Description: A class is disjoint from its singleton. A consequence of regularity. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Revised by BJ, 4-Apr-2019)

Ref Expression
Assertion disjcsn ( 𝐴 ∩ { 𝐴 } ) = ∅

Proof

Step Hyp Ref Expression
1 elirr ¬ 𝐴𝐴
2 disjsn ( ( 𝐴 ∩ { 𝐴 } ) = ∅ ↔ ¬ 𝐴𝐴 )
3 1 2 mpbir ( 𝐴 ∩ { 𝐴 } ) = ∅