![]() |
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 6237 | . 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝑋⟶𝐴 ↔ 𝐹:𝑋⟶𝐵)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐹:𝑋⟶𝐴 ↔ 𝐹:𝑋⟶𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 = wceq 1653 ⟶wf 6095 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2775 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2784 df-cleq 2790 df-clel 2793 df-in 3774 df-ss 3781 df-f 6103 |
This theorem is referenced by: feq123d 6243 fsn2 6628 fsng 6629 fsnunf 6678 funcres2b 16868 funcres2 16869 funcres2c 16872 catciso 17068 hofcl 17211 yonedalem4c 17229 yonedalem3b 17231 yonedainv 17233 gsumress 17588 resmhm2b 17673 pwsdiagmhm 17681 frmdup3lem 17716 frmdup3 17717 isghm 17970 frgpup3lem 18502 gsumzsubmcl 18630 dmdprd 18710 frlmup2 20460 scmatghm 20662 scmatmhm 20663 mdetdiaglem 20727 cnpf2 21380 2ndcctbss 21584 1stcelcls 21590 uptx 21754 txcn 21755 tsmssubm 22271 cnextucn 22432 pi1addf 23171 caufval 23398 equivcau 23423 lmcau 23436 plypf1 24306 coef2 24325 ulmval 24472 uhgr0vb 26299 uhgrun 26301 uhgrstrrepe 26305 isumgrs 26323 upgrun 26345 umgrun 26347 wksfval 26851 wlkres 26913 wlkresOLD 26915 ajfval 28181 chscllem4 29016 rrhf 30550 sibff 30906 sibfof 30910 orvcval4 31031 bj-finsumval0 33638 matunitlindflem2 33887 poimirlem9 33899 isbnd3 34062 prdsbnd 34071 heibor 34099 elghomlem1OLD 34163 cnfsmf 41683 upwlksfval 42503 resmgmhm2b 42587 zrtermorngc 42788 zrtermoringc 42857 |
Copyright terms: Public domain | W3C validator |