Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 {cab 2710
∀wral 3062 ⊆
wss 3949 ∩ cint 4951 |
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-ral 3063 df-v 3477 df-in 3956 df-ss 3966 df-int 4952 |
This theorem is referenced by: uniintsn
4992 intabs
5343 cofon1
8671 naddssim
8684 fiss
9419 tc2
9737 tcss
9739 tcel
9740 rankval4
9862 cfub
10244 cflm
10245 cflecard
10248 fin23lem26
10320 clsslem
14931 mrcss
17560 lspss
20595 lbsextlem3
20773 aspss
21431 clsss
22558 1stcfb
22949 ufinffr
23433 cofcut1
27407 spanss
30601 fldgenss
32406 ss2mcls
34559 pclssN
38765 dochspss
40249 clss2lem
42362 |