Colors of
variables: wff
setvar class |
Syntax hints:
= wceq 1542 ∖ cdif 3946
∪ cun 3947 |
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-or 847 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 |
This theorem is referenced by: undif
4482 dfif5
4545 funiunfv
7247 difex2
7747 undom
9059 undomOLD
9060 sucdom2OLD
9082 domss2
9136 sucdom2
9206 unfiOLD
9313 marypha1lem
9428 kmlem11
10155 hashun2
14343 hashun3
14344 cvgcmpce
15764 dprd2da
19912 dpjcntz
19922 dpjdisj
19923 dpjlsm
19924 dpjidcl
19928 ablfac1eu
19943 dfconn2
22923 2ndcdisj2
22961 fixufil
23426 fin1aufil
23436 xrge0gsumle
24349 unmbl
25054 volsup
25073 mbfss
25163 itg2cnlem2
25280 iblss2
25323 amgm
26495 wilthlem2
26573 ftalem3
26579 rpvmasum2
27015 noetasuplem4
27239 noetainflem4
27243 esumpad
33053 srcmpltd
34085 imadifss
36463 elrfi
41432 oaun2
42131 oaun3
42132 meaunle
45180 |