Theorem xrleidd 13092

Description: 'Less than or equal to' is reflexive for extended reals. Deduction form of xrleid 13091. (Contributed by Glauco Siliprandi, 26-Jun-2021.)

Hypothesis

Ref	Expression
xrleidd.1	⊢ (𝜑 → 𝐴 ∈ ℝ*)

Assertion

Ref	Expression
xrleidd	⊢ (𝜑 → 𝐴 ≤ 𝐴)

Proof of Theorem xrleidd

Step	Hyp	Ref	Expression
1		xrleidd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
2		xrleid 13091	. 2 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐴 ≤ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5086  ℝ^*cxr 11167   ≤ cle 11169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368  ax-un 7680  ax-cnex 11083  ax-resscn 11084  ax-pre-lttri 11101  ax-pre-lttrn 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-po 5530  df-so 5531  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174

This theorem is referenced by:  xleadd1a  13194  supxrre  13268  infxrre  13278  icossico2d  13363  ioounsn  13419  snunioo  13420  snunico  13421  limsupgre  15432  limsupbnd1  15433  limsupbnd2  15434  pcdvdstr  16836  pcadd  16849  xrge0omnd  21433  imasdsf1olem  24347  blssps  24398  blss  24399  blcld  24479  nmolb  24691  metds0  24825  metdstri  24826  metdseq0  24829  itg2eqa  25721  mdeglt  26042  deg1lt  26074  eliccelico  32870  elicoelioo  32871  difioo  32875  ply1degltel  33674  ply1degleel  33675  ply1degltlss  33676  esumpmono  34244  signsply0  34716  iocinico  43655  xadd0ge  45767  infxrpnf  45889  monoordxrv  45924  iooiinioc  46001  limcresiooub  46085  liminflelimsupuz  46228  ismbl4  46436  sge0prle  46844  iunhoiioo  47119  iccpartleu  47885  iccpartgel  47886  iccdisj2  49369