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

Theorem df2o3 7162
Description: Expanded value of the ordinal number 2. (Contributed by Mario Carneiro, 14-Aug-2015.)
Assertion
Ref Expression
df2o3

Proof of Theorem df2o3
StepHypRef Expression
1 df-2o 7150 . 2
2 df-suc 4889 . 2
3 df1o2 7161 . . . 4
43uneq1i 3653 . . 3
5 df-pr 4032 . . 3
64, 5eqtr4i 2489 . 2
71, 2, 63eqtri 2490 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  u.cun 3473   c0 3784  {csn 4029  {cpr 4031  succsuc 4885   c1o 7142   c2o 7143
This theorem is referenced by:  df2o2  7163  2oconcl  7172  map2xp  7707  1sdom  7742  cantnflem2  8130  xp2cda  8581  sdom2en01  8703  sadcf  14103  xpscfn  14956  xpscfv  14959  xpsfrnel  14960  xpsfeq  14961  xpsfrnel2  14962  xpsle  14978  setcepi  15415  efgi0  16738  efgi1  16739  vrgpf  16786  vrgpinv  16787  frgpuptinv  16789  frgpup2  16794  frgpup3lem  16795  frgpnabllem1  16877  dmdprdpr  17098  dprdpr  17099  xpstopnlem1  20310  xpstopnlem2  20312  xpsxmetlem  20882  xpsdsval  20884  xpsmet  20885  onint1  29914  pw2f1ocnv  30979  wepwsolem  30987
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-dif 3478  df-un 3480  df-nul 3785  df-pr 4032  df-suc 4889  df-1o 7149  df-2o 7150
  Copyright terms: Public domain W3C validator