![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > feq3d | Structured version Visualization version GIF version |
Description: Equality deduction for functions. (Contributed by AV, 1-Jan-2020.) |
Ref | Expression |
---|---|
feq2d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
feq3d | ⊢ (𝜑 → (𝐹:𝑋⟶𝐴 ↔ 𝐹:𝑋⟶𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | feq2d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | feq3 6706 | . 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝑋⟶𝐴 ↔ 𝐹:𝑋⟶𝐵)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐹:𝑋⟶𝐴 ↔ 𝐹:𝑋⟶𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1533 ⟶wf 6545 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-cleq 2717 df-ss 3961 df-f 6553 |
This theorem is referenced by: feq123d 6712 fsn2 7145 fsng 7146 fsnunf 7194 funcres2b 17886 funcres2 17887 funcres2c 17893 catciso 18103 hofcl 18254 yonedalem4c 18272 yonedalem3b 18274 yonedainv 18276 gsumress 18645 resmgmhm2b 18676 resmhm2b 18782 pwsdiagmhm 18791 frmdup3lem 18826 frmdup3 18827 isghmOLD 19179 frgpup3lem 19744 gsumzsubmcl 19885 dmdprd 19967 zrtermorngc 20588 zrtermoringc 20620 imadrhmcl 20697 rngqiprngghm 21206 frlmup2 21750 scmatghm 22479 scmatmhm 22480 mdetdiaglem 22544 cnpf2 23198 2ndcctbss 23403 1stcelcls 23409 uptx 23573 txcn 23574 tsmssubm 24091 cnextucn 24252 pi1addf 25018 caufval 25247 equivcau 25272 lmcau 25285 plypf1 26191 coef2 26210 ulmval 26361 uhgr0vb 28957 uhgrun 28959 uhgrstrrepe 28963 isumgrs 28981 upgrun 29003 umgrun 29005 wksfval 29495 wlkres 29556 ajfval 30691 chscllem4 31522 feq3dd 32490 rlocf1 33063 imasmhm 33165 imasghm 33166 imasrhm 33167 lindfpropd 33194 ply1degltdimlem 33448 fedgmullem1 33455 rrhf 33727 sibff 34084 sibfof 34088 orvcval4 34208 bj-finsumval0 36892 matunitlindflem2 37218 poimirlem9 37230 isbnd3 37385 prdsbnd 37394 heibor 37422 elghomlem1OLD 37486 aks6d1c6lem2 41771 aks6d1c6lem3 41772 aks6d1c6isolem2 41775 aks6d1c6lem5 41777 evlsvvval 41928 cnfsmf 46263 upwlksfval 47380 |
Copyright terms: Public domain | W3C validator |