| 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 6910 | . 2 ⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘𝐵)) |
| 3 | 2 | eqeq1d 2739 | 1 ⊢ (𝜑 → ((𝐹‘𝐴) = 𝐶 ↔ (𝐹‘𝐵) = 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 ‘cfv 6561 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-iota 6514 df-fv 6569 |
| This theorem is referenced by: fveqeq2 6915 op1stg 8026 op2ndg 8027 ttrclss 9760 ttrclselem2 9766 fpwwecbv 10684 fpwwelem 10685 fseq1m1p1 13639 ico01fl0 13859 divfl0 13864 hashssdif 14451 cshw1 14860 smumullem 16529 algcvga 16616 vdwlem6 17024 vdwlem8 17026 ramub1lem1 17064 resmgmhm 18724 resmhm 18833 isghmOLD 19234 fislw 19643 pgpfaclem2 20102 0ringdif 20527 abvfval 20811 abvpropd 20836 lspsneq0 21010 reslmhm 21051 lspsneq 21124 mdetunilem7 22624 imasdsf1olem 24383 bcth 25363 ovoliunnul 25542 lognegb 26632 vmaval 27156 2lgslem3c 27442 2lgslem3d 27443 rusgrnumwrdl2 29604 wlkiswwlks2 29895 rusgrnumwwlks 29994 clwlkclwwlklem1 30018 clwlkclwwlklem2 30019 numclwwlk1 30380 wlkl0 30386 numclwlk1lem1 30388 isnvlem 30629 lnoval 30771 normsub0 31155 elunop2 32032 ishst 32233 hstri 32284 aciunf1lem 32672 lmatfval 33813 lmatcl 33815 voliune 34230 volfiniune 34231 snmlval 35336 voliunnfl 37671 sdclem1 37750 islshp 38980 lshpnel2N 38986 lshpset2N 39120 dicffval 41176 dicfval 41177 mapdhval 41726 hdmap1fval 41798 hdmap1vallem 41799 hdmap1val 41800 aks6d1c6isolem1 42175 aks6d1c6lem5 42178 diophin 42783 eldioph4b 42822 eldioph4i 42823 diophren 42824 fperiodmullem 45315 fargshiftfva 47430 paireqne 47498 isuspgrim0 47872 grimidvtxedg 47876 grimcnv 47879 grimco 47880 uhgrimisgrgriclem 47898 clnbgrgrimlem 47901 |
| Copyright terms: Public domain | W3C validator |