Theorem feq2d 6494

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1533  ⟶wf 6345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-fn 6352  df-f 6353

This theorem is referenced by:  feq12d  6496  ffdm  6530  fsng  6893  fsn2g  6894  fsnunf2  6942  issmo2  7980  qliftf  8379  elpm2r  8418  ralxpmap  8454  axdc3lem3  9868  axdc3lem4  9869  fseq1p1m1  12975  fseq1m1p1  12976  seqf1o  13405  iswrdi  13859  wrdf  13860  wrdffz  13879  ffz0iswrd  13885  ffz0iswrdOLD  13886  wrdnval  13890  ccatalpha  13941  swrdf  14006  swrdwrdsymb  14018  cats1un  14077  cshwf  14156  wrdlen2i  14298  wwlktovf  14314  rlimi  14864  rlimmptrcl  14958  lo1mptrcl  14972  o1mptrcl  14973  o1fsum  15162  ram0  16352  funcres  17160  curf2cl  17475  uncfcurf  17483  yonedalem4c  17521  intopsn  17858  gsumprval  17892  resmhm  17979  gsumwsubmcl  17995  gsumsgrpccat  17998  gsumccatOLD  17999  gsumwmhm  18004  frmdup1  18023  frmdup3lem  18025  isghm  18352  resghm  18368  subgga  18424  gasubg  18426  psgnunilem2  18617  sylow2blem2  18740  pj2f  18818  pj1ghm  18823  frgpupf  18893  frgpup3lem  18897  gsumval3  19021  gsummptfzcl  19083  dprdf2  19123  ablfac2  19205  isabvd  19585  abvpropd  19607  mplasclf  20271  evlssca  20296  lply1binomsc  20469  cygznlem2a  20708  frgpcyg  20714  mat1dimelbas  21074  mat2pmatbas  21328  cpmadugsumlemF  21478  cnpf2  21852  ptpjcn  22213  cnextfres1  22670  cnextfres  22671  cnmpopc  23526  pi1addf  23645  pi1xfrf  23651  pi1cof  23657  mbfmptcl  24231  iblcnlem  24383  limcres  24478  cnplimc  24479  limccnp  24483  limccnp2  24484  limcun  24487  dvidlem  24507  cpnord  24526  dvaddf  24533  dvmulf  24534  dvcmulf  24536  dvcof  24539  dvcj  24541  dvrec  24546  dvmptcl  24550  dvcnvlem  24567  dvcnv  24568  rolle  24581  cmvth  24582  mvth  24583  dvlip  24584  dvlipcn  24585  c1lip2  24589  dv11cn  24592  dvivthlem1  24599  dvivthlem2  24600  dvivth  24601  dvne0  24602  lhop1lem  24604  lhop1  24605  lhop2  24606  lhop  24607  dvcnvrelem2  24609  taylthlem1  24955  taylthlem2  24956  ulmf2  24966  ulm2  24967  ulmdv  24985  pserdv  25011  rlimcxp  25545  o1cxp  25546  dchrptlem2  25835  axlowdimlem5  26726  axlowdimlem7  26728  axlowdimlem10  26731  uhgrn0  26846  wrdupgr  26864  upgrfn  26866  wrdumgr  26876  umgrfn  26878  upgr2wlk  27444  wlkres  27446  redwlklem  27447  wlkdlem1  27458  uhgrwkspthlem2  27529  usgr2wlkneq  27531  usgr2pthlem  27538  usgr2pth  27539  crctcshwlkn0  27593  wlkiswwlks2lem3  27643  wlkiswwlks2  27647  wlkiswwlksupgr2  27649  wlknewwlksn  27659  wpthswwlks2on  27734  clwlkclwwlklem2a  27770  clwlkclwwlklem1  27771  1wlkdlem1  27910  upgr3v3e3cycl  27953  upgr4cycl4dv4e  27958  isgrpo  28268  vciOLD  28332  isvclem  28348  isnvlem  28381  ajfval  28580  acunirnmpt2  30399  acunirnmpt2f  30400  wrdfd  30607  lbsdiflsp0  31017  smatrcl  31056  locfinref  31100  1stmbfm  31513  2ndmbfm  31514  sibfof  31593  rrvf2  31701  signshf  31853  reprsuc  31881  pfxwlk  32365  revwlk  32366  cvmliftmolem1  32523  cvmliftlem7  32533  cvmliftlem10  32536  cvmlift2lem9  32553  filnetlem4  33724  poimirlem16  34902  poimirlem19  34905  poimirlem23  34909  poimirlem24  34910  poimirlem25  34911  poimirlem29  34915  poimirlem31  34917  sdclem2  35011  sdclem1  35012  sdc  35013  fdc  35014  sstotbnd2  35046  elghomlem1OLD  35157  rngosn3  35196  frlmfzowrdb  39136  amgm4d  40546  mnurnd  40612  mptelpm  41425  fsneqrn  41467  cncfuni  42162  cncfiooicclem1  42169  dvsubf  42191  dvdivf  42200  dvbdfbdioolem1  42206  ioodvbdlimc1lem1  42209  ioodvbdlimc1lem2  42210  ioodvbdlimc1  42211  ioodvbdlimc2lem  42212  ioodvbdlimc2  42213  dvnprodlem3  42226  itgsubsticclem  42253  fourierdlem48  42433  fourierdlem49  42434  fourierdlem58  42443  fourierdlem59  42444  fourierdlem60  42445  fourierdlem61  42446  fourierdlem69  42454  fourierdlem75  42460  fourierdlem81  42466  fourierdlem89  42474  fourierdlem91  42476  fourierdlem97  42482  fourierdlem113  42498  meaf  42729  ismeannd  42743  psmeasure  42747  omef  42772  isomennd  42807  hoidmvlelem2  42872  hoidmvlelem3  42873  ovnhoi  42879  hspmbllem2  42903  sssmf  43009  smfpimioompt  43055  smffmpt  43073  2ffzoeq  43522  fundcmpsurbijinjpreimafv  43561  fargshiftf  43594  resmgmhm  44059  elbigolo1  44611