Colors of
variables: wff
setvar class |
Syntax hints:
⊆ wss 3911 × cxp 5632
ℝcr 11055 ℝ*cxr 11193 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914
ax-6 1972 ax-7 2012 ax-8 2109
ax-9 2117 ax-ext 2704 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3446 df-un 3916 df-in 3918 df-ss 3928 df-opab 5169 df-xp 5640 df-xr 11198 |
This theorem is referenced by: ltrelxr
11221 xrsdsre
24189 ovolfioo
24847 ovolficc
24848 ovolficcss
24849 ovollb
24859 ovolicc2
24902 ovolfs2
24951 uniiccdif
24958 uniioovol
24959 uniiccvol
24960 uniioombllem2
24963 uniioombllem3a
24964 uniioombllem3
24965 uniioombllem4
24966 uniioombllem5
24967 uniioombl
24969 dyadmbllem
24979 opnmbllem
24981 icoreresf
35869 icoreelrn
35878 relowlpssretop
35881 opnmbllem0
36160 mblfinlem1
36161 mblfinlem2
36162 voliooicof
44323 ovolval3
44974 ovolval4lem2
44977 ovolval5lem2
44980 ovolval5lem3
44981 ovnovollem1
44983 ovnovollem2
44984 |