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 207   = wceq 1547  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-fn 6495  df-f 6496

This theorem is referenced by:  feq2dd  6648  feq12d  6650  fco  6686  ffdm  6691  fsng  7086  fsn2g  7087  fsnunf2  7137  issmo2  8286  qliftf  8749  elpm2r  8789  ralxpmap  8841  axdc3lem3  10372  axdc3lem4  10373  fseq1p1m1  13550  fseq1m1p1  13551  seqf1o  14003  iswrdi  14477  wrdf  14478  wrdfd  14479  wrdffz  14495  ffz0iswrd  14501  wrdnval  14505  ccatalpha  14554  swrdf  14611  swrdwrdsymb  14623  cats1un  14681  cshwf  14760  wrdlen2i  14902  wwlktovf  14916  rlimi  15473  rlimmptrcl  15568  lo1mptrcl  15582  o1mptrcl  15583  o1fsum  15774  ram0  16991  funcres  17861  curf2cl  18195  uncfcurf  18203  yonedalem4c  18241  intopsn  18620  gsumprval  18654  resmgmhm  18677  resmhm  18786  gsumwsubmcl  18803  gsumsgrpccat  18806  gsumwmhm  18811  frmdup1  18830  frmdup3lem  18832  isghmOLD  19189  resghm  19205  subgga  19273  gasubg  19275  psgnunilem2  19468  sylow2blem2  19594  pj2f  19671  pj1ghm  19676  frgpupf  19746  frgpup3lem  19750  gsumval3  19880  gsummptfzcl  19942  dprdf2  19982  ablfac2  20064  isabvd  20791  abvpropd  20814  cygznlem2a  21549  frgpcyg  21555  psrasclcl  21961  mplasclf  22048  evlssca  22077  lply1binomsc  22304  mat1dimelbas  22461  mat2pmatbas  22716  cpmadugsumlemF  22866  cnpf2  23240  ptpjcn  23601  cnextfres1  24058  cnextfres  24059  cnmpopc  24920  pi1addf  25039  pi1xfrf  25045  pi1cof  25051  mbfmptcl  25628  iblcnlem  25781  limcres  25878  cnplimc  25879  limccnp  25883  limccnp2  25884  limcun  25887  dvidlem  25907  cpnord  25927  dvaddf  25934  dvmulf  25935  dvcmulf  25937  dvcof  25940  dvcj  25942  dvrec  25947  dvmptcl  25951  dvcnvlem  25968  dvcnv  25969  rolle  25982  cmvth  25983  mvth  25984  dvlip  25985  dvlipcn  25986  c1lip2  25990  dv11cn  25993  dvivthlem1  26000  dvivthlem2  26001  dvivth  26002  dvne0  26003  lhop1lem  26005  lhop1  26006  lhop2  26007  lhop  26008  dvcnvrelem2  26010  taylthlem1  26363  taylthlem2  26364  ulmf2  26374  ulm2  26375  ulmdv  26393  pserdv  26419  rlimcxp  26962  o1cxp  26963  dchrptlem2  27253  axlowdimlem5  29040  axlowdimlem7  29042  axlowdimlem10  29045  uhgrn0  29161  wrdupgr  29179  upgrfn  29181  wrdumgr  29191  umgrfn  29193  upgr2wlk  29760  wlkres  29762  redwlklem  29763  wlkdlem1  29774  uhgrwkspthlem2  29847  usgr2wlkneq  29849  usgr2pthlem  29856  usgr2pth  29857  crctcshwlkn0  29914  wlkiswwlks2lem3  29964  wlkiswwlks2  29968  wlkiswwlksupgr2  29970  wlknewwlksn  29980  wpthswwlks2on  30057  clwlkclwwlklem2a  30093  clwlkclwwlklem1  30094  1wlkdlem1  30232  upgr3v3e3cycl  30275  upgr4cycl4dv4e  30280  isgrpo  30593  vciOLD  30657  isvclem  30673  isnvlem  30706  ajfval  30905  acunirnmpt2  32759  acunirnmpt2f  32760  elrspunidl  33518  lbsdiflsp0  33817  smatrcl  33987  locfinref  34032  1stmbfm  34451  2ndmbfm  34452  sibfof  34531  rrvf2  34639  signshf  34779  reprsuc  34806  pfxwlk  35359  revwlk  35360  cvmliftmolem1  35516  cvmliftlem7  35526  cvmliftlem10  35529  cvmlift2lem9  35546  filnetlem4  36616  poimirlem16  38010  poimirlem19  38013  poimirlem23  38017  poimirlem24  38018  poimirlem25  38019  poimirlem29  38023  poimirlem31  38025  sdclem2  38116  sdclem1  38117  sdc  38118  fdc  38119  sstotbnd2  38148  elghomlem1OLD  38259  rngosn3  38298  sticksstones9  42646  sticksstones11  42648  sticksstones16  42654  frlmfzowrdb  43001  evlselvlem  43045  evlselv  43046  ofoafg  43806  amgm4d  44651  mnurnd  44734  mptelpm  45630  fsneqrn  45663  cncfuni  46336  cncfiooicclem1  46343  dvsubf  46364  dvdivf  46372  dvbdfbdioolem1  46378  ioodvbdlimc1lem1  46381  ioodvbdlimc1lem2  46382  ioodvbdlimc1  46383  ioodvbdlimc2lem  46384  ioodvbdlimc2  46385  dvnprodlem3  46398  itgsubsticclem  46425  fourierdlem48  46604  fourierdlem49  46605  fourierdlem58  46614  fourierdlem59  46615  fourierdlem60  46616  fourierdlem61  46617  fourierdlem69  46625  fourierdlem75  46631  fourierdlem81  46637  fourierdlem89  46645  fourierdlem91  46647  fourierdlem97  46653  fourierdlem113  46669  meaf  46903  ismeannd  46917  psmeasure  46921  omef  46946  isomennd  46981  hoidmvlelem2  47046  hoidmvlelem3  47047  ovnhoi  47053  hspmbllem2  47077  sssmf  47188  smfpimioompt  47236  smffmptf  47254  chnsubseqword  47330  2ffzoeq  47798  fundcmpsurbijinjpreimafv  47889  fargshiftf  47922  upgrimwlklem2  48396  upgrimwlklem4  48398  upgrimpths  48407  gpgprismgr4cycllem9  48601  elbigolo1  49055  naryfvalelwrdf  49131  0aryfvalel  49132  0funcg2  49581  termcfuncval  50029