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

Theorem feq3d 6241
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 6237 . 2 (𝐴 = 𝐵 → (𝐹:𝑋𝐴𝐹:𝑋𝐵))
31, 2syl 17 1 (𝜑 → (𝐹:𝑋𝐴𝐹:𝑋𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198   = wceq 1653  wf 6095
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2775
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-in 3774  df-ss 3781  df-f 6103
This theorem is referenced by:  feq123d  6243  fsn2  6628  fsng  6629  fsnunf  6678  funcres2b  16868  funcres2  16869  funcres2c  16872  catciso  17068  hofcl  17211  yonedalem4c  17229  yonedalem3b  17231  yonedainv  17233  gsumress  17588  resmhm2b  17673  pwsdiagmhm  17681  frmdup3lem  17716  frmdup3  17717  isghm  17970  frgpup3lem  18502  gsumzsubmcl  18630  dmdprd  18710  frlmup2  20460  scmatghm  20662  scmatmhm  20663  mdetdiaglem  20727  cnpf2  21380  2ndcctbss  21584  1stcelcls  21590  uptx  21754  txcn  21755  tsmssubm  22271  cnextucn  22432  pi1addf  23171  caufval  23398  equivcau  23423  lmcau  23436  plypf1  24306  coef2  24325  ulmval  24472  uhgr0vb  26299  uhgrun  26301  uhgrstrrepe  26305  isumgrs  26323  upgrun  26345  umgrun  26347  wksfval  26851  wlkres  26913  wlkresOLD  26915  ajfval  28181  chscllem4  29016  rrhf  30550  sibff  30906  sibfof  30910  orvcval4  31031  bj-finsumval0  33638  matunitlindflem2  33887  poimirlem9  33899  isbnd3  34062  prdsbnd  34071  heibor  34099  elghomlem1OLD  34163  cnfsmf  41683  upwlksfval  42503  resmgmhm2b  42587  zrtermorngc  42788  zrtermoringc  42857
  Copyright terms: Public domain W3C validator