Theorem feq2d 6654

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-fn 6503  df-f 6504

This theorem is referenced by:  feq2dd  6656  feq12d  6658  fco  6694  ffdm  6699  fsng  7092  fsn2g  7093  fsnunf2  7142  issmo2  8291  qliftf  8754  elpm2r  8794  ralxpmap  8846  axdc3lem3  10374  axdc3lem4  10375  fseq1p1m1  13526  fseq1m1p1  13527  seqf1o  13978  iswrdi  14452  wrdf  14453  wrdfd  14454  wrdffz  14470  ffz0iswrd  14476  wrdnval  14480  ccatalpha  14529  swrdf  14586  swrdwrdsymb  14598  cats1un  14656  cshwf  14735  wrdlen2i  14877  wwlktovf  14891  rlimi  15448  rlimmptrcl  15543  lo1mptrcl  15557  o1mptrcl  15558  o1fsum  15748  ram0  16962  funcres  17832  curf2cl  18166  uncfcurf  18174  yonedalem4c  18212  intopsn  18591  gsumprval  18625  resmgmhm  18648  resmhm  18757  gsumwsubmcl  18774  gsumsgrpccat  18777  gsumwmhm  18782  frmdup1  18801  frmdup3lem  18803  isghmOLD  19157  resghm  19173  subgga  19241  gasubg  19243  psgnunilem2  19436  sylow2blem2  19562  pj2f  19639  pj1ghm  19644  frgpupf  19714  frgpup3lem  19718  gsumval3  19848  gsummptfzcl  19910  dprdf2  19950  ablfac2  20032  isabvd  20757  abvpropd  20780  cygznlem2a  21534  frgpcyg  21540  psrasclcl  21947  mplasclf  22032  evlssca  22061  lply1binomsc  22267  mat1dimelbas  22427  mat2pmatbas  22682  cpmadugsumlemF  22832  cnpf2  23206  ptpjcn  23567  cnextfres1  24024  cnextfres  24025  cnmpopc  24890  pi1addf  25015  pi1xfrf  25021  pi1cof  25027  mbfmptcl  25605  iblcnlem  25758  limcres  25855  cnplimc  25856  limccnp  25860  limccnp2  25861  limcun  25864  dvidlem  25884  cpnord  25905  dvaddf  25913  dvmulf  25914  dvcmulf  25916  dvcof  25920  dvcj  25922  dvrec  25927  dvmptcl  25931  dvcnvlem  25948  dvcnv  25949  rolle  25962  cmvth  25963  cmvthOLD  25964  mvth  25965  dvlip  25966  dvlipcn  25967  c1lip2  25971  dv11cn  25974  dvivthlem1  25981  dvivthlem2  25982  dvivth  25983  dvne0  25984  lhop1lem  25986  lhop1  25987  lhop2  25988  lhop  25989  dvcnvrelem2  25991  taylthlem1  26349  taylthlem2  26350  taylthlem2OLD  26351  ulmf2  26361  ulm2  26362  ulmdv  26380  pserdv  26407  rlimcxp  26952  o1cxp  26953  dchrptlem2  27244  axlowdimlem5  29031  axlowdimlem7  29033  axlowdimlem10  29036  uhgrn0  29152  wrdupgr  29170  upgrfn  29172  wrdumgr  29182  umgrfn  29184  upgr2wlk  29752  wlkres  29754  redwlklem  29755  wlkdlem1  29766  uhgrwkspthlem2  29839  usgr2wlkneq  29841  usgr2pthlem  29848  usgr2pth  29849  crctcshwlkn0  29906  wlkiswwlks2lem3  29956  wlkiswwlks2  29960  wlkiswwlksupgr2  29962  wlknewwlksn  29972  wpthswwlks2on  30049  clwlkclwwlklem2a  30085  clwlkclwwlklem1  30086  1wlkdlem1  30224  upgr3v3e3cycl  30267  upgr4cycl4dv4e  30272  isgrpo  30584  vciOLD  30648  isvclem  30664  isnvlem  30697  ajfval  30896  acunirnmpt2  32749  acunirnmpt2f  32750  elrspunidl  33520  lbsdiflsp0  33803  smatrcl  33973  locfinref  34018  1stmbfm  34437  2ndmbfm  34438  sibfof  34517  rrvf2  34625  signshf  34765  reprsuc  34792  pfxwlk  35337  revwlk  35338  cvmliftmolem1  35494  cvmliftlem7  35504  cvmliftlem10  35507  cvmlift2lem9  35524  filnetlem4  36594  poimirlem16  37881  poimirlem19  37884  poimirlem23  37888  poimirlem24  37889  poimirlem25  37890  poimirlem29  37894  poimirlem31  37896  sdclem2  37987  sdclem1  37988  sdc  37989  fdc  37990  sstotbnd2  38019  elghomlem1OLD  38130  rngosn3  38169  sticksstones9  42518  sticksstones11  42520  sticksstones16  42526  frlmfzowrdb  42868  evlselvlem  42938  evlselv  42939  ofoafg  43705  amgm4d  44550  mnurnd  44633  mptelpm  45529  fsneqrn  45563  cncfuni  46238  cncfiooicclem1  46245  dvsubf  46266  dvdivf  46274  dvbdfbdioolem1  46280  ioodvbdlimc1lem1  46283  ioodvbdlimc1lem2  46284  ioodvbdlimc1  46285  ioodvbdlimc2lem  46286  ioodvbdlimc2  46287  dvnprodlem3  46300  itgsubsticclem  46327  fourierdlem48  46506  fourierdlem49  46507  fourierdlem58  46516  fourierdlem59  46517  fourierdlem60  46518  fourierdlem61  46519  fourierdlem69  46527  fourierdlem75  46533  fourierdlem81  46539  fourierdlem89  46547  fourierdlem91  46549  fourierdlem97  46555  fourierdlem113  46571  meaf  46805  ismeannd  46819  psmeasure  46823  omef  46848  isomennd  46883  hoidmvlelem2  46948  hoidmvlelem3  46949  ovnhoi  46955  hspmbllem2  46979  sssmf  47090  smfpimioompt  47138  smffmptf  47156  chnsubseqword  47230  2ffzoeq  47681  fundcmpsurbijinjpreimafv  47761  fargshiftf  47794  upgrimwlklem2  48252  upgrimwlklem4  48254  upgrimpths  48263  gpgprismgr4cycllem9  48457  elbigolo1  48911  naryfvalelwrdf  48987  0aryfvalel  48988  0funcg2  49437  termcfuncval  49885