Colors of
variables: wff
setvar class |
Syntax hints:
= wceq 1542 ∈ wcel 2107
∀wral 3062 Vcvv 3475
∅c0 4323 ∩ 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-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3063 df-v 3477 df-dif 3952 df-nul 4324 df-int 4952 |
This theorem is referenced by: unissint
4977 uniintsn
4992 rint0
4995 intex
5338 intnex
5339 oev2
8523 fiint
9324 elfi2
9409 fi0
9415 cardmin2
9994 00lsp
20592 cmpfi
22912 ptbasfi
23085 fbssint
23342 fclscmp
23534 zarcmplem
32861 rankeq1o
35143 bj-0int
35982 heibor1lem
36677 ipoglb0
47619 mreclat
47622 |