Colors of
variables: wff
setvar class |
Syntax hints:
= wceq 1542 ∖ cdif 3908
⊆ wss 3911 ∅c0 4283 |
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-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3446 df-dif 3914 df-in 3918 df-ss 3928 df-nul 4284 |
This theorem is referenced by: symdif0
5046 fresaun
6714 dffv2
6937 ablfac1eulem
19856 itgioo
25196 newval
27207 nbgr0vtx
28346 imadifxp
31565 sibf0
32991 ballotlemfval0
33152 ballotlemgun
33181 satf0
34023 mdvval
34155 fzdifsuc2
43631 ibliooicc
44298 disjdifb
46980 |