Colors of
variables: wff
setvar class |
Syntax hints: -> wi 4 = wceq 1395
e. wcel 1818 U_ ciun 4330 |
This theorem is referenced by: iununi
4415 oelim2
7263 ituniiun
8823 imasval
14908 mreacs
15055 cnextval
20561 taylfval
22754 iunpreima
27432 msubvrs
28920 dfrtrclrec2
29066 rtrclreclem.refl
29067 rtrclreclem.subset
29068 rtrclreclem.min
29070 trpredeq1
29303 trpredeq2
29304 voliunnfl
30058 neibastop2
30179 sstotbnd2
30270 equivtotbnd
30274 totbndbnd
30285 heiborlem3
30309 otiunsndisjX
32301 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1618 ax-4 1631 ax-5 1704
ax-6 1747 ax-7 1790 ax-10 1837 ax-11 1842 ax-12 1854 ax-13 1999 ax-ext 2435 |
This theorem depends on definitions:
df-bi 185 df-an 371
df-tru 1398 df-ex 1613 df-nf 1617 df-sb 1740 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ral 2812 df-rex 2813 df-v 3111 df-in 3482 df-ss 3489 df-iun 4332 |