Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∖ cdif 3908
⊆ wss 3911 |
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-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 |
This theorem is referenced by: ssdifssd
4103 xrsupss
13234 xrinfmss
13235 rpnnen2lem12
16112 lpval
22506 lpdifsn
22510 islp2
22512 lpcls
22731 mblfinlem3
36163 mblfinlem4
36164 voliunnfl
36168 ssdifcl
41931 sssymdifcl
41932 supxrmnf2
43754 infxrpnf2
43784 fourierdlem102
44535 fourierdlem114
44547 lindslinindimp2lem4
46628 lindslinindsimp2lem5
46629 lindslinindsimp2
46630 lincresunit3
46648 |