Theorem feq2d 6722

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ⟶wf 6557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-fn 6564  df-f 6565

This theorem is referenced by:  feq12d  6724  fco  6760  ffdm  6765  fsng  7157  fsn2g  7158  fsnunf2  7206  issmo2  8389  qliftf  8845  elpm2r  8885  ralxpmap  8936  axdc3lem3  10492  axdc3lem4  10493  fseq1p1m1  13638  fseq1m1p1  13639  seqf1o  14084  iswrdi  14556  wrdf  14557  wrdffz  14573  ffz0iswrd  14579  wrdnval  14583  ccatalpha  14631  swrdf  14688  swrdwrdsymb  14700  cats1un  14759  cshwf  14838  wrdlen2i  14981  wwlktovf  14995  rlimi  15549  rlimmptrcl  15644  lo1mptrcl  15658  o1mptrcl  15659  o1fsum  15849  ram0  17060  funcres  17941  curf2cl  18276  uncfcurf  18284  yonedalem4c  18322  intopsn  18667  gsumprval  18701  resmgmhm  18724  resmhm  18833  gsumwsubmcl  18850  gsumsgrpccat  18853  gsumwmhm  18858  frmdup1  18877  frmdup3lem  18879  isghmOLD  19234  resghm  19250  subgga  19318  gasubg  19320  psgnunilem2  19513  sylow2blem2  19639  pj2f  19716  pj1ghm  19721  frgpupf  19791  frgpup3lem  19795  gsumval3  19925  gsummptfzcl  19987  dprdf2  20027  ablfac2  20109  isabvd  20813  abvpropd  20836  cygznlem2a  21586  frgpcyg  21592  psrasclcl  22000  mplasclf  22089  evlssca  22113  lply1binomsc  22315  mat1dimelbas  22477  mat2pmatbas  22732  cpmadugsumlemF  22882  cnpf2  23258  ptpjcn  23619  cnextfres1  24076  cnextfres  24077  cnmpopc  24955  pi1addf  25080  pi1xfrf  25086  pi1cof  25092  mbfmptcl  25671  iblcnlem  25824  limcres  25921  cnplimc  25922  limccnp  25926  limccnp2  25927  limcun  25930  dvidlem  25950  cpnord  25971  dvaddf  25979  dvmulf  25980  dvcmulf  25982  dvcof  25986  dvcj  25988  dvrec  25993  dvmptcl  25997  dvcnvlem  26014  dvcnv  26015  rolle  26028  cmvth  26029  cmvthOLD  26030  mvth  26031  dvlip  26032  dvlipcn  26033  c1lip2  26037  dv11cn  26040  dvivthlem1  26047  dvivthlem2  26048  dvivth  26049  dvne0  26050  lhop1lem  26052  lhop1  26053  lhop2  26054  lhop  26055  dvcnvrelem2  26057  taylthlem1  26415  taylthlem2  26416  taylthlem2OLD  26417  ulmf2  26427  ulm2  26428  ulmdv  26446  pserdv  26473  rlimcxp  27017  o1cxp  27018  dchrptlem2  27309  axlowdimlem5  28961  axlowdimlem7  28963  axlowdimlem10  28966  uhgrn0  29084  wrdupgr  29102  upgrfn  29104  wrdumgr  29114  umgrfn  29116  upgr2wlk  29686  wlkres  29688  redwlklem  29689  wlkdlem1  29700  uhgrwkspthlem2  29774  usgr2wlkneq  29776  usgr2pthlem  29783  usgr2pth  29784  crctcshwlkn0  29841  wlkiswwlks2lem3  29891  wlkiswwlks2  29895  wlkiswwlksupgr2  29897  wlknewwlksn  29907  wpthswwlks2on  29981  clwlkclwwlklem2a  30017  clwlkclwwlklem1  30018  1wlkdlem1  30156  upgr3v3e3cycl  30199  upgr4cycl4dv4e  30204  isgrpo  30516  vciOLD  30580  isvclem  30596  isnvlem  30629  ajfval  30828  feq2dd  32632  acunirnmpt2  32670  acunirnmpt2f  32671  wrdfd  32918  elrspunidl  33456  lbsdiflsp0  33677  smatrcl  33795  locfinref  33840  1stmbfm  34262  2ndmbfm  34263  sibfof  34342  rrvf2  34450  signshf  34603  reprsuc  34630  pfxwlk  35129  revwlk  35130  cvmliftmolem1  35286  cvmliftlem7  35296  cvmliftlem10  35299  cvmlift2lem9  35316  filnetlem4  36382  poimirlem16  37643  poimirlem19  37646  poimirlem23  37650  poimirlem24  37651  poimirlem25  37652  poimirlem29  37656  poimirlem31  37658  sdclem2  37749  sdclem1  37750  sdc  37751  fdc  37752  sstotbnd2  37781  elghomlem1OLD  37892  rngosn3  37931  sticksstones9  42155  sticksstones11  42157  sticksstones16  42163  frlmfzowrdb  42514  evlselvlem  42596  evlselv  42597  ofoafg  43367  amgm4d  44213  mnurnd  44302  mptelpm  45181  fsneqrn  45216  cncfuni  45901  cncfiooicclem1  45908  dvsubf  45929  dvdivf  45937  dvbdfbdioolem1  45943  ioodvbdlimc1lem1  45946  ioodvbdlimc1lem2  45947  ioodvbdlimc1  45948  ioodvbdlimc2lem  45949  ioodvbdlimc2  45950  dvnprodlem3  45963  itgsubsticclem  45990  fourierdlem48  46169  fourierdlem49  46170  fourierdlem58  46179  fourierdlem59  46180  fourierdlem60  46181  fourierdlem61  46182  fourierdlem69  46190  fourierdlem75  46196  fourierdlem81  46202  fourierdlem89  46210  fourierdlem91  46212  fourierdlem97  46218  fourierdlem113  46234  meaf  46468  ismeannd  46482  psmeasure  46486  omef  46511  isomennd  46546  hoidmvlelem2  46611  hoidmvlelem3  46612  ovnhoi  46618  hspmbllem2  46642  sssmf  46753  smfpimioompt  46801  smffmptf  46819  2ffzoeq  47339  fundcmpsurbijinjpreimafv  47394  fargshiftf  47427  elbigolo1  48478  naryfvalelwrdf  48554  0aryfvalel  48555  0funcg2  48917