Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ↔ wb 205
∀wal 1538 ∈
wcel 2105 ∀wral 3060
Vcvv 3473 ∩ cint 4950 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912
ax-6 1970 ax-7 2010 ax-8 2107
ax-9 2115 ax-ext 2702 |
This theorem depends on definitions:
df-bi 206 df-an 396
df-tru 1543 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-ral 3061 df-int 4951 |
This theorem is referenced by: int0
4966 ssint
4968 intssuni
4974 iinuni
5101 onint
7782 intwun
10736 inttsk
10775 intgru
10815 subgint
19073 subrngint
20456 subrgint
20493 lssintcl
20807 toponmre
22917 alexsubALTlem3
23873 shintcli
31015 chintcli
31017 intlidl
32976 fin2so
36939 intidl
37361 mzpincl
41935 elimaint
42863 elintima
42867 intsal
45505 salgencntex
45518 |