Theorem xrleidd 13144

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

Syntax hints:   → wi 4   ∈ wcel 2136   class class class wbr 5094  ℝ^*cxr 11205   ≤ cle 11207

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-10 2169  ax-11 2185  ax-12 2206  ax-ext 2728  ax-sep 5240  ax-nul 5250  ax-pow 5316  ax-pr 5384  ax-un 7707  ax-cnex 11119  ax-resscn 11120  ax-pre-lttri 11137  ax-pre-lttrn 11138

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3or 1096  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-nf 1798  df-sb 2085  df-mo 2560  df-eu 2590  df-clab 2735  df-cleq 2748  df-clel 2831  df-nfc 2905  df-ne 2952  df-nel 3056  df-ral 3071  df-rex 3081  df-rab 3409  df-v 3450  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4475  df-pw 4551  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-opab 5157  df-mpt 5176  df-id 5535  df-po 5548  df-so 5549  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-iota 6466  df-fun 6512  df-fn 6513  df-f 6514  df-f1 6515  df-fo 6516  df-f1o 6517  df-fv 6518  df-er 8666  df-en 8917  df-dom 8918  df-sdom 8919  df-pnf 11208  df-mnf 11209  df-xr 11210  df-ltxr 11211  df-le 11212

This theorem is referenced by:  xleadd1a  13246  supxrre  13320  infxrre  13330  icossico2d  13415  ioounsn  13471  snunioo  13472  snunico  13473  limsupgre  15484  limsupbnd1  15485  limsupbnd2  15486  pcdvdstr  16888  pcadd  16901  xrge0omnd  21470  imasdsf1olem  24406  blssps  24457  blss  24458  blcld  24538  nmolb  24750  metds0  24884  metdstri  24885  metdseq0  24888  itg2eqa  25780  mdeglt  26098  deg1lt  26130  eliccelico  32922  elicoelioo  32923  difioo  32927  ply1degltel  33744  ply1degleel  33745  ply1degltlss  33746  esumpmono  34330  signsply0  34802  iocinico  43737  xadd0ge  45846  infxrpnf  45968  monoordxrv  46003  iooiinioc  46080  limcresiooub  46164  liminflelimsupuz  46307  ismbl4  46515  sge0prle  46923  iunhoiioo  47198  iccpartleu  47982  iccpartgel  47983  iccdisj2  49466