Colors of
variables: wff
setvar class |
Syntax hints:
∈ wcel 2107 Vcvv 3444
𝒫 cpw 4561 ∪ cuni 4866 ℂcc 11054
+∞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-pow 5321 ax-un 7673 ax-cnex 11112 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3446 df-in 3918 df-ss 3928 df-pw 4563 df-uni 4867 df-pnf 11196 |
This theorem is referenced by: pnfxr
11214 mnfxr
11217 elxnn0
12492 elxr
13042 xnegex
13133 xaddval
13148 xmulval
13150 xrinfmss
13235 hashgval
14239 hashinf
14241 hashfxnn0
14243 pcval
16721 pc0
16731 ramcl2
16893 iccpnfhmeo
24324 taylfval
25734 xrlimcnp
26334 xrge0iifcv
32572 xrge0iifiso
32573 xrge0iifhom
32575 sge0f1o
44709 sge0sup
44718 sge0pnfmpt
44772 |