Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∖ cdif 3944
⊆ wss 3947 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911
ax-6 1969 ax-7 2009 ax-8 2106
ax-9 2114 ax-ext 2701 |
This theorem depends on definitions:
df-bi 206 df-an 395
df-tru 1542 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-v 3474 df-dif 3950 df-in 3954 df-ss 3964 |
This theorem is referenced by: ssdifssd
4141 xrsupss
13292 xrinfmss
13293 rpnnen2lem12
16172 lpval
22863 lpdifsn
22867 islp2
22869 lpcls
23088 mblfinlem3
36830 mblfinlem4
36831 voliunnfl
36835 ssdifcl
42624 sssymdifcl
42625 supxrmnf2
44441 infxrpnf2
44471 fourierdlem102
45222 fourierdlem114
45234 lindslinindimp2lem4
47229 lindslinindsimp2lem5
47230 lindslinindsimp2
47231 lincresunit3
47249 |