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

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