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 208   = wceq 1530  wf 6344
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-in 3941  df-ss 3950  df-f 6352
This theorem is referenced by:  feq123d  6496  fsn2  6891  fsng  6892  fsnunf  6940  funcres2b  17159  funcres2  17160  funcres2c  17163  catciso  17359  hofcl  17501  yonedalem4c  17519  yonedalem3b  17521  yonedainv  17523  gsumress  17884  resmhm2b  17979  pwsdiagmhm  17987  frmdup3lem  18023  frmdup3  18024  isghm  18350  frgpup3lem  18895  gsumzsubmcl  19030  dmdprd  19112  frlmup2  20935  scmatghm  21134  scmatmhm  21135  mdetdiaglem  21199  cnpf2  21850  2ndcctbss  22055  1stcelcls  22061  uptx  22225  txcn  22226  tsmssubm  22743  cnextucn  22904  pi1addf  23643  caufval  23870  equivcau  23895  lmcau  23908  plypf1  24794  coef2  24813  ulmval  24960  uhgr0vb  26849  uhgrun  26851  uhgrstrrepe  26855  isumgrs  26873  upgrun  26895  umgrun  26897  wksfval  27383  wlkres  27444  ajfval  28578  chscllem4  29409  lindfpropd  30935  fedgmullem1  31013  rrhf  31227  sibff  31582  sibfof  31586  orvcval4  31706  bj-finsumval0  34554  matunitlindflem2  34876  poimirlem9  34888  isbnd3  35049  prdsbnd  35058  heibor  35086  elghomlem1OLD  35150  selvval2lem4  39121  cnfsmf  43002  upwlksfval  43995  resmgmhm2b  44052  zrtermorngc  44257  zrtermoringc  44326
  Copyright terms: Public domain W3C validator