Metamath Proof Explorer

Theorem onirri

Description: An ordinal number is not a member of itself. Theorem 7M(c) of Enderton p. 192. (Contributed by NM, 11-Jun-1994)

Ref Expression
Hypothesis on.1 
|- A e. On
Assertion onirri 
|- -. A e. A

Proof

Step Hyp Ref Expression
1 on.1 
 |-  A e. On
2 1 onordi 
 |-  Ord A
3 ordirr 
 |-  ( Ord A -> -. A e. A )
4 2 3 ax-mp 
 |-  -. A e. A