| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Equality theorem for function predicate. |
| Ref | Expression |
|---|---|
| funeq |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | funss 4543 |
. . . 4
| |
| 2 | funss 4543 |
. . . 4
| |
| 3 | 1, 2 | anim12i 536 |
. . 3
|
| 4 | 3 | ancoms 416 |
. 2
|
| 5 | eqss 2860 |
. 2
| |
| 6 | dfbi2 704 |
. 2
| |
| 7 | 4, 5, 6 | 3imtr4i 328 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: funeqi 4545 funeqd 4546 fununi 4582 funcnvuni 4583 cnvresid 4588 fneq1 4602 f1cnvcnv 4699 f1co 4700 f10 4753 fvopab6 4843 funoprabg 5032 tfrlem10 5292 tz7.44lem1 5299 tz7.48-2OLD 5330 abianfp 5338 th3qcor 5536 elpm 5556 ssdomg 5628 fndmeng 5649 sbthlem7 5682 sbthlem8 5683 ordtypelem4 5918 tz9.12lem2 6007 tz9.12lem3 6008 axdc3lem2 6306 zorn2lem4 6364 axaddopr 6783 axmulopr 6784 idcn 9908 fungid 10208 vsfval 10455 ajfuni 10730 dfrelog 10981 funadj 12282 funcnvadj 12286 bnj1379 13871 bnj1385 13873 bnj1375 14280 bnj1497 14331 injrec2 15178 cmpfun 15214 repfuntw 15241 cur1val 15285 isalg 15862 algi 15868 tartarmap 16075 ordtypelem4OLD 16202 neibastop2lem1 16343 neibastop2lem3 16345 neibastop2lem4 16346 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1592 ax-gen 1593 ax-8 1594 ax-9 1595 ax-10 1596 ax-11 1597 ax-12 1598 ax-14 1600 ax-17 1605 ax-4 1608 ax-5o 1610 ax-6o 1613 ax-9o 1763 ax-10o 1781 ax-16 1854 ax-11o 1864 ax-ext 2123 ax-sep 3606 ax-nul 3613 ax-pow 3649 ax-pr 3687 |
| This theorem depends on definitions: df-bi 220 df-or 338 df-an 339 df-ex 1616 df-sb 1816 df-eu 2041 df-mo 2042 df-clab 2129 df-cleq 2134 df-clel 2137 df-ne 2268 df-v 2540 df-dif 2830 df-un 2832 df-in 2834 df-ss 2836 df-nul 3083 df-pw 3229 df-sn 3242 df-pr 3243 df-op 3246 df-br 3508 df-opab 3566 df-id 3747 df-rel 4134 df-cnv 4135 df-co 4136 df-fun 4141 |