Theorem xrleidd 13161

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

Syntax hints:   → wi 4   ∈ wcel 2107   class class class wbr 5117  ℝ^*cxr 11261   ≤ cle 11263

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5264  ax-nul 5274  ax-pow 5333  ax-pr 5400  ax-un 7724  ax-cnex 11178  ax-resscn 11179  ax-pre-lttri 11196  ax-pre-lttrn 11197

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3414  df-v 3459  df-sbc 3764  df-csb 3873  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4882  df-br 5118  df-opab 5180  df-mpt 5200  df-id 5546  df-po 5559  df-so 5560  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-iota 6481  df-fun 6530  df-fn 6531  df-f 6532  df-f1 6533  df-fo 6534  df-f1o 6535  df-fv 6536  df-er 8714  df-en 8955  df-dom 8956  df-sdom 8957  df-pnf 11264  df-mnf 11265  df-xr 11266  df-ltxr 11267  df-le 11268

This theorem is referenced by:  xleadd1a  13262  supxrre  13336  infxrre  13345  ioounsn  13484  snunioo  13485  snunico  13486  limsupgre  15486  limsupbnd1  15487  limsupbnd2  15488  pcdvdstr  16883  pcadd  16896  imasdsf1olem  24299  blssps  24350  blss  24351  blcld  24431  nmolb  24643  metds0  24777  metdstri  24778  metdseq0  24781  itg2eqa  25685  mdeglt  26009  deg1lt  26041  eliccelico  32691  elicoelioo  32692  difioo  32696  xrge0omnd  33016  ply1degltel  33539  ply1degleel  33540  ply1degltlss  33541  esumpmono  34039  signsply0  34512  iocinico  43168  xadd0ge  45282  infxrpnf  45407  monoordxrv  45442  iooiinioc  45519  icossico2  45527  limcresiooub  45607  liminflelimsupuz  45750  ismbl4  45958  sge0prle  46366  iunhoiioo  46641  iccpartleu  47368  iccpartgel  47369  iccdisj2  48765