Theorem feq2d 6493

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1531  ⟶wf 6344

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-9 2118  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775  df-cleq 2812  df-fn 6351  df-f 6352

This theorem is referenced by:  feq12d  6495  ffdm  6529  fsng  6892  fsn2g  6893  fsnunf2  6941  issmo2  7978  qliftf  8377  elpm2r  8416  ralxpmap  8452  axdc3lem3  9866  axdc3lem4  9867  fseq1p1m1  12973  fseq1m1p1  12974  seqf1o  13403  iswrdi  13857  wrdf  13858  wrdffz  13877  ffz0iswrd  13883  ffz0iswrdOLD  13884  wrdnval  13888  ccatalpha  13939  swrdf  14004  swrdwrdsymb  14016  cats1un  14075  cshwf  14154  wrdlen2i  14296  wwlktovf  14312  rlimi  14862  rlimmptrcl  14956  lo1mptrcl  14970  o1mptrcl  14971  o1fsum  15160  ram0  16350  funcres  17158  curf2cl  17473  uncfcurf  17481  yonedalem4c  17519  intopsn  17856  gsumprval  17890  resmhm  17977  gsumwsubmcl  17993  gsumsgrpccat  17996  gsumccatOLD  17997  gsumwmhm  18002  frmdup1  18021  frmdup3lem  18023  isghm  18350  resghm  18366  subgga  18422  gasubg  18424  psgnunilem2  18615  sylow2blem2  18738  pj2f  18816  pj1ghm  18821  frgpupf  18891  frgpup3lem  18895  gsumval3  19019  gsummptfzcl  19081  dprdf2  19121  ablfac2  19203  isabvd  19583  abvpropd  19605  mplasclf  20269  evlssca  20294  lply1binomsc  20467  cygznlem2a  20706  frgpcyg  20712  mat1dimelbas  21072  mat2pmatbas  21326  cpmadugsumlemF  21476  cnpf2  21850  ptpjcn  22211  cnextfres1  22668  cnextfres  22669  cnmpopc  23524  pi1addf  23643  pi1xfrf  23649  pi1cof  23655  mbfmptcl  24229  iblcnlem  24381  limcres  24476  cnplimc  24477  limccnp  24481  limccnp2  24482  limcun  24485  dvidlem  24505  cpnord  24524  dvaddf  24531  dvmulf  24532  dvcmulf  24534  dvcof  24537  dvcj  24539  dvrec  24544  dvmptcl  24548  dvcnvlem  24565  dvcnv  24566  rolle  24579  cmvth  24580  mvth  24581  dvlip  24582  dvlipcn  24583  c1lip2  24587  dv11cn  24590  dvivthlem1  24597  dvivthlem2  24598  dvivth  24599  dvne0  24600  lhop1lem  24602  lhop1  24603  lhop2  24604  lhop  24605  dvcnvrelem2  24607  taylthlem1  24953  taylthlem2  24954  ulmf2  24964  ulm2  24965  ulmdv  24983  pserdv  25009  rlimcxp  25543  o1cxp  25544  dchrptlem2  25833  axlowdimlem5  26724  axlowdimlem7  26726  axlowdimlem10  26729  uhgrn0  26844  wrdupgr  26862  upgrfn  26864  wrdumgr  26874  umgrfn  26876  upgr2wlk  27442  wlkres  27444  redwlklem  27445  wlkdlem1  27456  uhgrwkspthlem2  27527  usgr2wlkneq  27529  usgr2pthlem  27536  usgr2pth  27537  crctcshwlkn0  27591  wlkiswwlks2lem3  27641  wlkiswwlks2  27645  wlkiswwlksupgr2  27647  wlknewwlksn  27657  wpthswwlks2on  27732  clwlkclwwlklem2a  27768  clwlkclwwlklem1  27769  1wlkdlem1  27908  upgr3v3e3cycl  27951  upgr4cycl4dv4e  27956  isgrpo  28266  vciOLD  28330  isvclem  28346  isnvlem  28379  ajfval  28578  acunirnmpt2  30397  acunirnmpt2f  30398  wrdfd  30605  lbsdiflsp0  31015  smatrcl  31054  locfinref  31098  1stmbfm  31511  2ndmbfm  31512  sibfof  31591  rrvf2  31699  signshf  31851  reprsuc  31879  pfxwlk  32363  revwlk  32364  cvmliftmolem1  32521  cvmliftlem7  32531  cvmliftlem10  32534  cvmlift2lem9  32551  filnetlem4  33722  poimirlem16  34900  poimirlem19  34903  poimirlem23  34907  poimirlem24  34908  poimirlem25  34909  poimirlem29  34913  poimirlem31  34915  sdclem2  35009  sdclem1  35010  sdc  35011  fdc  35012  sstotbnd2  35044  elghomlem1OLD  35155  rngosn3  35194  frlmfzowrdb  39133  amgm4d  40543  mnurnd  40609  mptelpm  41421  fsneqrn  41463  cncfuni  42158  cncfiooicclem1  42165  dvsubf  42187  dvdivf  42196  dvbdfbdioolem1  42202  ioodvbdlimc1lem1  42205  ioodvbdlimc1lem2  42206  ioodvbdlimc1  42207  ioodvbdlimc2lem  42208  ioodvbdlimc2  42209  dvnprodlem3  42222  itgsubsticclem  42249  fourierdlem48  42429  fourierdlem49  42430  fourierdlem58  42439  fourierdlem59  42440  fourierdlem60  42441  fourierdlem61  42442  fourierdlem69  42450  fourierdlem75  42456  fourierdlem81  42462  fourierdlem89  42470  fourierdlem91  42472  fourierdlem97  42478  fourierdlem113  42494  meaf  42725  ismeannd  42739  psmeasure  42743  omef  42768  isomennd  42803  hoidmvlelem2  42868  hoidmvlelem3  42869  ovnhoi  42875  hspmbllem2  42899  sssmf  43005  smfpimioompt  43051  smffmpt  43069  2ffzoeq  43518  fundcmpsurbijinjpreimafv  43557  fargshiftf  43590  resmgmhm  44055  elbigolo1  44607