Colors of
variables: wff
setvar class |
Syntax hints:
∈ wcel 2107 ∉ wnel 3046
𝒫 cpw 4561 ∪ cuni 4866 ℂcc 11054
ℝ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-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: pnfnre2
11202 renepnf
11208 ltxrlt
11230 nn0nepnf
12498 xrltnr
13045 pnfnlt
13054 xnn0lenn0nn0
13170 hashclb
14264 hasheq0
14269 pcgcd1
16754 pc2dvds
16756 ramtcl2
16888 odhash3
19363 xrsdsreclblem
20859 pnfnei
22587 iccpnfcnv
24323 i1f0rn
25062 |