Theorem feq2d 6652

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ⟶wf 6494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-fn 6501  df-f 6502

This theorem is referenced by:  feq2dd  6654  feq12d  6656  fco  6692  ffdm  6697  fsng  7090  fsn2g  7091  fsnunf2  7141  issmo2  8289  qliftf  8752  elpm2r  8792  ralxpmap  8844  axdc3lem3  10374  axdc3lem4  10375  fseq1p1m1  13552  fseq1m1p1  13553  seqf1o  14005  iswrdi  14479  wrdf  14480  wrdfd  14481  wrdffz  14497  ffz0iswrd  14503  wrdnval  14507  ccatalpha  14556  swrdf  14613  swrdwrdsymb  14625  cats1un  14683  cshwf  14762  wrdlen2i  14904  wwlktovf  14918  rlimi  15475  rlimmptrcl  15570  lo1mptrcl  15584  o1mptrcl  15585  o1fsum  15776  ram0  16993  funcres  17863  curf2cl  18197  uncfcurf  18205  yonedalem4c  18243  intopsn  18622  gsumprval  18656  resmgmhm  18679  resmhm  18788  gsumwsubmcl  18805  gsumsgrpccat  18808  gsumwmhm  18813  frmdup1  18832  frmdup3lem  18834  isghmOLD  19191  resghm  19207  subgga  19275  gasubg  19277  psgnunilem2  19470  sylow2blem2  19596  pj2f  19673  pj1ghm  19678  frgpupf  19748  frgpup3lem  19752  gsumval3  19882  gsummptfzcl  19944  dprdf2  19984  ablfac2  20066  isabvd  20789  abvpropd  20812  cygznlem2a  21547  frgpcyg  21553  psrasclcl  21958  mplasclf  22043  evlssca  22072  lply1binomsc  22276  mat1dimelbas  22436  mat2pmatbas  22691  cpmadugsumlemF  22841  cnpf2  23215  ptpjcn  23576  cnextfres1  24033  cnextfres  24034  cnmpopc  24895  pi1addf  25014  pi1xfrf  25020  pi1cof  25026  mbfmptcl  25603  iblcnlem  25756  limcres  25853  cnplimc  25854  limccnp  25858  limccnp2  25859  limcun  25862  dvidlem  25882  cpnord  25902  dvaddf  25909  dvmulf  25910  dvcmulf  25912  dvcof  25915  dvcj  25917  dvrec  25922  dvmptcl  25926  dvcnvlem  25943  dvcnv  25944  rolle  25957  cmvth  25958  mvth  25959  dvlip  25960  dvlipcn  25961  c1lip2  25965  dv11cn  25968  dvivthlem1  25975  dvivthlem2  25976  dvivth  25977  dvne0  25978  lhop1lem  25980  lhop1  25981  lhop2  25982  lhop  25983  dvcnvrelem2  25985  taylthlem1  26338  taylthlem2  26339  ulmf2  26349  ulm2  26350  ulmdv  26368  pserdv  26394  rlimcxp  26937  o1cxp  26938  dchrptlem2  27228  axlowdimlem5  29015  axlowdimlem7  29017  axlowdimlem10  29020  uhgrn0  29136  wrdupgr  29154  upgrfn  29156  wrdumgr  29166  umgrfn  29168  upgr2wlk  29735  wlkres  29737  redwlklem  29738  wlkdlem1  29749  uhgrwkspthlem2  29822  usgr2wlkneq  29824  usgr2pthlem  29831  usgr2pth  29832  crctcshwlkn0  29889  wlkiswwlks2lem3  29939  wlkiswwlks2  29943  wlkiswwlksupgr2  29945  wlknewwlksn  29955  wpthswwlks2on  30032  clwlkclwwlklem2a  30068  clwlkclwwlklem1  30069  1wlkdlem1  30207  upgr3v3e3cycl  30250  upgr4cycl4dv4e  30255  isgrpo  30568  vciOLD  30632  isvclem  30648  isnvlem  30681  ajfval  30880  acunirnmpt2  32733  acunirnmpt2f  32734  elrspunidl  33488  lbsdiflsp0  33770  smatrcl  33940  locfinref  33985  1stmbfm  34404  2ndmbfm  34405  sibfof  34484  rrvf2  34592  signshf  34732  reprsuc  34759  pfxwlk  35306  revwlk  35307  cvmliftmolem1  35463  cvmliftlem7  35473  cvmliftlem10  35476  cvmlift2lem9  35493  filnetlem4  36563  poimirlem16  37957  poimirlem19  37960  poimirlem23  37964  poimirlem24  37965  poimirlem25  37966  poimirlem29  37970  poimirlem31  37972  sdclem2  38063  sdclem1  38064  sdc  38065  fdc  38066  sstotbnd2  38095  elghomlem1OLD  38206  rngosn3  38245  sticksstones9  42593  sticksstones11  42595  sticksstones16  42601  frlmfzowrdb  42949  evlselvlem  43019  evlselv  43020  ofoafg  43782  amgm4d  44627  mnurnd  44710  mptelpm  45606  fsneqrn  45640  cncfuni  46314  cncfiooicclem1  46321  dvsubf  46342  dvdivf  46350  dvbdfbdioolem1  46356  ioodvbdlimc1lem1  46359  ioodvbdlimc1lem2  46360  ioodvbdlimc1  46361  ioodvbdlimc2lem  46362  ioodvbdlimc2  46363  dvnprodlem3  46376  itgsubsticclem  46403  fourierdlem48  46582  fourierdlem49  46583  fourierdlem58  46592  fourierdlem59  46593  fourierdlem60  46594  fourierdlem61  46595  fourierdlem69  46603  fourierdlem75  46609  fourierdlem81  46615  fourierdlem89  46623  fourierdlem91  46625  fourierdlem97  46631  fourierdlem113  46647  meaf  46881  ismeannd  46895  psmeasure  46899  omef  46924  isomennd  46959  hoidmvlelem2  47024  hoidmvlelem3  47025  ovnhoi  47031  hspmbllem2  47055  sssmf  47166  smfpimioompt  47214  smffmptf  47232  chnsubseqword  47308  2ffzoeq  47776  fundcmpsurbijinjpreimafv  47867  fargshiftf  47900  upgrimwlklem2  48374  upgrimwlklem4  48376  upgrimpths  48385  gpgprismgr4cycllem9  48579  elbigolo1  49033  naryfvalelwrdf  49109  0aryfvalel  49110  0funcg2  49559  termcfuncval  50007