Theorem feq2d 6693

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569  ⟶wf 6534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-fn 6541  df-f 6542

This theorem is used by:  feq2dd  6695  feq12d  6697  fco  6734  ffdm  6739  fsng  7138  fsn2g  7139  fsnunf2  7191  issmo2  8360  qliftf  8829  elpm2r  8868  ralxpmap  8927  axdc3lem3  10533  axdc3lem4  10534  fseq1p1m1  13735  fseq1m1p1  13736  seqf1o  14189  iswrdi  14665  wrdf  14666  wrdfd  14667  wrdffz  14683  ffz0iswrd  14689  wrdnval  14693  ccatalpha  14743  swrdf  14802  swrdwrdsymb  14816  cats1un  14874  cshwf  14955  wrdlen2i  15098  wwlktovf  15114  rlimi  15685  rlimmptrcl  15780  lo1mptrcl  15794  o1mptrcl  15795  o1fsum  15985  ram0  17205  funcres  18076  curf2cl  18410  uncfcurf  18418  yonedalem4c  18456  intopsn  18837  gsumprval  18882  resmgmhm  18905  resmhm  19021  gsumwsubmcl  19038  gsumsgrpccat  19041  gsumwmhm  19046  frmdup1  19065  frmdup3lem  19067  resghm  19451  subgga  19519  gasubg  19521  psgnunilem2  19714  sylow2blem2  19840  pj2f  19917  pj1ghm  19922  frgpupf  19992  frgpup3lem  19996  gsumval3  20126  gsummptfzcl  20188  dprdf2  20228  ablfac2  20310  isabvd  21074  abvpropd  21097  cygznlem2a  21878  frgpcyg  21884  psrasclcl  22292  mplasclf  22379  evlssca  22408  lply1binomsc  22634  mat1dimelbas  22791  mat2pmatbas  23049  cpmadugsumlemF  23199  cnpf2  23573  ptpjcn  23935  cnextfres1  24392  cnextfres  24393  cnmpopc  25254  pi1addf  25373  pi1xfrf  25379  pi1cof  25385  mbfmptcl  25962  iblcnlem  26114  limcres  26211  cnplimc  26212  limccnp  26216  limccnp2  26217  limcun  26220  dvidlem  26240  cpnord  26260  dvaddf  26267  dvmulf  26268  dvcmulf  26270  dvcof  26273  dvcj  26275  dvrec  26280  dvmptcl  26284  dvcnvlem  26301  dvcnv  26302  rolle  26315  cmvth  26316  mvth  26317  dvlip  26318  dvlipcn  26319  c1lip2  26323  dv11cn  26326  dvivthlem1  26333  dvivthlem2  26334  dvivth  26335  dvne0  26336  lhop1lem  26338  lhop1  26339  lhop2  26340  lhop  26341  dvcnvrelem2  26343  taylthlem1  26705  taylthlem2  26706  ulmf2  26716  ulm2  26717  ulmdv  26735  pserdv  26761  rlimcxp  27306  o1cxp  27307  dchrptlem2  27597  axlowdimlem5  29529  axlowdimlem7  29531  axlowdimlem10  29534  uhgrn0  29650  wrdupgr  29668  upgrfn  29670  wrdumgr  29680  umgrfn  29682  upgr2wlk  30252  wlkres  30254  redwlklem  30255  wlkdlem1  30266  pfxwlk  30271  revwlk  30272  uhgrwkspthlem2  30345  usgr2wlkneq  30347  usgr2pthlem  30354  usgr2pth  30355  crctcshwlkn0  30415  wlkiswwlks2lem3  30465  wlkiswwlks2  30469  wlkiswwlksupgr2  30471  wlknewwlksn  30481  wpthswwlks2on  30558  clwlkclwwlklem2a  30594  clwlkclwwlklem1  30595  1wlkdlem1  30733  upgr3v3e3cycl  30786  upgr4cycl4dv4e  30791  isgrpo  31104  vciOLD  31168  isvclem  31184  isnvlem  31217  ajfval  31416  lbsdiflsp0  34304  smatrcl  34474  locfinref  34519  1stmbfm  34938  2ndmbfm  34939  sibfof  35018  rrvf2  35126  signshf  35263  reprsuc  35290  cvmliftmolem1  36132  cvmliftlem7  36142  cvmliftlem10  36145  cvmlift2lem9  36162  filnetlem4  37261  poimirlem16  38647  poimirlem19  38650  poimirlem23  38654  poimirlem24  38655  poimirlem25  38656  poimirlem29  38660  poimirlem31  38662  sdclem2  38769  sdclem1  38770  sdc  38771  fdc  38772  sstotbnd2  38801  elghomlem1OLD  38912  rngosn3  38951  sticksstones9  43297  sticksstones11  43299  sticksstones16  43305  frlmfzowrdb  43664  evlselv  43710  ofoafg  44449  amgm4d  45293  mnurnd  45360  mptelpm  46284  fsneqrn  46317  cncfiooicclem1  46996  dvsubf  47017  dvdivf  47025  dvbdfbdioolem1  47031  ioodvbdlimc1lem1  47034  ioodvbdlimc1lem2  47035  ioodvbdlimc1  47036  ioodvbdlimc2lem  47037  ioodvbdlimc2  47038  dvnprodlem3  47051  itgsubsticclem  47078  fourierdlem58  47267  fourierdlem59  47268  fourierdlem60  47269  fourierdlem61  47270  fourierdlem69  47278  fourierdlem75  47284  fourierdlem81  47290  fourierdlem89  47298  fourierdlem91  47300  fourierdlem97  47306  meaf  47556  ismeannd  47570  psmeasure  47574  omef  47599  isomennd  47634  hoidmvlelem2  47699  hoidmvlelem3  47700  ovnhoi  47706  hspmbllem2  47730  smfpimioompt  47889  smffmptf  47907  chnsubseqword  47981  2ffzoeq  48491  fundcmpsurbijinjpreimafv  48582  fargshiftf  48615  upgrimwlklem2  49089  upgrimwlklem4  49091  upgrimpths  49100  gpgprismgr4cycllem9  49294  elbigolo1  49762  naryfvalelwrdf  49838  0aryfvalel  49839  0funcg2  50292  termcfuncval  50760