Theorem feq2d 6671

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559  ⟶wf 6513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-fn 6520  df-f 6521

This theorem is referenced by:  feq2dd  6673  feq12d  6675  fco  6712  ffdm  6717  fsng  7115  fsn2g  7116  fsnunf2  7166  issmo2  8315  qliftf  8782  elpm2r  8822  ralxpmap  8874  axdc3lem3  10406  axdc3lem4  10407  fseq1p1m1  13600  fseq1m1p1  13601  seqf1o  14053  iswrdi  14527  wrdf  14528  wrdfd  14529  wrdffz  14545  ffz0iswrd  14551  wrdnval  14555  ccatalpha  14604  swrdf  14661  swrdwrdsymb  14673  cats1un  14731  cshwf  14810  wrdlen2i  14952  wwlktovf  14966  rlimi  15523  rlimmptrcl  15618  lo1mptrcl  15632  o1mptrcl  15633  o1fsum  15824  ram0  17041  funcres  17912  curf2cl  18246  uncfcurf  18254  yonedalem4c  18292  intopsn  18671  gsumprval  18705  resmgmhm  18728  resmhm  18837  gsumwsubmcl  18854  gsumsgrpccat  18857  gsumwmhm  18862  frmdup1  18881  frmdup3lem  18883  resghm  19255  subgga  19323  gasubg  19325  psgnunilem2  19518  sylow2blem2  19644  pj2f  19721  pj1ghm  19726  frgpupf  19796  frgpup3lem  19800  gsumval3  19930  gsummptfzcl  19992  dprdf2  20032  ablfac2  20114  isabvd  20841  abvpropd  20864  cygznlem2a  21599  frgpcyg  21605  psrasclcl  22011  mplasclf  22098  evlssca  22127  lply1binomsc  22354  mat1dimelbas  22511  mat2pmatbas  22766  cpmadugsumlemF  22916  cnpf2  23290  ptpjcn  23651  cnextfres1  24108  cnextfres  24109  cnmpopc  24970  pi1addf  25089  pi1xfrf  25095  pi1cof  25101  mbfmptcl  25678  iblcnlem  25831  limcres  25928  cnplimc  25929  limccnp  25933  limccnp2  25934  limcun  25937  dvidlem  25957  cpnord  25977  dvaddf  25984  dvmulf  25985  dvcmulf  25987  dvcof  25990  dvcj  25992  dvrec  25997  dvmptcl  26001  dvcnvlem  26018  dvcnv  26019  rolle  26032  cmvth  26033  mvth  26034  dvlip  26035  dvlipcn  26036  c1lip2  26040  dv11cn  26043  dvivthlem1  26050  dvivthlem2  26051  dvivth  26052  dvne0  26053  lhop1lem  26055  lhop1  26056  lhop2  26057  lhop  26058  dvcnvrelem2  26060  taylthlem1  26413  taylthlem2  26414  ulmf2  26424  ulm2  26425  ulmdv  26443  pserdv  26469  rlimcxp  27015  o1cxp  27016  dchrptlem2  27306  axlowdimlem5  29093  axlowdimlem7  29095  axlowdimlem10  29098  uhgrn0  29214  wrdupgr  29232  upgrfn  29234  wrdumgr  29244  umgrfn  29246  upgr2wlk  29813  wlkres  29815  redwlklem  29816  wlkdlem1  29827  uhgrwkspthlem2  29900  usgr2wlkneq  29902  usgr2pthlem  29909  usgr2pth  29910  crctcshwlkn0  29967  wlkiswwlks2lem3  30017  wlkiswwlks2  30021  wlkiswwlksupgr2  30023  wlknewwlksn  30033  wpthswwlks2on  30110  clwlkclwwlklem2a  30146  clwlkclwwlklem1  30147  1wlkdlem1  30285  upgr3v3e3cycl  30328  upgr4cycl4dv4e  30333  isgrpo  30646  vciOLD  30710  isvclem  30726  isnvlem  30759  ajfval  30958  acunirnmpt2  32812  acunirnmpt2f  32813  elrspunidl  33575  lbsdiflsp0  33884  smatrcl  34054  locfinref  34099  1stmbfm  34518  2ndmbfm  34519  sibfof  34598  rrvf2  34706  signshf  34846  reprsuc  34873  pfxwlk  35438  revwlk  35439  cvmliftmolem1  35595  cvmliftlem7  35605  cvmliftlem10  35608  cvmlift2lem9  35625  filnetlem4  36705  poimirlem16  38099  poimirlem19  38102  poimirlem23  38106  poimirlem24  38107  poimirlem25  38108  poimirlem29  38112  poimirlem31  38114  sdclem2  38205  sdclem1  38206  sdc  38207  fdc  38208  sstotbnd2  38237  elghomlem1OLD  38348  rngosn3  38387  sticksstones9  42735  sticksstones11  42737  sticksstones16  42743  frlmfzowrdb  43090  evlselvlem  43134  evlselv  43135  ofoafg  43895  amgm4d  44740  mnurnd  44823  mptelpm  45718  fsneqrn  45751  cncfiooicclem1  46431  dvsubf  46452  dvdivf  46460  dvbdfbdioolem1  46466  ioodvbdlimc1lem1  46469  ioodvbdlimc1lem2  46470  ioodvbdlimc1  46471  ioodvbdlimc2lem  46472  ioodvbdlimc2  46473  dvnprodlem3  46486  itgsubsticclem  46513  fourierdlem58  46702  fourierdlem59  46703  fourierdlem60  46704  fourierdlem61  46705  fourierdlem69  46713  fourierdlem75  46719  fourierdlem81  46725  fourierdlem89  46733  fourierdlem91  46735  fourierdlem97  46741  meaf  46991  ismeannd  47005  psmeasure  47009  omef  47034  isomennd  47069  hoidmvlelem2  47134  hoidmvlelem3  47135  ovnhoi  47141  hspmbllem2  47165  smfpimioompt  47324  smffmptf  47342  chnsubseqword  47418  2ffzoeq  47886  fundcmpsurbijinjpreimafv  47977  fargshiftf  48010  upgrimwlklem2  48484  upgrimwlklem4  48486  upgrimpths  48495  gpgprismgr4cycllem9  48689  elbigolo1  49143  naryfvalelwrdf  49219  0aryfvalel  49220  0funcg2  49669  termcfuncval  50117