Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 = wceq 1542
∈ wcel 2107 ≠
wne 2940 ℝcr 11055
+∞cpnf 11191 |
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 ax-sep 5257 ax-pr 5385 ax-un 7673 ax-resscn 11113 |
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-ne 2941 df-nel 3047 df-rab 3407 df-v 3446 df-un 3916 df-in 3918 df-ss 3928 df-pw 4563 df-sn 4588 df-pr 4590 df-uni 4867 df-pnf 11196 |
This theorem is referenced by: renepnfd
11211 renfdisj
11220 xrnepnf
13044 rexneg
13136 rexadd
13157 xaddnepnf
13162 xaddcom
13165 xaddid1
13166 xnn0xadd0
13172 xnegdi
13173 xpncan
13176 xleadd1a
13178 rexmul
13196 xmulpnf1
13199 xadddilem
13219 rpsup
13777 hashneq0
14270 hash1snb
14325 xrsnsgrp
20849 xaddeq0
31705 icorempo
35868 ovoliunnfl
36166 voliunnfl
36168 volsupnfl
36169 supxrgelem
43658 supxrge
43659 infleinflem1
43691 infleinflem2
43692 xrre4
43732 supminfxr2
43790 climxrre
44077 sge0repnf
44713 voliunsge0lem
44799 |