Colors of
variables: wff
setvar class |
Syntax hints:
∈ wcel 2106 Vcvv 3474
∪ cun 3945 {cpr 4629
ℝcr 11105 +∞cpnf 11241 -∞cmnf 11242
ℝ*cxr 11243 |
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 1913
ax-6 1971 ax-7 2011 ax-8 2108
ax-9 2116 ax-ext 2703 ax-sep 5298 ax-nul 5305 ax-pr 5426 ax-un 7721 ax-cnex 11162 ax-resscn 11163 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-or 846 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-rab 3433 df-v 3476 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-sn 4628 df-pr 4630 df-uni 4908 df-xr 11248 |
This theorem is referenced by: ixxval
13328 ixxf
13330 ixxex
13331 limsuple
15418 limsuplt
15419 limsupbnd1
15422 prdsds
17406 letsr
18542 xrsbas
20953 xrsadd
20954 xrsmul
20955 xrsle
20957 xrs1mnd
20975 xrs10
20976 xrs1cmn
20977 xrge0subm
20978 xrge0cmn
20979 xrsds
20980 znle
21079 leordtval2
22707 lecldbas
22714 ispsmet
23801 isxmet
23821 imasdsf1olem
23870 blfvalps
23880 nmoffn
24219 nmofval
24222 xrsxmet
24316 xrge0gsumle
24340 xrge0tsms
24341 xrlimcnp
26462 xrge00
32174 xrge0tsmsd
32196 xrhval
32986 icof
43903 elicores
44232 fuzxrpmcn
44530 gsumge0cl
45073 ovnval2b
45254 volicorescl
45255 ovnsubaddlem1
45272 |