Colors of
variables: wff
setvar class |
Syntax hints:
∈ wcel 2107 Vcvv 3475
𝒫 cpw 4603 ∪ cuni 4909 ℂcc 11108
+∞cpnf 11245 |
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 5300 ax-pow 5364 ax-un 7725 ax-cnex 11166 |
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 3477 df-in 3956 df-ss 3966 df-pw 4605 df-uni 4910 df-pnf 11250 |
This theorem is referenced by: pnfxr
11268 mnfxr
11271 elxnn0
12546 elxr
13096 xnegex
13187 xaddval
13202 xmulval
13204 xrinfmss
13289 hashgval
14293 hashinf
14295 hashfxnn0
14297 pcval
16777 pc0
16787 ramcl2
16949 iccpnfhmeo
24461 taylfval
25871 xrlimcnp
26473 xrge0iifcv
32914 xrge0iifiso
32915 xrge0iifhom
32917 sge0f1o
45098 sge0sup
45107 sge0pnfmpt
45161 |