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

Theorem feq3d 6070
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 6066 . 2 (𝐴 = 𝐵 → (𝐹:𝑋𝐴𝐹:𝑋𝐵))
31, 2syl 17 1 (𝜑 → (𝐹:𝑋𝐴𝐹:𝑋𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  wf 5922
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621  df-f 5930
This theorem is referenced by:  feq123d  6072  fsn2  6443  fsng  6444  fsnunf  6492  funcres2b  16604  funcres2  16605  funcres2c  16608  catciso  16804  hofcl  16946  yonedalem4c  16964  yonedalem3b  16966  yonedainv  16968  gsumress  17323  resmhm2b  17408  pwsdiagmhm  17416  frmdup3lem  17450  frmdup3  17451  isghm  17707  frgpup3lem  18236  gsumzsubmcl  18364  dmdprd  18443  frlmup2  20186  scmatghm  20387  scmatmhm  20388  mdetdiaglem  20452  cnpf2  21102  2ndcctbss  21306  1stcelcls  21312  uptx  21476  txcn  21477  tsmssubm  21993  cnextucn  22154  pi1addf  22893  caufval  23119  equivcau  23144  lmcau  23157  plypf1  24013  coef2  24032  ulmval  24179  uhgr0vb  26012  uhgrun  26014  uhgrstrrepe  26018  isumgrs  26036  upgrun  26058  umgrun  26060  wksfval  26561  wlkres  26623  ajfval  27792  chscllem4  28627  rrhf  30170  sibff  30526  sibfof  30530  orvcval4  30650  bj-finsumval0  33277  matunitlindflem2  33536  poimirlem9  33548  isbnd3  33713  prdsbnd  33722  heibor  33750  elghomlem1OLD  33814  cnfsmf  41270  upwlksfval  42041  resmgmhm2b  42125  zrtermorngc  42326  zrtermoringc  42395
  Copyright terms: Public domain W3C validator