Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2107
≠ wne 2941 ∀wral 3062 ∃wrex 3071
⊆ wss 3949 ∅c0 4323 ∪ cuni 4909 ∩ 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-ne 2942 df-ral 3063 df-rex 3072 df-v 3477 df-dif 3952 df-in 3956 df-ss 3966 df-nul 4324 df-uni 4910 df-int 4952 |
This theorem is referenced by: unissint
4977 intssuni2
4978 intss2
5112 fin23lem31
10338 wunint
10710 tskint
10780 incexc
15783 incexc2
15784 subgint
19030 efgval
19585 lbsextlem3
20773 cssmre
21246 uffixfr
23427 uffix2
23428 uffixsn
23429 ssmxidllem
32589 insiga
33135 dfon2lem8
34762 intidl
36897 elrfi
41432 toplatglb
47626 |