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

Theorem feq3d 6494
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 6490 . 2 (𝐴 = 𝐵 → (𝐹:𝑋𝐴𝐹:𝑋𝐵))
31, 2syl 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