Theorem feq2d 6570

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ⟶wf 6414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-fn 6421  df-f 6422

This theorem is referenced by:  feq12d  6572  fco  6608  ffdm  6614  fsng  6991  fsn2g  6992  fsnunf2  7040  issmo2  8151  qliftf  8552  elpm2r  8591  ralxpmap  8642  axdc3lem3  10139  axdc3lem4  10140  fseq1p1m1  13259  fseq1m1p1  13260  seqf1o  13692  iswrdi  14149  wrdf  14150  wrdffz  14166  ffz0iswrd  14172  wrdnval  14176  ccatalpha  14226  swrdf  14291  swrdwrdsymb  14303  cats1un  14362  cshwf  14441  wrdlen2i  14583  wwlktovf  14599  rlimi  15150  rlimmptrcl  15245  lo1mptrcl  15259  o1mptrcl  15260  o1fsum  15453  ram0  16651  funcres  17527  curf2cl  17865  uncfcurf  17873  yonedalem4c  17911  intopsn  18253  gsumprval  18287  resmhm  18374  gsumwsubmcl  18390  gsumsgrpccat  18393  gsumccatOLD  18394  gsumwmhm  18399  frmdup1  18418  frmdup3lem  18420  isghm  18749  resghm  18765  subgga  18821  gasubg  18823  psgnunilem2  19018  sylow2blem2  19141  pj2f  19219  pj1ghm  19224  frgpupf  19294  frgpup3lem  19298  gsumval3  19423  gsummptfzcl  19485  dprdf2  19525  ablfac2  19607  isabvd  19995  abvpropd  20017  cygznlem2a  20687  frgpcyg  20693  mplasclf  21183  evlssca  21209  lply1binomsc  21388  mat1dimelbas  21528  mat2pmatbas  21783  cpmadugsumlemF  21933  cnpf2  22309  ptpjcn  22670  cnextfres1  23127  cnextfres  23128  cnmpopc  23997  pi1addf  24116  pi1xfrf  24122  pi1cof  24128  mbfmptcl  24705  iblcnlem  24858  limcres  24955  cnplimc  24956  limccnp  24960  limccnp2  24961  limcun  24964  dvidlem  24984  cpnord  25004  dvaddf  25011  dvmulf  25012  dvcmulf  25014  dvcof  25017  dvcj  25019  dvrec  25024  dvmptcl  25028  dvcnvlem  25045  dvcnv  25046  rolle  25059  cmvth  25060  mvth  25061  dvlip  25062  dvlipcn  25063  c1lip2  25067  dv11cn  25070  dvivthlem1  25077  dvivthlem2  25078  dvivth  25079  dvne0  25080  lhop1lem  25082  lhop1  25083  lhop2  25084  lhop  25085  dvcnvrelem2  25087  taylthlem1  25437  taylthlem2  25438  ulmf2  25448  ulm2  25449  ulmdv  25467  pserdv  25493  rlimcxp  26028  o1cxp  26029  dchrptlem2  26318  axlowdimlem5  27217  axlowdimlem7  27219  axlowdimlem10  27222  uhgrn0  27340  wrdupgr  27358  upgrfn  27360  wrdumgr  27370  umgrfn  27372  upgr2wlk  27938  wlkres  27940  redwlklem  27941  wlkdlem1  27952  uhgrwkspthlem2  28023  usgr2wlkneq  28025  usgr2pthlem  28032  usgr2pth  28033  crctcshwlkn0  28087  wlkiswwlks2lem3  28137  wlkiswwlks2  28141  wlkiswwlksupgr2  28143  wlknewwlksn  28153  wpthswwlks2on  28227  clwlkclwwlklem2a  28263  clwlkclwwlklem1  28264  1wlkdlem1  28402  upgr3v3e3cycl  28445  upgr4cycl4dv4e  28450  isgrpo  28760  vciOLD  28824  isvclem  28840  isnvlem  28873  ajfval  29072  acunirnmpt2  30899  acunirnmpt2f  30900  wrdfd  31112  elrspunidl  31508  lbsdiflsp0  31609  smatrcl  31648  locfinref  31693  1stmbfm  32127  2ndmbfm  32128  sibfof  32207  rrvf2  32315  signshf  32467  reprsuc  32495  pfxwlk  32985  revwlk  32986  cvmliftmolem1  33143  cvmliftlem7  33153  cvmliftlem10  33156  cvmlift2lem9  33173  filnetlem4  34497  poimirlem16  35720  poimirlem19  35723  poimirlem23  35727  poimirlem24  35728  poimirlem25  35729  poimirlem29  35733  poimirlem31  35735  sdclem2  35827  sdclem1  35828  sdc  35829  fdc  35830  sstotbnd2  35859  elghomlem1OLD  35970  rngosn3  36009  sticksstones9  40038  sticksstones11  40040  sticksstones16  40046  frlmfzowrdb  40161  amgm4d  41700  mnurnd  41790  mptelpm  42601  fsneqrn  42640  cncfuni  43317  cncfiooicclem1  43324  dvsubf  43345  dvdivf  43353  dvbdfbdioolem1  43359  ioodvbdlimc1lem1  43362  ioodvbdlimc1lem2  43363  ioodvbdlimc1  43364  ioodvbdlimc2lem  43365  ioodvbdlimc2  43366  dvnprodlem3  43379  itgsubsticclem  43406  fourierdlem48  43585  fourierdlem49  43586  fourierdlem58  43595  fourierdlem59  43596  fourierdlem60  43597  fourierdlem61  43598  fourierdlem69  43606  fourierdlem75  43612  fourierdlem81  43618  fourierdlem89  43626  fourierdlem91  43628  fourierdlem97  43634  fourierdlem113  43650  meaf  43881  ismeannd  43895  psmeasure  43899  omef  43924  isomennd  43959  hoidmvlelem2  44024  hoidmvlelem3  44025  ovnhoi  44031  hspmbllem2  44055  sssmf  44161  smfpimioompt  44207  smffmpt  44225  2ffzoeq  44708  fundcmpsurbijinjpreimafv  44747  fargshiftf  44780  resmgmhm  45240  elbigolo1  45791  naryfvalelwrdf  45867  0aryfvalel  45868