![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > feq1 | Structured version Visualization version Unicode version |
Description: Equality theorem for functions. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
feq1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fneq1 5686 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | rneq 5079 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | sseq1d 3471 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | anbi12d 722 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | df-f 5605 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | df-f 5605 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 4, 5, 6 | 3bitr4g 296 |
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 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-rab 2758 df-v 3059 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-nul 3744 df-if 3894 df-sn 3981 df-pr 3983 df-op 3987 df-br 4417 df-opab 4476 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-fun 5603 df-fn 5604 df-f 5605 |
This theorem is referenced by: feq1d 5736 feq1i 5742 elimf 5750 f00 5788 f0bi 5789 f0dom0 5790 fconstg 5793 f1eq1 5797 fconst2g 6143 fconstfvOLD 6152 fsnex 6206 elmapg 7511 ac6sfi 7841 ac5num 8493 acni2 8503 cofsmo 8725 cfsmolem 8726 cfcoflem 8728 coftr 8729 alephsing 8732 axdc2lem 8904 axdc3lem2 8907 axdc3lem3 8908 axdc3 8910 axdc4lem 8911 ac6num 8935 inar1 9226 1fv 11939 axdc4uzlem 12227 seqf1olem2 12285 seqf1o 12286 iswrd 12705 iswrdOLD 12706 wrdlen2i 13067 ramub2 15020 ramcl 15036 isacs2 15608 isacs1i 15612 mreacs 15613 mgmb1mgm1 16548 isgrpinv 16765 isghm 16932 islindf 19419 mat1dimelbas 19545 1stcfb 20509 upxp 20687 txcn 20690 isi1f 22681 mbfi1fseqlem6 22727 mbfi1flimlem 22729 itg2addlem 22765 plyf 23201 wlkelwrd 25307 iseupa 25742 isgrpo 25973 ismgmOLD 26097 elghomlem2OLD 26139 vci 26216 isvclem 26245 isnvlem 26278 ajmoi 26549 ajval 26552 hlimi 26890 chlimi 26936 chcompl 26944 adjmo 27534 adjeu 27591 adjval 27592 adj1 27635 adjeq 27637 cnlnssadj 27782 pjinvari 27893 padct 28356 locfinref 28717 isrnmeas 29071 fprb 30462 orderseqlem 30539 soseq 30541 elno 30582 filnetlem4 31086 bj-finsumval0 31747 poimirlem25 32010 poimirlem28 32013 volsupnfl 32030 mbfresfi 32032 upixp 32101 sdclem2 32116 sdclem1 32117 fdc 32119 istendo 34372 ismrc 35588 fmuldfeqlem1 37698 fmuldfeq 37699 dvnprodlem1 37859 stoweidlem15 37913 stoweidlem16 37914 stoweidlem17 37915 stoweidlem19 37917 stoweidlem20 37918 stoweidlem21 37919 stoweidlem22 37920 stoweidlem23 37921 stoweidlem27 37925 stoweidlem31 37930 stoweidlem32 37931 stoweidlem42 37941 stoweidlem48 37947 stoweidlem51 37950 stoweidlem59 37958 isomenndlem 38389 griedg0prc 39386 lincdifsn 40490 |
Copyright terms: Public domain | W3C validator |