Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 = wceq 1542
∈ wcel 2107 ⊆
wss 3949 ∪ ciun 4998 |
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-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-tru 1545 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ral 3063 df-rex 3072 df-v 3477 df-in 3956 df-ss 3966 df-iun 5000 |
This theorem is referenced by: fviunfun
7931 onfununi
8341 oaordi
8546 omordi
8566 dffi3
9426 alephordi
10069 domtriomlem
10437 pwxpndom2
10660 wunex2
10733 imasaddvallem
17475 imasvscaval
17484 iundisj2
25066 voliunlem1
25067 volsup
25073 iundisj2fi
32008 bnj906
33941 bnj1137
34006 bnj1408
34047 cvmliftlem10
34285 cvmliftlem13
34287 sstotbnd2
36642 mapdrvallem3
40517 onsucunifi
42120 fvmptiunrelexplb0d
42435 fvmptiunrelexplb1d
42437 corclrcl
42458 trclrelexplem
42462 corcltrcl
42490 cotrclrcl
42493 iunincfi
43783 iundjiunlem
45175 meaiuninc3v
45200 caratheodorylem1
45242 ovnhoilem1
45317 |