Theorem feq2d 6640

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

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

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 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-fn 6489  df-f 6490

This theorem is referenced by:  feq2dd  6642  feq12d  6644  fco  6680  ffdm  6685  fsng  7075  fsn2g  7076  fsnunf2  7126  issmo2  8279  qliftf  8739  elpm2r  8779  ralxpmap  8830  axdc3lem3  10365  axdc3lem4  10366  fseq1p1m1  13519  fseq1m1p1  13520  seqf1o  13968  iswrdi  14442  wrdf  14443  wrdfd  14444  wrdffz  14460  ffz0iswrd  14466  wrdnval  14470  ccatalpha  14518  swrdf  14575  swrdwrdsymb  14587  cats1un  14645  cshwf  14724  wrdlen2i  14867  wwlktovf  14881  rlimi  15438  rlimmptrcl  15533  lo1mptrcl  15547  o1mptrcl  15548  o1fsum  15738  ram0  16952  funcres  17821  curf2cl  18155  uncfcurf  18163  yonedalem4c  18201  intopsn  18546  gsumprval  18580  resmgmhm  18603  resmhm  18712  gsumwsubmcl  18729  gsumsgrpccat  18732  gsumwmhm  18737  frmdup1  18756  frmdup3lem  18758  isghmOLD  19113  resghm  19129  subgga  19197  gasubg  19199  psgnunilem2  19392  sylow2blem2  19518  pj2f  19595  pj1ghm  19600  frgpupf  19670  frgpup3lem  19674  gsumval3  19804  gsummptfzcl  19866  dprdf2  19906  ablfac2  19988  isabvd  20715  abvpropd  20738  cygznlem2a  21492  frgpcyg  21498  psrasclcl  21905  mplasclf  21988  evlssca  22012  lply1binomsc  22214  mat1dimelbas  22374  mat2pmatbas  22629  cpmadugsumlemF  22779  cnpf2  23153  ptpjcn  23514  cnextfres1  23971  cnextfres  23972  cnmpopc  24838  pi1addf  24963  pi1xfrf  24969  pi1cof  24975  mbfmptcl  25553  iblcnlem  25706  limcres  25803  cnplimc  25804  limccnp  25808  limccnp2  25809  limcun  25812  dvidlem  25832  cpnord  25853  dvaddf  25861  dvmulf  25862  dvcmulf  25864  dvcof  25868  dvcj  25870  dvrec  25875  dvmptcl  25879  dvcnvlem  25896  dvcnv  25897  rolle  25910  cmvth  25911  cmvthOLD  25912  mvth  25913  dvlip  25914  dvlipcn  25915  c1lip2  25919  dv11cn  25922  dvivthlem1  25929  dvivthlem2  25930  dvivth  25931  dvne0  25932  lhop1lem  25934  lhop1  25935  lhop2  25936  lhop  25937  dvcnvrelem2  25939  taylthlem1  26297  taylthlem2  26298  taylthlem2OLD  26299  ulmf2  26309  ulm2  26310  ulmdv  26328  pserdv  26355  rlimcxp  26900  o1cxp  26901  dchrptlem2  27192  axlowdimlem5  28909  axlowdimlem7  28911  axlowdimlem10  28914  uhgrn0  29030  wrdupgr  29048  upgrfn  29050  wrdumgr  29060  umgrfn  29062  upgr2wlk  29630  wlkres  29632  redwlklem  29633  wlkdlem1  29644  uhgrwkspthlem2  29717  usgr2wlkneq  29719  usgr2pthlem  29726  usgr2pth  29727  crctcshwlkn0  29784  wlkiswwlks2lem3  29834  wlkiswwlks2  29838  wlkiswwlksupgr2  29840  wlknewwlksn  29850  wpthswwlks2on  29924  clwlkclwwlklem2a  29960  clwlkclwwlklem1  29961  1wlkdlem1  30099  upgr3v3e3cycl  30142  upgr4cycl4dv4e  30147  isgrpo  30459  vciOLD  30523  isvclem  30539  isnvlem  30572  ajfval  30771  acunirnmpt2  32617  acunirnmpt2f  32618  elrspunidl  33375  lbsdiflsp0  33598  smatrcl  33762  locfinref  33807  1stmbfm  34227  2ndmbfm  34228  sibfof  34307  rrvf2  34415  signshf  34555  reprsuc  34582  pfxwlk  35096  revwlk  35097  cvmliftmolem1  35253  cvmliftlem7  35263  cvmliftlem10  35266  cvmlift2lem9  35283  filnetlem4  36354  poimirlem16  37615  poimirlem19  37618  poimirlem23  37622  poimirlem24  37623  poimirlem25  37624  poimirlem29  37628  poimirlem31  37630  sdclem2  37721  sdclem1  37722  sdc  37723  fdc  37724  sstotbnd2  37753  elghomlem1OLD  37864  rngosn3  37903  sticksstones9  42127  sticksstones11  42129  sticksstones16  42135  frlmfzowrdb  42477  evlselvlem  42559  evlselv  42560  ofoafg  43327  amgm4d  44173  mnurnd  44256  mptelpm  45154  fsneqrn  45189  cncfuni  45868  cncfiooicclem1  45875  dvsubf  45896  dvdivf  45904  dvbdfbdioolem1  45910  ioodvbdlimc1lem1  45913  ioodvbdlimc1lem2  45914  ioodvbdlimc1  45915  ioodvbdlimc2lem  45916  ioodvbdlimc2  45917  dvnprodlem3  45930  itgsubsticclem  45957  fourierdlem48  46136  fourierdlem49  46137  fourierdlem58  46146  fourierdlem59  46147  fourierdlem60  46148  fourierdlem61  46149  fourierdlem69  46157  fourierdlem75  46163  fourierdlem81  46169  fourierdlem89  46177  fourierdlem91  46179  fourierdlem97  46185  fourierdlem113  46201  meaf  46435  ismeannd  46449  psmeasure  46453  omef  46478  isomennd  46513  hoidmvlelem2  46578  hoidmvlelem3  46579  ovnhoi  46585  hspmbllem2  46609  sssmf  46720  smfpimioompt  46768  smffmptf  46786  2ffzoeq  47312  fundcmpsurbijinjpreimafv  47392  fargshiftf  47425  upgrimwlklem2  47883  upgrimwlklem4  47885  upgrimpths  47894  gpgprismgr4cycllem9  48088  elbigolo1  48543  naryfvalelwrdf  48619  0aryfvalel  48620  0funcg2  49070  termcfuncval  49518