Theorem 1e0p1 12670

Description: The successor of zero. (Contributed by Mario Carneiro, 18-Feb-2014.)

Assertion

Ref	Expression
1e0p1	⊢ 1 = (0 + 1)

Proof of Theorem 1e0p1

Step	Hyp	Ref	Expression
1		0p1e1 12282	. 2 ⊢ (0 + 1) = 1
2	1	eqcomi 2738	1 ⊢ 1 = (0 + 1)

Syntax hints:   = wceq 1540  (class class class)co 7370  0cc0 11047  1c1 11048   + caddc 11050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7692  ax-resscn 11104  ax-1cn 11105  ax-icn 11106  ax-addcl 11107  ax-addrcl 11108  ax-mulcl 11109  ax-mulrcl 11110  ax-mulcom 11111  ax-addass 11112  ax-mulass 11113  ax-distr 11114  ax-i2m1 11115  ax-1ne0 11116  ax-1rid 11117  ax-rnegex 11118  ax-rrecex 11119  ax-cnre 11120  ax-pre-lttri 11121  ax-pre-lttrn 11122  ax-pre-ltadd 11123

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6453  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7373  df-er 8649  df-en 8897  df-dom 8898  df-sdom 8899  df-pnf 11189  df-mnf 11190  df-ltxr 11192

This theorem is referenced by:  6p5e11  12701  7p4e11  12704  8p3e11  12709  9p2e11  12715  fz1ssfz0  13563  fz0to3un2pr  13569  fzo01  13687  fz01pr  13691  bcp1nk  14261  pfx1  14646  arisum2  15805  ege2le3  16034  ef4p  16059  efgt1p2  16060  efgt1p  16061  bitsmod  16384  prmdiv  16733  prmreclem2  16866  vdwap1  16926  11prm  17063  631prm  17075  mulgnn0p1  19001  gsummptfzsplitl  19849  itgcnlem  25726  dveflem  25918  ply1rem  26106  vieta1lem2  26254  vieta1  26255  pserdvlem2  26373  pserdv2  26375  abelthlem6  26381  abelthlem9  26385  cosne0  26473  logf1o2  26594  logtayl  26604  ang180lem3  26756  birthdaylem2  26897  ftalem5  27022  ppi2  27115  ppiublem2  27149  ppiub  27150  bclbnd  27226  bposlem2  27231  lgsdir2lem3  27273  lgseisenlem1  27321  axlowdimlem13  28936  spthispth  29706  uhgrwkspthlem2  29736  cyclnumvtx  29782  upgr3v3e3cycl  30161  upgr4cycl4dv4e  30166  ballotlemii  34490  ballotlem1c  34494  subfacval2  35169  cvmliftlem5  35271  aks6d1c5lem1  42119  sticksstones11  42139  sticksstones12  42141  3cubeslem1  42667  halffl  45289  sinaover2ne0  45861  stoweidlem11  46004  stoweidlem13  46006  stirlinglem7  46073  fourierdlem48  46147  fourierdlem49  46148  fourierdlem69  46168  fourierdlem79  46178  fourierdlem93  46192  etransclem7  46234  etransclem25  46252  etransclem26  46253  etransclem37  46264  tworepnotupword  46879  iccpartlt  47420  31prm  47593  gpgprismgr4cycllem3  48082  1odd  48154  itcoval1  48647  ackval1  48665  ackval41a  48678