MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  onirri Structured version   Visualization version   GIF version

Theorem onirri 6046
Description: An ordinal number is not a member of itself. Theorem 7M(c) of [Enderton] p. 192. (Contributed by NM, 11-Jun-1994.)
Hypothesis
Ref Expression
on.1 𝐴 ∈ On
Assertion
Ref Expression
onirri ¬ 𝐴𝐴

Proof of Theorem onirri
StepHypRef Expression
1 on.1 . . 3 𝐴 ∈ On
21onordi 6044 . 2 Ord 𝐴
3 ordirr 5958 . 2 (Ord 𝐴 → ¬ 𝐴𝐴)
42, 3ax-mp 5 1 ¬ 𝐴𝐴
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wcel 2157  Ord word 5939  Oncon0 5940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2776  ax-sep 4974  ax-nul 4982  ax-pr 5096
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2785  df-cleq 2791  df-clel 2794  df-nfc 2929  df-ne 2971  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3386  df-sbc 3633  df-dif 3771  df-un 3773  df-in 3775  df-ss 3782  df-nul 4115  df-if 4277  df-sn 4368  df-pr 4370  df-op 4374  df-uni 4628  df-br 4843  df-opab 4905  df-tr 4945  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-ord 5943  df-on 5944
This theorem is referenced by:  onssnel2i  6050  onuninsuci  7273  oelim2  7914  omopthlem2  7975  harndom  8710  wfelirr  8937  carduni  9092  pm54.43  9111  alephle  9196  alephfp  9216  pwxpndom2  9774  onsucsuccmpi  32943  onint1  32949  finxpreclem5  33723  wepwsolem  38386
  Copyright terms: Public domain W3C validator