Metamath Proof Explorer

Theorem neirr

Description: No class is unequal to itself. Inequality is irreflexive. (Contributed by Stefan O'Rear, 1-Jan-2015)

Ref Expression
Assertion neirr 
|- -. A =/= A

Proof

Step Hyp Ref Expression
1 eqid 
 |-  A = A
2 nne 
 |-  ( -. A =/= A <-> A = A )
3 1 2 mpbir 
 |-  -. A =/= A