Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2099
≠ wne 2935 ∀wral 3056 ∃wrex 3065
⊆ wss 3944 ∅c0 4318 ∪ cuni 4903 ∩ cint 4944 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906
ax-6 1964 ax-7 2004 ax-8 2101
ax-9 2109 ax-ext 2698 |
This theorem depends on definitions:
df-bi 206 df-an 396
df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2705 df-cleq 2719 df-clel 2805 df-ne 2936 df-ral 3057 df-rex 3066 df-v 3471 df-dif 3947 df-in 3951 df-ss 3961 df-nul 4319 df-uni 4904 df-int 4945 |
This theorem is referenced by: unissint
4970 intssuni2
4971 intss2
5105 fin23lem31
10358 wunint
10730 tskint
10800 incexc
15807 incexc2
15808 subgint
19096 efgval
19663 lbsextlem3
21037 cssmre
21612 uffixfr
23814 uffix2
23815 uffixsn
23816 ssmxidllem
33122 insiga
33692 dfon2lem8
35322 intidl
37437 elrfi
42036 toplatglb
47935 |