Theorem 1e0p1 12558

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 12174	. 2 ⊢ (0 + 1) = 1
2	1	eqcomi 2745	1 ⊢ 1 = (0 + 1)

Syntax hints:   = wceq 1540  (class class class)co 7316  0cc0 10950  1c1 10951   + caddc 10953

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5237  ax-nul 5244  ax-pow 5302  ax-pr 5366  ax-un 7629  ax-resscn 11007  ax-1cn 11008  ax-icn 11009  ax-addcl 11010  ax-addrcl 11011  ax-mulcl 11012  ax-mulrcl 11013  ax-mulcom 11014  ax-addass 11015  ax-mulass 11016  ax-distr 11017  ax-i2m1 11018  ax-1ne0 11019  ax-1rid 11020  ax-rnegex 11021  ax-rrecex 11022  ax-cnre 11023  ax-pre-lttri 11024  ax-pre-lttrn 11025  ax-pre-ltadd 11026

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3442  df-sbc 3726  df-csb 3842  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-nul 4267  df-if 4471  df-pw 4546  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4850  df-br 5087  df-opab 5149  df-mpt 5170  df-id 5506  df-po 5520  df-so 5521  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-ov 7319  df-er 8547  df-en 8783  df-dom 8784  df-sdom 8785  df-pnf 11090  df-mnf 11091  df-ltxr 11093

This theorem is referenced by:  6p5e11  12589  7p4e11  12592  8p3e11  12597  9p2e11  12603  fz1ssfz0  13431  fz0to3un2pr  13437  fzo01  13548  bcp1nk  14110  pfx1  14492  arisum2  15649  ege2le3  15875  ef4p  15898  efgt1p2  15899  efgt1p  15900  bitsmod  16219  prmdiv  16560  prmreclem2  16692  vdwap1  16752  11prm  16890  631prm  16902  mulgnn0p1  18788  gsummptfzsplitl  19606  itgcnlem  25034  dveflem  25223  ply1rem  25408  vieta1lem2  25551  vieta1  25552  pserdvlem2  25667  pserdv2  25669  abelthlem6  25675  abelthlem9  25679  cosne0  25765  logf1o2  25885  logtayl  25895  ang180lem3  26041  birthdaylem2  26182  ftalem5  26306  ppi2  26399  ppiublem2  26431  ppiub  26432  bclbnd  26508  bposlem2  26513  lgsdir2lem3  26555  lgseisenlem1  26603  axlowdimlem13  27455  spthispth  28226  uhgrwkspthlem2  28254  upgr3v3e3cycl  28676  upgr4cycl4dv4e  28681  ballotlemii  32606  ballotlem1c  32610  subfacval2  33284  cvmliftlem5  33386  sticksstones11  40341  sticksstones12  40343  metakunt24  40377  3cubeslem1  40727  halffl  43089  sinaover2ne0  43664  stoweidlem11  43807  stoweidlem13  43809  stirlinglem7  43876  fourierdlem48  43950  fourierdlem49  43951  fourierdlem69  43971  fourierdlem79  43981  fourierdlem93  43995  etransclem7  44037  etransclem25  44055  etransclem26  44056  etransclem37  44067  iccpartlt  45146  31prm  45319  1odd  45635  itcoval1  46279  ackval1  46297  ackval41a  46310  tworepnotupword  46791