| 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 6718 | . 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝑋⟶𝐴 ↔ 𝐹:𝑋⟶𝐵)) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐹:𝑋⟶𝐴 ↔ 𝐹:𝑋⟶𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 ⟶wf 6557 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-ss 3968 df-f 6565 |
| This theorem is referenced by: feq123d 6725 fsn2 7156 fsng 7157 fsnunf 7205 funcres2b 17942 funcres2 17943 funcres2c 17948 catciso 18156 hofcl 18304 yonedalem4c 18322 yonedalem3b 18324 yonedainv 18326 gsumress 18695 resmgmhm2b 18726 resmhm2b 18835 pwsdiagmhm 18844 frmdup3lem 18879 frmdup3 18880 isghmOLD 19234 frgpup3lem 19795 gsumzsubmcl 19936 dmdprd 20018 zrtermorngc 20643 zrtermoringc 20675 imadrhmcl 20798 rngqiprngghm 21309 frlmup2 21819 scmatghm 22539 scmatmhm 22540 mdetdiaglem 22604 cnpf2 23258 2ndcctbss 23463 1stcelcls 23469 uptx 23633 txcn 23634 tsmssubm 24151 cnextucn 24312 pi1addf 25080 caufval 25309 equivcau 25334 lmcau 25347 plypf1 26251 coef2 26270 ulmval 26423 uhgr0vb 29089 uhgrun 29091 uhgrstrrepe 29095 isumgrs 29113 upgrun 29135 umgrun 29137 wksfval 29627 wlkres 29688 ajfval 30828 chscllem4 31659 feq3dd 32633 rlocf1 33277 imasmhm 33382 imasghm 33383 imasrhm 33384 lindfpropd 33410 ply1degltdimlem 33673 fedgmullem1 33680 rrhf 33999 sibff 34338 sibfof 34342 orvcval4 34463 bj-finsumval0 37286 matunitlindflem2 37624 poimirlem9 37636 isbnd3 37791 prdsbnd 37800 heibor 37828 elghomlem1OLD 37892 aks6d1c6lem2 42172 aks6d1c6lem3 42173 aks6d1c6isolem2 42176 aks6d1c6lem5 42178 evlsvvval 42573 cnfsmf 46755 upwlksfval 48051 |
| Copyright terms: Public domain | W3C validator |