Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ↔ wb 205
∀wal 1540 ∈
wcel 2107 ∀wral 3062
Vcvv 3475 ∩ 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-int 4952 |
This theorem is referenced by: int0
4967 ssint
4969 intssuni
4975 iinuni
5102 onint
7778 intwun
10730 inttsk
10769 intgru
10809 subgint
19030 subrgint
20342 lssintcl
20575 toponmre
22597 alexsubALTlem3
23553 shintcli
30613 chintcli
30615 intlidl
32567 fin2so
36523 intidl
36945 mzpincl
41520 elimaint
42448 elintima
42452 intsal
45094 salgencntex
45107 subrngint
46787 |