Theorem feq2d 6733

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  ⟶wf 6569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-fn 6576  df-f 6577

This theorem is referenced by:  feq12d  6735  fco  6771  ffdm  6777  fsng  7171  fsn2g  7172  fsnunf2  7220  issmo2  8405  qliftf  8863  elpm2r  8903  ralxpmap  8954  axdc3lem3  10521  axdc3lem4  10522  fseq1p1m1  13658  fseq1m1p1  13659  seqf1o  14094  iswrdi  14566  wrdf  14567  wrdffz  14583  ffz0iswrd  14589  wrdnval  14593  ccatalpha  14641  swrdf  14698  swrdwrdsymb  14710  cats1un  14769  cshwf  14848  wrdlen2i  14991  wwlktovf  15005  rlimi  15559  rlimmptrcl  15654  lo1mptrcl  15668  o1mptrcl  15669  o1fsum  15861  ram0  17069  funcres  17960  curf2cl  18301  uncfcurf  18309  yonedalem4c  18347  intopsn  18692  gsumprval  18726  resmgmhm  18749  resmhm  18855  gsumwsubmcl  18872  gsumsgrpccat  18875  gsumwmhm  18880  frmdup1  18899  frmdup3lem  18901  isghmOLD  19256  resghm  19272  subgga  19340  gasubg  19342  psgnunilem2  19537  sylow2blem2  19663  pj2f  19740  pj1ghm  19745  frgpupf  19815  frgpup3lem  19819  gsumval3  19949  gsummptfzcl  20011  dprdf2  20051  ablfac2  20133  isabvd  20835  abvpropd  20858  cygznlem2a  21609  frgpcyg  21615  psrasclcl  22023  mplasclf  22112  evlssca  22136  lply1binomsc  22336  mat1dimelbas  22498  mat2pmatbas  22753  cpmadugsumlemF  22903  cnpf2  23279  ptpjcn  23640  cnextfres1  24097  cnextfres  24098  cnmpopc  24974  pi1addf  25099  pi1xfrf  25105  pi1cof  25111  mbfmptcl  25690  iblcnlem  25844  limcres  25941  cnplimc  25942  limccnp  25946  limccnp2  25947  limcun  25950  dvidlem  25970  cpnord  25991  dvaddf  25999  dvmulf  26000  dvcmulf  26002  dvcof  26006  dvcj  26008  dvrec  26013  dvmptcl  26017  dvcnvlem  26034  dvcnv  26035  rolle  26048  cmvth  26049  cmvthOLD  26050  mvth  26051  dvlip  26052  dvlipcn  26053  c1lip2  26057  dv11cn  26060  dvivthlem1  26067  dvivthlem2  26068  dvivth  26069  dvne0  26070  lhop1lem  26072  lhop1  26073  lhop2  26074  lhop  26075  dvcnvrelem2  26077  taylthlem1  26433  taylthlem2  26434  taylthlem2OLD  26435  ulmf2  26445  ulm2  26446  ulmdv  26464  pserdv  26491  rlimcxp  27035  o1cxp  27036  dchrptlem2  27327  axlowdimlem5  28979  axlowdimlem7  28981  axlowdimlem10  28984  uhgrn0  29102  wrdupgr  29120  upgrfn  29122  wrdumgr  29132  umgrfn  29134  upgr2wlk  29704  wlkres  29706  redwlklem  29707  wlkdlem1  29718  uhgrwkspthlem2  29790  usgr2wlkneq  29792  usgr2pthlem  29799  usgr2pth  29800  crctcshwlkn0  29854  wlkiswwlks2lem3  29904  wlkiswwlks2  29908  wlkiswwlksupgr2  29910  wlknewwlksn  29920  wpthswwlks2on  29994  clwlkclwwlklem2a  30030  clwlkclwwlklem1  30031  1wlkdlem1  30169  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  isgrpo  30529  vciOLD  30593  isvclem  30609  isnvlem  30642  ajfval  30841  feq2dd  32642  acunirnmpt2  32678  acunirnmpt2f  32679  wrdfd  32900  elrspunidl  33421  lbsdiflsp0  33639  smatrcl  33742  locfinref  33787  1stmbfm  34225  2ndmbfm  34226  sibfof  34305  rrvf2  34413  signshf  34565  reprsuc  34592  pfxwlk  35091  revwlk  35092  cvmliftmolem1  35249  cvmliftlem7  35259  cvmliftlem10  35262  cvmlift2lem9  35279  filnetlem4  36347  poimirlem16  37596  poimirlem19  37599  poimirlem23  37603  poimirlem24  37604  poimirlem25  37605  poimirlem29  37609  poimirlem31  37611  sdclem2  37702  sdclem1  37703  sdc  37704  fdc  37705  sstotbnd2  37734  elghomlem1OLD  37845  rngosn3  37884  sticksstones9  42111  sticksstones11  42113  sticksstones16  42119  frlmfzowrdb  42459  evlselvlem  42541  evlselv  42542  ofoafg  43316  amgm4d  44162  mnurnd  44252  mptelpm  45083  fsneqrn  45118  cncfuni  45807  cncfiooicclem1  45814  dvsubf  45835  dvdivf  45843  dvbdfbdioolem1  45849  ioodvbdlimc1lem1  45852  ioodvbdlimc1lem2  45853  ioodvbdlimc1  45854  ioodvbdlimc2lem  45855  ioodvbdlimc2  45856  dvnprodlem3  45869  itgsubsticclem  45896  fourierdlem48  46075  fourierdlem49  46076  fourierdlem58  46085  fourierdlem59  46086  fourierdlem60  46087  fourierdlem61  46088  fourierdlem69  46096  fourierdlem75  46102  fourierdlem81  46108  fourierdlem89  46116  fourierdlem91  46118  fourierdlem97  46124  fourierdlem113  46140  meaf  46374  ismeannd  46388  psmeasure  46392  omef  46417  isomennd  46452  hoidmvlelem2  46517  hoidmvlelem3  46518  ovnhoi  46524  hspmbllem2  46548  sssmf  46659  smfpimioompt  46707  smffmptf  46725  2ffzoeq  47242  fundcmpsurbijinjpreimafv  47281  fargshiftf  47314  elbigolo1  48291  naryfvalelwrdf  48367  0aryfvalel  48368