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

Definition df-2o 7150
Description: Define the ordinal number 2. (Contributed by NM, 18-Feb-2004.)
Assertion
Ref Expression
df-2o

Detailed syntax breakdown of Definition df-2o
StepHypRef Expression
1 c2o 7143 . 2
2 c1o 7142 . . 3
32csuc 4885 . 2
41, 3wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  2on  7157  2on0  7158  df2o3  7162  ondif2  7171  o1p1e2  7209  oneo  7249  2onn  7308  nnm2  7317  nnneo  7319  nneob  7320  snnen2o  7726  1sdom2  7738  1sdom  7742  en2  7776  pm54.43  8402  en2eleq  8407  en2other2  8408  infxpenc  8416  infxpenc2  8420  infxpencOLD  8421  infxpenc2OLD  8424  pm110.643ALT  8579  fin1a2lem4  8804  cfpwsdom  8980  canthp1lem2  9052  pwxpndom2  9064  tsk2  9164  hash2  12470  f1otrspeq  16472  pmtrf  16480  pmtrmvd  16481  pmtrfinv  16486  efgmnvl  16732  isnzr2  17911  sltval2  29416  nosgnn0  29418  sltsolem1  29428  pw2f1ocnv  30979  pwfi2f1o  31044  bj-2ex  34508
  Copyright terms: Public domain W3C validator