Colors of
variables: wff
setvar class |
Syntax hints:
∈ wcel 2107 ∉ wnel 3047
𝒫 cpw 4603 ∪ cuni 4909 ℂcc 11108
ℝcr 11109 +∞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-pr 5428 ax-un 7725 ax-resscn 11167 |
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-nel 3048 df-rab 3434 df-v 3477 df-un 3954 df-in 3956 df-ss 3966 df-pw 4605 df-sn 4630 df-pr 4632 df-uni 4910 df-pnf 11250 |
This theorem is referenced by: pnfnre2
11256 renepnf
11262 ltxrlt
11284 nn0nepnf
12552 xrltnr
13099 pnfnlt
13108 xnn0lenn0nn0
13224 hashclb
14318 hasheq0
14323 pcgcd1
16810 pc2dvds
16812 ramtcl2
16944 odhash3
19444 xrsdsreclblem
20991 pnfnei
22724 iccpnfcnv
24460 i1f0rn
25199 |