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 6673 | . 2 ⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘𝐵)) |
3 | 2 | eqeq1d 2823 | 1 ⊢ (𝜑 → ((𝐹‘𝐴) = 𝐶 ↔ (𝐹‘𝐵) = 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 = wceq 1533 ‘cfv 6354 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3496 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4467 df-sn 4567 df-pr 4569 df-op 4573 df-uni 4838 df-br 5066 df-iota 6313 df-fv 6362 |
This theorem is referenced by: fveqeq2 6678 op1stg 7700 op2ndg 7701 fpwwecbv 10065 fpwwelem 10066 fseq1m1p1 12981 ico01fl0 13188 divfl0 13193 hashssdif 13772 cshw1 14183 smumullem 15840 algcvga 15922 vdwlem6 16321 vdwlem8 16323 ramub1lem1 16361 resmhm 17984 isghm 18357 fislw 18749 pgpfaclem2 19203 abvfval 19588 abvpropd 19612 lspsneq0 19783 reslmhm 19823 lspsneq 19893 mdetunilem7 21226 imasdsf1olem 22982 bcth 23931 ovoliunnul 24107 lognegb 25172 vmaval 25689 2lgslem3c 25973 2lgslem3d 25974 rusgrnumwrdl2 27367 wlkiswwlks2 27652 rusgrnumwwlks 27752 clwlkclwwlklem1 27776 clwlkclwwlklem2 27777 numclwwlk1 28139 wlkl0 28145 numclwlk1lem1 28147 isnvlem 28386 lnoval 28528 normsub0 28912 elunop2 29789 ishst 29990 hstri 30041 aciunf1lem 30406 lmatfval 31079 lmatcl 31081 voliune 31488 volfiniune 31489 snmlval 32578 voliunnfl 34935 sdclem1 35017 islshp 36114 lshpnel2N 36120 lshpset2N 36254 dicffval 38309 dicfval 38310 mapdhval 38859 hdmap1fval 38931 hdmap1vallem 38932 hdmap1val 38933 diophin 39367 eldioph4b 39406 eldioph4i 39407 diophren 39408 fperiodmullem 41568 fargshiftfva 43602 paireqne 43672 resmgmhm 44064 0ringdif 44140 |
Copyright terms: Public domain | W3C validator |