Colors of
variables: wff
setvar class |
Syntax hints:
∈ wcel 2098 {crab 3426
⊆ wss 3943 ∩ cint 4943 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905
ax-6 1963 ax-7 2003 ax-8 2100
ax-9 2108 ax-11 2146 ax-ext 2697 |
This theorem depends on definitions:
df-bi 206 df-an 396
df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2704 df-cleq 2718 df-clel 2804 df-ral 3056 df-rab 3427 df-v 3470 df-in 3950 df-ss 3960 df-int 4944 |
This theorem is referenced by: intmin
4965 cofon2
8674 naddunif
8694 wuncid
10740 mrcssid
17570 lspssid
20832 lbsextlem3
21011 aspssid
21772 sscls
22915 filufint
23779 spanss2
31107 shsval2i
31149 ococin
31170 chsupsn
31175 fldgenssid
32906 sssigagen
33673 dynkin
33695 igenss
37443 pclssidN
39279 dochocss
40750 rgspnssid
42487 intubeu
47880 |