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

Theorem feq3d 5927
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 5923 . 2 (𝐴 = 𝐵 → (𝐹:𝑋𝐴𝐹:𝑋𝐵))
31, 2syl 17 1 (𝜑 → (𝐹:𝑋𝐴𝐹:𝑋𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wf 5782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-in 3542  df-ss 3549  df-f 5790
This theorem is referenced by:  feq123d  5929  fsn2  6290  fsng  6291  fsnunf  6330  funcres2b  16322  funcres2  16323  funcres2c  16326  catciso  16522  hofcl  16664  yonedalem4c  16682  yonedalem3b  16684  yonedainv  16686  gsumress  17041  resmhm2b  17126  pwsdiagmhm  17134  frmdup3lem  17168  frmdup3  17169  isghm  17425  frgpup3lem  17955  gsumzsubmcl  18083  dmdprd  18162  frlmup2  19895  scmatghm  20096  scmatmhm  20097  mdetdiaglem  20161  cnpf2  20802  2ndcctbss  21006  1stcelcls  21012  uptx  21176  txcn  21177  tsmssubm  21694  cnextucn  21855  pi1addf  22582  caufval  22795  equivcau  22820  lmcau  22832  plypf1  23685  coef2  23704  ulmval  23851  uhgrac  25596  ajfval  26850  chscllem4  27685  rrhf  29172  sibff  29527  sibfof  29531  orvcval4  29651  bj-finsumval0  32123  matunitlindflem2  32375  poimirlem9  32387  isbnd3  32552  prdsbnd  32561  heibor  32589  elghomlem1OLD  32653  cnfsmf  39427  uhgr0vb  40295  uhgrun  40297  uhgrstrrepe  40302  isumgrs  40319  upgrun  40341  umgrun  40343  1wlksfval  40809  wlksfval  40810  1wlkres  40877  resmgmhm2b  41588  zrtermorngc  41791  zrtermoringc  41860
  Copyright terms: Public domain W3C validator