![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > feq23d | Structured version Visualization version Unicode version |
Description: Equality deduction for functions. (Contributed by NM, 8-Jun-2013.) |
Ref | Expression |
---|---|
feq23d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
feq23d.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
feq23d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqidd 2454 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | feq23d.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | feq23d.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | feq123d 5723 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 988 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-rab 2748 df-v 3049 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-nul 3734 df-if 3884 df-sn 3971 df-pr 3973 df-op 3977 df-br 4406 df-opab 4465 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-fun 5587 df-fn 5588 df-f 5589 |
This theorem is referenced by: nvof1o 6184 axdc4uz 12203 isacs 15569 isfunc 15781 funcres 15813 funcpropd 15817 estrcco 16027 funcestrcsetclem9 16045 fullestrcsetc 16048 fullsetcestrc 16063 1stfcl 16094 2ndfcl 16095 evlfcl 16119 curf1cl 16125 yonedalem3b 16176 intopsn 16510 mhmpropd 16600 pwssplit1 18294 evls1sca 18924 islindf 19382 rrxds 22364 isgrp2d 25975 isgrpda 26037 isrngod 26119 rngosn3 26166 acunirnmpt 28273 cnmbfm 29097 elmrsubrn 30170 poimirlem3 31955 poimirlem28 31980 islfld 32640 tendofset 34337 tendoset 34338 mapfzcons 35570 diophrw 35613 refsum2cnlem1 37368 mgmhmpropd 39889 funcringcsetcALTV2lem9 40150 funcringcsetclem9ALTV 40173 aacllem 40644 |
Copyright terms: Public domain | W3C validator |