Colors of
variables: wff
setvar class |
Syntax hints: ¬ wn 3 → wi 4
= wceq 1539 ∈
wcel 2104 ≠ wne 2938
∩ cin 3946 ∅c0 4321 {csn 4627 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911
ax-6 1969 ax-7 2009 ax-8 2106
ax-9 2114 ax-ext 2701 |
This theorem depends on definitions:
df-bi 206 df-an 395
df-tru 1542 df-fal 1552 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-ne 2939 df-ral 3060 df-v 3474 df-dif 3950 df-in 3954 df-nul 4322 df-sn 4628 |
This theorem is referenced by: disjpr2
4716 disjtpsn
4718 difprsn1
4802 otsndisj
5518 xpsndisj
6161 funprg
6601 funtp
6604 funcnvpr
6609 f1oprg
6877 xp01disjl
8494 enpr2dOLD
9052 phplem1OLD
9219 djuin
9915 pm54.43
9998 pr2nelemOLD
10000 f1oun2prg
14872 s3sndisj
14918 sumpr
15698 cshwsdisj
17036 setsfun0
17109 setscom
17117 gsumpr
19864 dmdprdpr
19960 dprdpr
19961 ablfac1eulem
19983 cnfldfunALT
21157 cnfldfunALTOLD
21158 m2detleib
22353 dishaus
23106 dissnlocfin
23253 xpstopnlem1
23533 perfectlem2
26969 cosnopne
32183 prodpr
32299 esumpr
33362 esum2dlem
33388 prodfzo03
33913 gg-cnfldfunALT
35484 onint1
35637 bj-disjsn01
36136 lindsadd
36784 poimirlem26
36817 sumpair
44021 perfectALTVlem2
46688 |