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

Theorem leidd 9526
Description: 'Less than or equal to' is reflexive. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
leidd.1  |-  ( ph  ->  A  e.  RR )
Assertion
Ref Expression
leidd  |-  ( ph  ->  A  <_  A )

Proof of Theorem leidd
StepHypRef Expression
1 leidd.1 . 2  |-  ( ph  ->  A  e.  RR )
2 leid 9103 . 2  |-  ( A  e.  RR  ->  A  <_  A )
31, 2syl 16 1  |-  ( ph  ->  A  <_  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   class class class wbr 4154   RRcr 8923    <_ cle 9055
This theorem is referenced by:  zextle  10276  uzind  10294  uzid  10433  ifle  10716  supxrre  10839  infmxrre  10847  injresinjlem  11127  flid  11144  modabs2  11203  monoord  11281  leexp2r  11365  facwordi  11508  faclbnd6  11518  iseraltlem2  12404  climcndslem1  12557  cvgrat  12588  eirrlem  12731  ruclem2  12759  ruclem9  12765  sadcaddlem  12897  nn0seqcvgd  12989  eulerthlem2  13099  pcidlem  13173  pc2dvds  13180  pcprmpw2  13183  pcmpt  13189  ramub1lem2  13323  pgpfi  15167  psrridm  16396  zntoslem  16761  methaus  18441  nmoid  18648  xrsxmet  18712  reconnlem1  18729  metdstri  18753  nmoleub3  18999  ovolctb  19254  ovolicc1  19280  volcn  19366  mbflimsup  19426  mbfi1fseqlem4  19478  itg2const2  19501  itg2uba  19503  itg2splitlem  19508  itg2cnlem1  19521  itg2cnlem2  19522  iblss  19564  itgless  19576  itgsplitioo  19597  dvge0  19758  dvcvx  19772  dvfsumlem2  19779  dvfsumlem3  19780  dvfsumrlim  19783  coe1mul4  19891  deg1mul2  19905  ply1divex  19927  deg1submon1p  19943  coe1termlem  20044  dgradd2  20054  dgrco  20061  aaliou3lem2  20128  abelth2  20226  jensen  20695  logexprlim  20877  bcmono  20929  bcmax  20930  dchrisum0flblem1  21070  pntleml  21173  wlkonwlk  21400  cyclnspth  21467  eupath2  21551  blocnilem  22154  dstfrvunirn  24512  ballotlemsi  24552  itg2addnclem  25958  itg2addnc  25960  itg2gt0cn  25961  ssbnd  26189  bfplem1  26223  acongeq  26740  expdiophlem1  26784  hbt  27004  fmul01  27379  fmul01lt1lem1  27383  stoweidlem20  27438  stoweidlem51  27469  wallispilem3  27485
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369  ax-sep 4272  ax-nul 4280  ax-pow 4319  ax-pr 4345  ax-un 4642  ax-resscn 8981  ax-pre-lttri 8998
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2243  df-mo 2244  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ne 2553  df-nel 2554  df-ral 2655  df-rex 2656  df-rab 2659  df-v 2902  df-sbc 3106  df-csb 3196  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-nul 3573  df-if 3684  df-pw 3745  df-sn 3764  df-pr 3765  df-op 3767  df-uni 3959  df-br 4155  df-opab 4209  df-mpt 4210  df-id 4440  df-xp 4825  df-rel 4826  df-cnv 4827  df-co 4828  df-dm 4829  df-rn 4830  df-res 4831  df-ima 4832  df-iota 5359  df-fun 5397  df-fn 5398  df-f 5399  df-f1 5400  df-fo 5401  df-f1o 5402  df-fv 5403  df-er 6842  df-en 7047  df-dom 7048  df-sdom 7049  df-pnf 9056  df-mnf 9057  df-xr 9058  df-ltxr 9059  df-le 9060
  Copyright terms: Public domain W3C validator