| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > fveqeq2d | Structured version Visualization version GIF version | ||
| Description: Equality deduction for function value. (Contributed by BJ, 30-Aug-2022.) |
| Ref | Expression |
|---|---|
| fveqeq2d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
| Ref | Expression |
|---|---|
| fveqeq2d | ⊢ (𝜑 → ((𝐹‘𝐴) = 𝐶 ↔ (𝐹‘𝐵) = 𝐶)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fveqeq2d.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
| 2 | 1 | fveq2d 6871 | . 2 ⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘𝐵)) |
| 3 | 2 | eqeq1d 2764 | 1 ⊢ (𝜑 → ((𝐹‘𝐴) = 𝐶 ↔ (𝐹‘𝐵) = 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 208 = wceq 1560 ‘cfv 6521 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-ext 2734 |
| This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-sb 2091 df-clab 2741 df-cleq 2754 df-clel 2837 df-rab 3415 df-v 3456 df-dif 3907 df-un 3909 df-ss 3921 df-nul 4286 df-if 4481 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-br 5101 df-iota 6477 df-fv 6529 |
| This theorem is referenced by: fveqeq2 6876 op1stg 7982 op2ndg 7983 ttrclss 9675 ttrclselem2 9681 fpwwecbv 10602 fpwwelem 10603 fseq1m1p1 13604 ico01fl0 13829 divfl0 13834 hashssdif 14425 cshw1 14835 smumullem 16526 algcvga 16613 vdwlem6 17022 vdwlem8 17024 ramub1lem1 17062 resmgmhm 18745 resmhm 18854 fislw 19665 pgpfaclem2 20124 0ringdif 20577 abvfval 20859 abvpropd 20884 lspsneq0 21079 reslmhm 21119 lspsneq 21192 mdetunilem7 22678 imasdsf1olem 24433 bcth 25391 ovoliunnul 25569 lognegb 26655 vmaval 27177 2lgslem3c 27462 2lgslem3d 27463 rusgrnumwrdl2 29787 wlkiswwlks2 30075 rusgrnumwwlks 30177 clwlkclwwlklem1 30201 clwlkclwwlklem2 30202 numclwwlk1 30563 wlkl0 30569 numclwlk1lem1 30571 isnvlem 30813 lnoval 30955 normsub0 31339 elunop2 32216 ishst 32417 hstri 32468 aciunf1lem 32864 esplyfvaln 33871 esplyind 33872 vietadeg1 33875 lmatfval 34111 lmatcl 34113 voliune 34526 volfiniune 34527 snmlval 35681 qdiff 37819 voliunnfl 38163 sdclem1 38242 islshp 39603 lshpnel2N 39609 lshpset2N 39743 dicffval 41798 dicfval 41799 mapdhval 42348 hdmap1fval 42420 hdmap1vallem 42421 hdmap1val 42422 aks6d1c6isolem1 42791 aks6d1c6lem5 42794 diophin 43353 eldioph4b 43388 eldioph4i 43389 diophren 43390 fperiodmullem 45882 fourierdlem48 46728 fourierdlem49 46729 fargshiftfva 48049 paireqne 48117 grimidvtxedg 48507 grimcnv 48510 grimco 48511 isuspgrim0 48516 uhgrimisgrgriclem 48552 clnbgrgrimlem 48555 |
| Copyright terms: Public domain | W3C validator |