Colors of
variables: wff
setvar class |
Syntax hints:
∧ wa 397 = wceq 1542
∈ wcel 2107 {copab 5171 ↦ cmpt 5192
I cid 5534 ↾ cres 5639 |
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-10 2138 ax-12 2172 ax-ext 2704 ax-sep 5260 ax-nul 5267 ax-pr 5388 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3407 df-v 3449 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-nul 4287 df-if 4491 df-sn 4591 df-pr 4593 df-op 4597 df-opab 5172 df-mpt 5193 df-id 5535 df-xp 5643 df-rel 5644 df-res 5649 |
This theorem is referenced by: idref
7096 2fvcoidd
7247 pwfseqlem5
10607 restid2
17320 curf2ndf
18144 hofcl
18156 yonedainv
18178 smndex2dlinvh
18735 sylow1lem2
19389 sylow3lem1
19417 0frgp
19569 frgpcyg
21003 evpmodpmf1o
21023 cnmptid
23035 txswaphmeolem
23178 idnghm
24130 dvexp
25340 dvmptid
25344 mvth
25379 plyid
25593 coeidp
25647 dgrid
25648 plyremlem
25687 taylply2
25750 wilthlem2
26441 ftalem7
26451 fusgrfis
28327 fzto1st1
32007 cycpm2tr
32024 zrhre
32664 qqhre
32665 fsovcnvlem
42377 fourierdlem60
44497 fourierdlem61
44498 itcoval0mpt
46842 |