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
|- ( A i^i { A } ) = (/)

Proof

Step Hyp Ref Expression
1 elirr
 |-  -. A e. A
2 disjsn
 |-  ( ( A i^i { A } ) = (/) <-> -. A e. A )
3 1 2 mpbir
 |-  ( A i^i { A } ) = (/)