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

Theorem leidd 10207
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 9754 . 2  |-  ( A  e.  RR  ->  A  <_  A )
31, 2syl 17 1  |-  ( ph  ->  A  <_  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1897   class class class wbr 4415   RRcr 9563    <_ cle 9701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609  ax-resscn 9621  ax-pre-lttri 9638
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-nel 2635  df-ral 2753  df-rex 2754  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-op 3986  df-uni 4212  df-br 4416  df-opab 4475  df-mpt 4476  df-id 4767  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-er 7388  df-en 7595  df-dom 7596  df-sdom 7597  df-pnf 9702  df-mnf 9703  df-xr 9704  df-ltxr 9705  df-le 9706
This theorem is referenced by:  zextle  11037  uzind  11055  uzid  11201  ifle  11518  supxrre  11641  infxrre  11650  infmxrreOLD  11654  nn0fz0  11918  fvinim0ffz  12054  flid  12075  modabs2  12162  monoord  12274  leexp2r  12361  facwordi  12505  faclbnd6  12515  2swrdeqwrdeq  12845  swrdccatid  12889  repswcshw  12947  iseraltlem2  13797  climcndslem1  13955  cvgrat  13987  eirrlem  14304  ruclem2  14332  ruclem9  14338  sadcaddlem  14479  nn0seqcvgd  14577  eulerthlem2  14778  pcidlem  14869  pc2dvds  14876  pcprmpw2  14879  pcmpt  14885  ramub1lem2  15033  prmolefac  15052  prmorlefacOLD  15066  prmgaplem4  15072  pgpfi  17305  psrridm  18676  zntoslem  19175  methaus  21583  nmoid  21811  xrsxmet  21875  reconnlem1  21892  metdstri  21916  metdstriOLD  21931  nmoleub3  22181  ovolctb  22491  ovolicc1  22517  volcn  22612  mbflimsup  22671  mbflimsupOLD  22672  mbfi1fseqlem4  22724  itg2const2  22747  itg2uba  22749  itg2splitlem  22754  itg2cnlem1  22767  itg2cnlem2  22768  iblss  22810  itgless  22822  itgsplitioo  22843  dvge0  23006  dvcvx  23020  dvfsumlem2  23027  dvfsumlem3  23028  dvfsumrlim  23031  coe1mul4  23097  deg1mul2  23111  ply1divex  23135  deg1submon1p  23151  coe1termlem  23260  dgradd2  23270  dgrco  23277  aaliou3lem2  23347  abelth2  23445  jensen  23962  logexprlim  24201  bcmono  24253  bcmax  24254  dchrisum0flblem1  24394  pntleml  24497  wlkonwlk  25313  cyclnspth  25407  eupath2  25756  blocnilem  26493  fiunelros  29044  dstfrvunirn  29355  ballotlemsi  29395  ballotlemsiOLD  29433  relowlssretop  31810  poimirlem28  32012  mblfinlem2  32022  itg2addnclem  32037  itg2gt0cn  32041  ftc1anclem7  32067  ftc1anclem8  32068  ftc1anc  32069  ssbnd  32164  bfplem1  32198  acongeq  35877  expdiophlem1  35920  hbt  36033  dvgrat  36704  fmul01  37695  fmul01lt1lem1  37699  limciccioolb  37738  ioccncflimc  37800  icocncflimc  37804  cncfiooicclem1  37808  dvnmul  37855  iblspltprt  37887  itgspltprt  37893  stoweidlem20  37917  stoweidlem51  37949  wallispilem3  37966  fourierdlem10  38016  fourierdlem11  38017  fourierdlem14  38020  fourierdlem17  38023  fourierdlem32  38039  fourierdlem33  38040  fourierdlem41  38048  fourierdlem46  38053  fourierdlem48  38055  fourierdlem49  38056  fourierdlem50  38057  fourierdlem73  38080  fourierdlem76  38083  fourierdlem79  38086  fourierdlem93  38100  fourierdlem102  38109  fourierdlem103  38110  fourierdlem104  38111  fourierdlem107  38114  fourierdlem111  38118  fourierdlem114  38121  etransclem23  38159  hsphoidmvle2  38444  hsphoidmvle  38445  hoidmv1lelem1  38450  hoidmv1lelem2  38451  hoidmv1lelem3  38452  hoidmvlelem1  38454  hoidifhspdmvle  38479  bgoldbachlt  38943  pfxsuffeqwrdeq  38986  2leaddle2  39085  logbpw2m1  40650  fllog2  40651  dignn0ldlem  40685
  Copyright terms: Public domain W3C validator