Theorem xrleidd 13070

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

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

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 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682  ax-cnex 11086  ax-resscn 11087  ax-pre-lttri 11104  ax-pre-lttrn 11105

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 3062  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176

This theorem is referenced by:  xleadd1a  13172  supxrre  13246  infxrre  13256  icossico2d  13341  ioounsn  13397  snunioo  13398  snunico  13399  limsupgre  15408  limsupbnd1  15409  limsupbnd2  15410  pcdvdstr  16808  pcadd  16821  xrge0omnd  21404  imasdsf1olem  24321  blssps  24372  blss  24373  blcld  24453  nmolb  24665  metds0  24799  metdstri  24800  metdseq0  24803  itg2eqa  25706  mdeglt  26030  deg1lt  26062  eliccelico  32838  elicoelioo  32839  difioo  32843  ply1degltel  33656  ply1degleel  33657  ply1degltlss  33658  esumpmono  34217  signsply0  34689  iocinico  43490  xadd0ge  45603  infxrpnf  45726  monoordxrv  45761  iooiinioc  45838  limcresiooub  45922  liminflelimsupuz  46065  ismbl4  46273  sge0prle  46681  iunhoiioo  46956  iccpartleu  47710  iccpartgel  47711  iccdisj2  49178