Colors of
variables: wff
setvar class |
Syntax hints:
= wceq 1542 ∈ wcel 2107
∀wral 3061 Vcvv 3444
∅c0 4283 ∩ cint 4908 |
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-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3062 df-v 3446 df-dif 3914 df-nul 4284 df-int 4909 |
This theorem is referenced by: unissint
4934 uniintsn
4949 rint0
4952 intex
5295 intnex
5296 oev2
8470 fiint
9271 elfi2
9355 fi0
9361 cardmin2
9940 00lsp
20457 cmpfi
22775 ptbasfi
22948 fbssint
23205 fclscmp
23397 zarcmplem
32519 rankeq1o
34802 bj-0int
35618 heibor1lem
36314 ipoglb0
47105 mreclat
47108 |