![]() |
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 6895 | . 2 ⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘𝐵)) |
3 | 2 | eqeq1d 2733 | 1 ⊢ (𝜑 → ((𝐹‘𝐴) = 𝐶 ↔ (𝐹‘𝐵) = 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1540 ‘cfv 6543 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-rab 3432 df-v 3475 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-iota 6495 df-fv 6551 |
This theorem is referenced by: fveqeq2 6900 op1stg 7991 op2ndg 7992 ttrclss 9721 ttrclselem2 9727 fpwwecbv 10645 fpwwelem 10646 fseq1m1p1 13583 ico01fl0 13791 divfl0 13796 hashssdif 14379 cshw1 14779 smumullem 16440 algcvga 16523 vdwlem6 16926 vdwlem8 16928 ramub1lem1 16966 resmgmhm 18642 resmhm 18743 isghm 19137 fislw 19541 pgpfaclem2 20000 0ringdif 20423 abvfval 20657 abvpropd 20681 lspsneq0 20855 reslmhm 20896 lspsneq 20969 mdetunilem7 22441 imasdsf1olem 24200 bcth 25178 ovoliunnul 25357 lognegb 26439 vmaval 26960 2lgslem3c 27246 2lgslem3d 27247 rusgrnumwrdl2 29278 wlkiswwlks2 29564 rusgrnumwwlks 29663 clwlkclwwlklem1 29687 clwlkclwwlklem2 29688 numclwwlk1 30049 wlkl0 30055 numclwlk1lem1 30057 isnvlem 30298 lnoval 30440 normsub0 30824 elunop2 31701 ishst 31902 hstri 31953 aciunf1lem 32322 lmatfval 33260 lmatcl 33262 voliune 33693 volfiniune 33694 snmlval 34788 voliunnfl 36999 sdclem1 37078 islshp 38316 lshpnel2N 38322 lshpset2N 38456 dicffval 40512 dicfval 40513 mapdhval 41062 hdmap1fval 41134 hdmap1vallem 41135 hdmap1val 41136 diophin 41976 eldioph4b 42015 eldioph4i 42016 diophren 42017 fperiodmullem 44475 fargshiftfva 46573 paireqne 46641 |
Copyright terms: Public domain | W3C validator |