Theorem xrleidd 13098

Description: 'Less than or equal to' is reflexive for extended reals. Deduction form of xrleid 13097. (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 13097	. 2 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐴 ≤ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2121   class class class wbr 5075  ℝ^*cxr 11173   ≤ cle 11175

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682  ax-cnex 11089  ax-resscn 11090  ax-pre-lttri 11107  ax-pre-lttrn 11108

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-nel 3041  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5157  df-id 5516  df-po 5529  df-so 5530  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11176  df-mnf 11177  df-xr 11178  df-ltxr 11179  df-le 11180

This theorem is referenced by:  xleadd1a  13200  supxrre  13274  infxrre  13284  icossico2d  13369  ioounsn  13425  snunioo  13426  snunico  13427  limsupgre  15438  limsupbnd1  15439  limsupbnd2  15440  pcdvdstr  16842  pcadd  16855  xrge0omnd  21424  imasdsf1olem  24360  blssps  24411  blss  24412  blcld  24492  nmolb  24704  metds0  24838  metdstri  24839  metdseq0  24842  itg2eqa  25734  mdeglt  26052  deg1lt  26084  eliccelico  32873  elicoelioo  32874  difioo  32878  ply1degltel  33689  ply1degleel  33690  ply1degltlss  33691  esumpmono  34275  signsply0  34747  iocinico  43672  xadd0ge  45781  infxrpnf  45903  monoordxrv  45938  iooiinioc  46015  limcresiooub  46099  liminflelimsupuz  46242  ismbl4  46450  sge0prle  46858  iunhoiioo  47133  iccpartleu  47917  iccpartgel  47918  iccdisj2  49401