Theorem feq2d 6641

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 6636	. 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))

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

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 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-fn 6490  df-f 6491

This theorem is referenced by:  feq2dd  6643  feq12d  6645  fco  6681  ffdm  6686  fsng  7076  fsn2g  7077  fsnunf2  7126  issmo2  8275  qliftf  8735  elpm2r  8775  ralxpmap  8826  axdc3lem3  10349  axdc3lem4  10350  fseq1p1m1  13504  fseq1m1p1  13505  seqf1o  13956  iswrdi  14430  wrdf  14431  wrdfd  14432  wrdffz  14448  ffz0iswrd  14454  wrdnval  14458  ccatalpha  14507  swrdf  14564  swrdwrdsymb  14576  cats1un  14634  cshwf  14713  wrdlen2i  14855  wwlktovf  14869  rlimi  15426  rlimmptrcl  15521  lo1mptrcl  15535  o1mptrcl  15536  o1fsum  15726  ram0  16940  funcres  17809  curf2cl  18143  uncfcurf  18151  yonedalem4c  18189  intopsn  18568  gsumprval  18602  resmgmhm  18625  resmhm  18734  gsumwsubmcl  18751  gsumsgrpccat  18754  gsumwmhm  18759  frmdup1  18778  frmdup3lem  18780  isghmOLD  19134  resghm  19150  subgga  19218  gasubg  19220  psgnunilem2  19413  sylow2blem2  19539  pj2f  19616  pj1ghm  19621  frgpupf  19691  frgpup3lem  19695  gsumval3  19825  gsummptfzcl  19887  dprdf2  19927  ablfac2  20009  isabvd  20733  abvpropd  20756  cygznlem2a  21510  frgpcyg  21516  psrasclcl  21923  mplasclf  22006  evlssca  22030  lply1binomsc  22232  mat1dimelbas  22392  mat2pmatbas  22647  cpmadugsumlemF  22797  cnpf2  23171  ptpjcn  23532  cnextfres1  23989  cnextfres  23990  cnmpopc  24855  pi1addf  24980  pi1xfrf  24986  pi1cof  24992  mbfmptcl  25570  iblcnlem  25723  limcres  25820  cnplimc  25821  limccnp  25825  limccnp2  25826  limcun  25829  dvidlem  25849  cpnord  25870  dvaddf  25878  dvmulf  25879  dvcmulf  25881  dvcof  25885  dvcj  25887  dvrec  25892  dvmptcl  25896  dvcnvlem  25913  dvcnv  25914  rolle  25927  cmvth  25928  cmvthOLD  25929  mvth  25930  dvlip  25931  dvlipcn  25932  c1lip2  25936  dv11cn  25939  dvivthlem1  25946  dvivthlem2  25947  dvivth  25948  dvne0  25949  lhop1lem  25951  lhop1  25952  lhop2  25953  lhop  25954  dvcnvrelem2  25956  taylthlem1  26314  taylthlem2  26315  taylthlem2OLD  26316  ulmf2  26326  ulm2  26327  ulmdv  26345  pserdv  26372  rlimcxp  26917  o1cxp  26918  dchrptlem2  27209  axlowdimlem5  28931  axlowdimlem7  28933  axlowdimlem10  28936  uhgrn0  29052  wrdupgr  29070  upgrfn  29072  wrdumgr  29082  umgrfn  29084  upgr2wlk  29652  wlkres  29654  redwlklem  29655  wlkdlem1  29666  uhgrwkspthlem2  29739  usgr2wlkneq  29741  usgr2pthlem  29748  usgr2pth  29749  crctcshwlkn0  29806  wlkiswwlks2lem3  29856  wlkiswwlks2  29860  wlkiswwlksupgr2  29862  wlknewwlksn  29872  wpthswwlks2on  29949  clwlkclwwlklem2a  29985  clwlkclwwlklem1  29986  1wlkdlem1  30124  upgr3v3e3cycl  30167  upgr4cycl4dv4e  30172  isgrpo  30484  vciOLD  30548  isvclem  30564  isnvlem  30597  ajfval  30796  acunirnmpt2  32649  acunirnmpt2f  32650  elrspunidl  33400  lbsdiflsp0  33646  smatrcl  33816  locfinref  33861  1stmbfm  34280  2ndmbfm  34281  sibfof  34360  rrvf2  34468  signshf  34608  reprsuc  34635  pfxwlk  35175  revwlk  35176  cvmliftmolem1  35332  cvmliftlem7  35342  cvmliftlem10  35345  cvmlift2lem9  35362  filnetlem4  36432  poimirlem16  37682  poimirlem19  37685  poimirlem23  37689  poimirlem24  37690  poimirlem25  37691  poimirlem29  37695  poimirlem31  37697  sdclem2  37788  sdclem1  37789  sdc  37790  fdc  37791  sstotbnd2  37820  elghomlem1OLD  37931  rngosn3  37970  sticksstones9  42253  sticksstones11  42255  sticksstones16  42261  frlmfzowrdb  42603  evlselvlem  42685  evlselv  42686  ofoafg  43452  amgm4d  44298  mnurnd  44381  mptelpm  45278  fsneqrn  45313  cncfuni  45989  cncfiooicclem1  45996  dvsubf  46017  dvdivf  46025  dvbdfbdioolem1  46031  ioodvbdlimc1lem1  46034  ioodvbdlimc1lem2  46035  ioodvbdlimc1  46036  ioodvbdlimc2lem  46037  ioodvbdlimc2  46038  dvnprodlem3  46051  itgsubsticclem  46078  fourierdlem48  46257  fourierdlem49  46258  fourierdlem58  46267  fourierdlem59  46268  fourierdlem60  46269  fourierdlem61  46270  fourierdlem69  46278  fourierdlem75  46284  fourierdlem81  46290  fourierdlem89  46298  fourierdlem91  46300  fourierdlem97  46306  fourierdlem113  46322  meaf  46556  ismeannd  46570  psmeasure  46574  omef  46599  isomennd  46634  hoidmvlelem2  46699  hoidmvlelem3  46700  ovnhoi  46706  hspmbllem2  46730  sssmf  46841  smfpimioompt  46889  smffmptf  46907  chnsubseqword  46981  2ffzoeq  47432  fundcmpsurbijinjpreimafv  47512  fargshiftf  47545  upgrimwlklem2  48003  upgrimwlklem4  48005  upgrimpths  48014  gpgprismgr4cycllem9  48208  elbigolo1  48663  naryfvalelwrdf  48739  0aryfvalel  48740  0funcg2  49190  termcfuncval  49638