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 6490 | . 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝑋⟶𝐴 ↔ 𝐹:𝑋⟶𝐵)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐹:𝑋⟶𝐴 ↔ 𝐹:𝑋⟶𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1528 ⟶wf 6344 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-in 3940 df-ss 3949 df-f 6352 |
This theorem is referenced by: feq123d 6496 fsn2 6890 fsng 6891 fsnunf 6939 funcres2b 17155 funcres2 17156 funcres2c 17159 catciso 17355 hofcl 17497 yonedalem4c 17515 yonedalem3b 17517 yonedainv 17519 gsumress 17880 resmhm2b 17975 pwsdiagmhm 17983 frmdup3lem 18019 frmdup3 18020 isghm 18296 frgpup3lem 18832 gsumzsubmcl 18967 dmdprd 19049 frlmup2 20871 scmatghm 21070 scmatmhm 21071 mdetdiaglem 21135 cnpf2 21786 2ndcctbss 21991 1stcelcls 21997 uptx 22161 txcn 22162 tsmssubm 22678 cnextucn 22839 pi1addf 23578 caufval 23805 equivcau 23830 lmcau 23843 plypf1 24729 coef2 24748 ulmval 24895 uhgr0vb 26784 uhgrun 26786 uhgrstrrepe 26790 isumgrs 26808 upgrun 26830 umgrun 26832 wksfval 27318 wlkres 27379 ajfval 28513 chscllem4 29344 lindfpropd 30869 fedgmullem1 30924 rrhf 31138 sibff 31493 sibfof 31497 orvcval4 31617 bj-finsumval0 34455 matunitlindflem2 34770 poimirlem9 34782 isbnd3 34943 prdsbnd 34952 heibor 34980 elghomlem1OLD 35044 selvval2lem4 39014 cnfsmf 42894 upwlksfval 43887 resmgmhm2b 43944 zrtermorngc 44200 zrtermoringc 44269 |
Copyright terms: Public domain | W3C validator |