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
32039 bnj906
33972 bnj1137
34037 bnj1408
34078 cvmliftlem10
34316 cvmliftlem13
34318 sstotbnd2
36690 mapdrvallem3
40565 onsucunifi
42168 fvmptiunrelexplb0d
42483 fvmptiunrelexplb1d
42485 corclrcl
42506 trclrelexplem
42510 corcltrcl
42538 cotrclrcl
42541 iunincfi
43831 iundjiunlem
45223 meaiuninc3v
45248 caratheodorylem1
45290 ovnhoilem1
45365 |