Theorem feq2d 6646

Description: Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
feq2d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
feq2d	⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))

Proof of Theorem feq2d

Step	Hyp	Ref	Expression
1		feq2d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		feq2 6641	. 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-fn 6495  df-f 6496

This theorem is referenced by:  feq2dd  6648  feq12d  6650  fco  6686  ffdm  6691  fsng  7082  fsn2g  7083  fsnunf2  7132  issmo2  8281  qliftf  8742  elpm2r  8782  ralxpmap  8834  axdc3lem3  10362  axdc3lem4  10363  fseq1p1m1  13514  fseq1m1p1  13515  seqf1o  13966  iswrdi  14440  wrdf  14441  wrdfd  14442  wrdffz  14458  ffz0iswrd  14464  wrdnval  14468  ccatalpha  14517  swrdf  14574  swrdwrdsymb  14586  cats1un  14644  cshwf  14723  wrdlen2i  14865  wwlktovf  14879  rlimi  15436  rlimmptrcl  15531  lo1mptrcl  15545  o1mptrcl  15546  o1fsum  15736  ram0  16950  funcres  17820  curf2cl  18154  uncfcurf  18162  yonedalem4c  18200  intopsn  18579  gsumprval  18613  resmgmhm  18636  resmhm  18745  gsumwsubmcl  18762  gsumsgrpccat  18765  gsumwmhm  18770  frmdup1  18789  frmdup3lem  18791  isghmOLD  19145  resghm  19161  subgga  19229  gasubg  19231  psgnunilem2  19424  sylow2blem2  19550  pj2f  19627  pj1ghm  19632  frgpupf  19702  frgpup3lem  19706  gsumval3  19836  gsummptfzcl  19898  dprdf2  19938  ablfac2  20020  isabvd  20745  abvpropd  20768  cygznlem2a  21522  frgpcyg  21528  psrasclcl  21935  mplasclf  22020  evlssca  22049  lply1binomsc  22255  mat1dimelbas  22415  mat2pmatbas  22670  cpmadugsumlemF  22820  cnpf2  23194  ptpjcn  23555  cnextfres1  24012  cnextfres  24013  cnmpopc  24878  pi1addf  25003  pi1xfrf  25009  pi1cof  25015  mbfmptcl  25593  iblcnlem  25746  limcres  25843  cnplimc  25844  limccnp  25848  limccnp2  25849  limcun  25852  dvidlem  25872  cpnord  25893  dvaddf  25901  dvmulf  25902  dvcmulf  25904  dvcof  25908  dvcj  25910  dvrec  25915  dvmptcl  25919  dvcnvlem  25936  dvcnv  25937  rolle  25950  cmvth  25951  cmvthOLD  25952  mvth  25953  dvlip  25954  dvlipcn  25955  c1lip2  25959  dv11cn  25962  dvivthlem1  25969  dvivthlem2  25970  dvivth  25971  dvne0  25972  lhop1lem  25974  lhop1  25975  lhop2  25976  lhop  25977  dvcnvrelem2  25979  taylthlem1  26337  taylthlem2  26338  taylthlem2OLD  26339  ulmf2  26349  ulm2  26350  ulmdv  26368  pserdv  26395  rlimcxp  26940  o1cxp  26941  dchrptlem2  27232  axlowdimlem5  29019  axlowdimlem7  29021  axlowdimlem10  29024  uhgrn0  29140  wrdupgr  29158  upgrfn  29160  wrdumgr  29170  umgrfn  29172  upgr2wlk  29740  wlkres  29742  redwlklem  29743  wlkdlem1  29754  uhgrwkspthlem2  29827  usgr2wlkneq  29829  usgr2pthlem  29836  usgr2pth  29837  crctcshwlkn0  29894  wlkiswwlks2lem3  29944  wlkiswwlks2  29948  wlkiswwlksupgr2  29950  wlknewwlksn  29960  wpthswwlks2on  30037  clwlkclwwlklem2a  30073  clwlkclwwlklem1  30074  1wlkdlem1  30212  upgr3v3e3cycl  30255  upgr4cycl4dv4e  30260  isgrpo  30572  vciOLD  30636  isvclem  30652  isnvlem  30685  ajfval  30884  acunirnmpt2  32738  acunirnmpt2f  32739  elrspunidl  33509  lbsdiflsp0  33783  smatrcl  33953  locfinref  33998  1stmbfm  34417  2ndmbfm  34418  sibfof  34497  rrvf2  34605  signshf  34745  reprsuc  34772  pfxwlk  35318  revwlk  35319  cvmliftmolem1  35475  cvmliftlem7  35485  cvmliftlem10  35488  cvmlift2lem9  35505  filnetlem4  36575  poimirlem16  37833  poimirlem19  37836  poimirlem23  37840  poimirlem24  37841  poimirlem25  37842  poimirlem29  37846  poimirlem31  37848  sdclem2  37939  sdclem1  37940  sdc  37941  fdc  37942  sstotbnd2  37971  elghomlem1OLD  38082  rngosn3  38121  sticksstones9  42404  sticksstones11  42406  sticksstones16  42412  frlmfzowrdb  42755  evlselvlem  42825  evlselv  42826  ofoafg  43592  amgm4d  44437  mnurnd  44520  mptelpm  45416  fsneqrn  45451  cncfuni  46126  cncfiooicclem1  46133  dvsubf  46154  dvdivf  46162  dvbdfbdioolem1  46168  ioodvbdlimc1lem1  46171  ioodvbdlimc1lem2  46172  ioodvbdlimc1  46173  ioodvbdlimc2lem  46174  ioodvbdlimc2  46175  dvnprodlem3  46188  itgsubsticclem  46215  fourierdlem48  46394  fourierdlem49  46395  fourierdlem58  46404  fourierdlem59  46405  fourierdlem60  46406  fourierdlem61  46407  fourierdlem69  46415  fourierdlem75  46421  fourierdlem81  46427  fourierdlem89  46435  fourierdlem91  46437  fourierdlem97  46443  fourierdlem113  46459  meaf  46693  ismeannd  46707  psmeasure  46711  omef  46736  isomennd  46771  hoidmvlelem2  46836  hoidmvlelem3  46837  ovnhoi  46843  hspmbllem2  46867  sssmf  46978  smfpimioompt  47026  smffmptf  47044  chnsubseqword  47118  2ffzoeq  47569  fundcmpsurbijinjpreimafv  47649  fargshiftf  47682  upgrimwlklem2  48140  upgrimwlklem4  48142  upgrimpths  48151  gpgprismgr4cycllem9  48345  elbigolo1  48799  naryfvalelwrdf  48875  0aryfvalel  48876  0funcg2  49325  termcfuncval  49773