Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 = wceq 1542
∈ wcel 2107 ∀wral 3061 ∃wrex 3070
∩ cin 3913 𝒫
cpw 4564 ∪ cuni 4869 Fincfn 8889
Topctop 22265 Compccmp 22760 |
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 |
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-ral 3062 df-rex 3071 df-rab 3407 df-v 3449 df-in 3921 df-ss 3931 df-pw 4566 df-uni 4870 df-cmp 22761 |
This theorem is referenced by: imacmp
22771 cmpcld
22776 fiuncmp
22778 cmpfii
22783 bwth
22784 locfincmp
22900 kgeni
22911 kgentopon
22912 kgencmp
22919 kgencmp2
22920 cmpkgen
22925 txcmplem1
23015 txcmp
23017 qtopcmp
23082 cmphaushmeo
23174 ptcmpfi
23187 fclscmpi
23403 alexsubALTlem1
23421 ptcmplem1
23426 ptcmpg
23431 evth
24345 evth2
24346 cmppcmp
32503 ordcmp
34972 poimirlem30
36158 heibor1lem
36318 cmpfiiin
41067 kelac1
41437 kelac2
41439 stoweidlem28
44359 stoweidlem50
44381 stoweidlem53
44384 stoweidlem57
44388 stoweidlem62
44393 |