Theorem feq2d 6694

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1533  ⟶wf 6530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-cleq 2716  df-fn 6537  df-f 6538

This theorem is referenced by:  feq12d  6696  fco  6732  ffdm  6738  fsng  7128  fsn2g  7129  fsnunf2  7177  issmo2  8345  qliftf  8796  elpm2r  8836  ralxpmap  8887  axdc3lem3  10444  axdc3lem4  10445  fseq1p1m1  13573  fseq1m1p1  13574  seqf1o  14007  iswrdi  14466  wrdf  14467  wrdffz  14483  ffz0iswrd  14489  wrdnval  14493  ccatalpha  14541  swrdf  14598  swrdwrdsymb  14610  cats1un  14669  cshwf  14748  wrdlen2i  14891  wwlktovf  14905  rlimi  15455  rlimmptrcl  15550  lo1mptrcl  15564  o1mptrcl  15565  o1fsum  15757  ram0  16956  funcres  17847  curf2cl  18188  uncfcurf  18196  yonedalem4c  18234  intopsn  18579  gsumprval  18613  resmgmhm  18636  resmhm  18737  gsumwsubmcl  18754  gsumsgrpccat  18757  gsumwmhm  18762  frmdup1  18781  frmdup3lem  18783  isghm  19133  resghm  19149  subgga  19208  gasubg  19210  psgnunilem2  19407  sylow2blem2  19533  pj2f  19610  pj1ghm  19615  frgpupf  19685  frgpup3lem  19689  gsumval3  19819  gsummptfzcl  19881  dprdf2  19921  ablfac2  20003  isabvd  20655  abvpropd  20677  cygznlem2a  21432  frgpcyg  21438  mplasclf  21938  evlssca  21964  lply1binomsc  22154  mat1dimelbas  22297  mat2pmatbas  22552  cpmadugsumlemF  22702  cnpf2  23078  ptpjcn  23439  cnextfres1  23896  cnextfres  23897  cnmpopc  24773  pi1addf  24898  pi1xfrf  24904  pi1cof  24910  mbfmptcl  25489  iblcnlem  25642  limcres  25739  cnplimc  25740  limccnp  25744  limccnp2  25745  limcun  25748  dvidlem  25768  cpnord  25789  dvaddf  25797  dvmulf  25798  dvcmulf  25800  dvcof  25804  dvcj  25806  dvrec  25811  dvmptcl  25815  dvcnvlem  25832  dvcnv  25833  rolle  25846  cmvth  25847  cmvthOLD  25848  mvth  25849  dvlip  25850  dvlipcn  25851  c1lip2  25855  dv11cn  25858  dvivthlem1  25865  dvivthlem2  25866  dvivth  25867  dvne0  25868  lhop1lem  25870  lhop1  25871  lhop2  25872  lhop  25873  dvcnvrelem2  25875  taylthlem1  26228  taylthlem2  26229  ulmf2  26239  ulm2  26240  ulmdv  26258  pserdv  26285  rlimcxp  26825  o1cxp  26826  dchrptlem2  27117  axlowdimlem5  28676  axlowdimlem7  28678  axlowdimlem10  28681  uhgrn0  28799  wrdupgr  28817  upgrfn  28819  wrdumgr  28829  umgrfn  28831  upgr2wlk  29397  wlkres  29399  redwlklem  29400  wlkdlem1  29411  uhgrwkspthlem2  29483  usgr2wlkneq  29485  usgr2pthlem  29492  usgr2pth  29493  crctcshwlkn0  29547  wlkiswwlks2lem3  29597  wlkiswwlks2  29601  wlkiswwlksupgr2  29603  wlknewwlksn  29613  wpthswwlks2on  29687  clwlkclwwlklem2a  29723  clwlkclwwlklem1  29724  1wlkdlem1  29862  upgr3v3e3cycl  29905  upgr4cycl4dv4e  29910  isgrpo  30222  vciOLD  30286  isvclem  30302  isnvlem  30335  ajfval  30534  acunirnmpt2  32357  acunirnmpt2f  32358  wrdfd  32572  elrspunidl  33018  lbsdiflsp0  33193  smatrcl  33268  locfinref  33313  1stmbfm  33751  2ndmbfm  33752  sibfof  33831  rrvf2  33939  signshf  34091  reprsuc  34118  pfxwlk  34605  revwlk  34606  cvmliftmolem1  34763  cvmliftlem7  34773  cvmliftlem10  34776  cvmlift2lem9  34793  gg-taylthlem2  35658  filnetlem4  35757  poimirlem16  36998  poimirlem19  37001  poimirlem23  37005  poimirlem24  37006  poimirlem25  37007  poimirlem29  37011  poimirlem31  37013  sdclem2  37104  sdclem1  37105  sdc  37106  fdc  37107  sstotbnd2  37136  elghomlem1OLD  37247  rngosn3  37286  sticksstones9  41467  sticksstones11  41469  sticksstones16  41475  frlmfzowrdb  41575  evlselvlem  41651  evlselv  41652  ofoafg  42618  amgm4d  43466  mnurnd  43556  mptelpm  44385  fsneqrn  44420  cncfuni  45112  cncfiooicclem1  45119  dvsubf  45140  dvdivf  45148  dvbdfbdioolem1  45154  ioodvbdlimc1lem1  45157  ioodvbdlimc1lem2  45158  ioodvbdlimc1  45159  ioodvbdlimc2lem  45160  ioodvbdlimc2  45161  dvnprodlem3  45174  itgsubsticclem  45201  fourierdlem48  45380  fourierdlem49  45381  fourierdlem58  45390  fourierdlem59  45391  fourierdlem60  45392  fourierdlem61  45393  fourierdlem69  45401  fourierdlem75  45407  fourierdlem81  45413  fourierdlem89  45421  fourierdlem91  45423  fourierdlem97  45429  fourierdlem113  45445  meaf  45679  ismeannd  45693  psmeasure  45697  omef  45722  isomennd  45757  hoidmvlelem2  45822  hoidmvlelem3  45823  ovnhoi  45829  hspmbllem2  45853  sssmf  45964  smfpimioompt  46012  smffmptf  46030  2ffzoeq  46546  fundcmpsurbijinjpreimafv  46585  fargshiftf  46618  elbigolo1  47456  naryfvalelwrdf  47532  0aryfvalel  47533