Colors of
variables: wff
setvar class |
Syntax hints:
∈ wcel 2098 {crab 3430
⊆ wss 3949 ∩ cint 4953 |
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 2699 |
This theorem depends on definitions:
df-bi 206 df-an 395
df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2706 df-cleq 2720 df-clel 2806 df-ral 3059 df-rab 3431 df-v 3475 df-in 3956 df-ss 3966 df-int 4954 |
This theorem is referenced by: intmin
4975 cofon2
8700 naddunif
8720 wuncid
10774 mrcssid
17604 lspssid
20876 lbsextlem3
21055 aspssid
21818 sscls
22980 filufint
23844 spanss2
31175 shsval2i
31217 ococin
31238 chsupsn
31243 fldgenssid
33024 sssigagen
33797 dynkin
33819 igenss
37568 pclssidN
39400 dochocss
40871 rgspnssid
42625 intubeu
48073 |