Theorem feq2d 6722

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536  ⟶wf 6558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-fn 6565  df-f 6566

This theorem is referenced by:  feq12d  6724  fco  6760  ffdm  6765  fsng  7156  fsn2g  7157  fsnunf2  7205  issmo2  8387  qliftf  8843  elpm2r  8883  ralxpmap  8934  axdc3lem3  10489  axdc3lem4  10490  fseq1p1m1  13634  fseq1m1p1  13635  seqf1o  14080  iswrdi  14552  wrdf  14553  wrdffz  14569  ffz0iswrd  14575  wrdnval  14579  ccatalpha  14627  swrdf  14684  swrdwrdsymb  14696  cats1un  14755  cshwf  14834  wrdlen2i  14977  wwlktovf  14991  rlimi  15545  rlimmptrcl  15640  lo1mptrcl  15654  o1mptrcl  15655  o1fsum  15845  ram0  17055  funcres  17946  curf2cl  18287  uncfcurf  18295  yonedalem4c  18333  intopsn  18679  gsumprval  18713  resmgmhm  18736  resmhm  18845  gsumwsubmcl  18862  gsumsgrpccat  18865  gsumwmhm  18870  frmdup1  18889  frmdup3lem  18891  isghmOLD  19246  resghm  19262  subgga  19330  gasubg  19332  psgnunilem2  19527  sylow2blem2  19653  pj2f  19730  pj1ghm  19735  frgpupf  19805  frgpup3lem  19809  gsumval3  19939  gsummptfzcl  20001  dprdf2  20041  ablfac2  20123  isabvd  20829  abvpropd  20852  cygznlem2a  21603  frgpcyg  21609  psrasclcl  22017  mplasclf  22106  evlssca  22130  lply1binomsc  22330  mat1dimelbas  22492  mat2pmatbas  22747  cpmadugsumlemF  22897  cnpf2  23273  ptpjcn  23634  cnextfres1  24091  cnextfres  24092  cnmpopc  24968  pi1addf  25093  pi1xfrf  25099  pi1cof  25105  mbfmptcl  25684  iblcnlem  25838  limcres  25935  cnplimc  25936  limccnp  25940  limccnp2  25941  limcun  25944  dvidlem  25964  cpnord  25985  dvaddf  25993  dvmulf  25994  dvcmulf  25996  dvcof  26000  dvcj  26002  dvrec  26007  dvmptcl  26011  dvcnvlem  26028  dvcnv  26029  rolle  26042  cmvth  26043  cmvthOLD  26044  mvth  26045  dvlip  26046  dvlipcn  26047  c1lip2  26051  dv11cn  26054  dvivthlem1  26061  dvivthlem2  26062  dvivth  26063  dvne0  26064  lhop1lem  26066  lhop1  26067  lhop2  26068  lhop  26069  dvcnvrelem2  26071  taylthlem1  26429  taylthlem2  26430  taylthlem2OLD  26431  ulmf2  26441  ulm2  26442  ulmdv  26460  pserdv  26487  rlimcxp  27031  o1cxp  27032  dchrptlem2  27323  axlowdimlem5  28975  axlowdimlem7  28977  axlowdimlem10  28980  uhgrn0  29098  wrdupgr  29116  upgrfn  29118  wrdumgr  29128  umgrfn  29130  upgr2wlk  29700  wlkres  29702  redwlklem  29703  wlkdlem1  29714  uhgrwkspthlem2  29786  usgr2wlkneq  29788  usgr2pthlem  29795  usgr2pth  29796  crctcshwlkn0  29850  wlkiswwlks2lem3  29900  wlkiswwlks2  29904  wlkiswwlksupgr2  29906  wlknewwlksn  29916  wpthswwlks2on  29990  clwlkclwwlklem2a  30026  clwlkclwwlklem1  30027  1wlkdlem1  30165  upgr3v3e3cycl  30208  upgr4cycl4dv4e  30213  isgrpo  30525  vciOLD  30589  isvclem  30605  isnvlem  30638  ajfval  30837  feq2dd  32639  acunirnmpt2  32676  acunirnmpt2f  32677  wrdfd  32902  elrspunidl  33435  lbsdiflsp0  33653  smatrcl  33756  locfinref  33801  1stmbfm  34241  2ndmbfm  34242  sibfof  34321  rrvf2  34429  signshf  34581  reprsuc  34608  pfxwlk  35107  revwlk  35108  cvmliftmolem1  35265  cvmliftlem7  35275  cvmliftlem10  35278  cvmlift2lem9  35295  filnetlem4  36363  poimirlem16  37622  poimirlem19  37625  poimirlem23  37629  poimirlem24  37630  poimirlem25  37631  poimirlem29  37635  poimirlem31  37637  sdclem2  37728  sdclem1  37729  sdc  37730  fdc  37731  sstotbnd2  37760  elghomlem1OLD  37871  rngosn3  37910  sticksstones9  42135  sticksstones11  42137  sticksstones16  42143  frlmfzowrdb  42490  evlselvlem  42572  evlselv  42573  ofoafg  43343  amgm4d  44189  mnurnd  44278  mptelpm  45118  fsneqrn  45153  cncfuni  45841  cncfiooicclem1  45848  dvsubf  45869  dvdivf  45877  dvbdfbdioolem1  45883  ioodvbdlimc1lem1  45886  ioodvbdlimc1lem2  45887  ioodvbdlimc1  45888  ioodvbdlimc2lem  45889  ioodvbdlimc2  45890  dvnprodlem3  45903  itgsubsticclem  45930  fourierdlem48  46109  fourierdlem49  46110  fourierdlem58  46119  fourierdlem59  46120  fourierdlem60  46121  fourierdlem61  46122  fourierdlem69  46130  fourierdlem75  46136  fourierdlem81  46142  fourierdlem89  46150  fourierdlem91  46152  fourierdlem97  46158  fourierdlem113  46174  meaf  46408  ismeannd  46422  psmeasure  46426  omef  46451  isomennd  46486  hoidmvlelem2  46551  hoidmvlelem3  46552  ovnhoi  46558  hspmbllem2  46582  sssmf  46693  smfpimioompt  46741  smffmptf  46759  2ffzoeq  47276  fundcmpsurbijinjpreimafv  47331  fargshiftf  47364  elbigolo1  48406  naryfvalelwrdf  48482  0aryfvalel  48483