MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2on Unicode version

Theorem 2on 7062
Description: Ordinal 2 is an ordinal number. (Contributed by NM, 18-Feb-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
Assertion
Ref Expression
2on

Proof of Theorem 2on
StepHypRef Expression
1 df-2o 7055 . 2
2 1on 7061 . . 3
32onsuci 6582 . 2
41, 3eqeltri 2538 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1758   con0 4836  succsuc 4838   c1o 7047   c2o 7048
This theorem is referenced by:  3on  7064  oneo  7154  infxpenc  8321  infxpenc2  8325  infxpencOLD  8326  infxpenc2OLD  8329  mappwen  8419  pwcdaen  8491  sdom2en01  8608  fin1a2lem4  8709  xpslem  14670  xpsadd  14673  xpsmul  14674  xpsvsca  14676  xpsle  14678  xpsmnd  15620  xpsgrp  15833  efgval  16375  efgtf  16380  frgpcpbl  16417  frgp0  16418  frgpeccl  16419  frgpadd  16421  frgpmhm  16423  vrgpf  16426  vrgpinv  16427  frgpupf  16431  frgpup1  16433  frgpup2  16434  frgpup3lem  16435  frgpnabllem1  16512  frgpnabllem2  16513  xpstopnlem1  19781  xpstps  19782  xpstopnlem2  19783  xpsxmetlem  20353  xpsdsval  20355  nofv  28254  sltres  28261  noxp2o  28264  nobndup  28297  ssoninhaus  28750  onint1  28751  pw2f1ocnv  29846  frlmpwfi  29913
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4530  ax-nul 4538  ax-pr 4648  ax-un 6505
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3083  df-sbc 3298  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3752  df-if 3906  df-pw 3978  df-sn 3994  df-pr 3996  df-tp 3998  df-op 4000  df-uni 4209  df-br 4410  df-opab 4468  df-tr 4503  df-eprel 4749  df-po 4758  df-so 4759  df-fr 4796  df-we 4798  df-ord 4839  df-on 4840  df-suc 4842  df-1o 7054  df-2o 7055
  Copyright terms: Public domain W3C validator