MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  feq3d Structured version   Visualization version   GIF version

Theorem feq3d 5999
Description: Equality deduction for functions. (Contributed by AV, 1-Jan-2020.)
Hypothesis
Ref Expression
feq2d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
feq3d (𝜑 → (𝐹:𝑋𝐴𝐹:𝑋𝐵))

Proof of Theorem feq3d
StepHypRef Expression
1 feq2d.1 . 2 (𝜑𝐴 = 𝐵)
2 feq3 5995 . 2 (𝐴 = 𝐵 → (𝐹:𝑋𝐴𝐹:𝑋𝐵))
31, 2syl 17 1 (𝜑 → (𝐹:𝑋𝐴𝐹:𝑋𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1480  wf 5853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3567  df-ss 3574  df-f 5861
This theorem is referenced by:  feq123d  6001  fsn2  6368  fsng  6369  fsnunf  6416  funcres2b  16497  funcres2  16498  funcres2c  16501  catciso  16697  hofcl  16839  yonedalem4c  16857  yonedalem3b  16859  yonedainv  16861  gsumress  17216  resmhm2b  17301  pwsdiagmhm  17309  frmdup3lem  17343  frmdup3  17344  isghm  17600  frgpup3lem  18130  gsumzsubmcl  18258  dmdprd  18337  frlmup2  20078  scmatghm  20279  scmatmhm  20280  mdetdiaglem  20344  cnpf2  20994  2ndcctbss  21198  1stcelcls  21204  uptx  21368  txcn  21369  tsmssubm  21886  cnextucn  22047  pi1addf  22787  caufval  23013  equivcau  23038  lmcau  23051  plypf1  23906  coef2  23925  ulmval  24072  uhgr0vb  25897  uhgrun  25899  uhgrstrrepe  25903  isumgrs  25920  upgrun  25942  umgrun  25944  wksfval  26409  wlkres  26470  ajfval  27552  chscllem4  28387  rrhf  29866  sibff  30221  sibfof  30225  orvcval4  30345  bj-finsumval0  32819  matunitlindflem2  33077  poimirlem9  33089  isbnd3  33254  prdsbnd  33263  heibor  33291  elghomlem1OLD  33355  cnfsmf  40286  upwlksfval  41034  resmgmhm2b  41118  zrtermorngc  41319  zrtermoringc  41388
  Copyright terms: Public domain W3C validator