Theorem feq2d 6640

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ⟶wf 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-fn 6489  df-f 6490

This theorem is referenced by:  feq2dd  6642  feq12d  6644  fco  6680  ffdm  6685  fsng  7076  fsn2g  7077  fsnunf2  7126  issmo2  8275  qliftf  8735  elpm2r  8775  ralxpmap  8826  axdc3lem3  10350  axdc3lem4  10351  fseq1p1m1  13500  fseq1m1p1  13501  seqf1o  13952  iswrdi  14426  wrdf  14427  wrdfd  14428  wrdffz  14444  ffz0iswrd  14450  wrdnval  14454  ccatalpha  14503  swrdf  14560  swrdwrdsymb  14572  cats1un  14630  cshwf  14709  wrdlen2i  14851  wwlktovf  14865  rlimi  15422  rlimmptrcl  15517  lo1mptrcl  15531  o1mptrcl  15532  o1fsum  15722  ram0  16936  funcres  17805  curf2cl  18139  uncfcurf  18147  yonedalem4c  18185  intopsn  18564  gsumprval  18598  resmgmhm  18621  resmhm  18730  gsumwsubmcl  18747  gsumsgrpccat  18750  gsumwmhm  18755  frmdup1  18774  frmdup3lem  18776  isghmOLD  19130  resghm  19146  subgga  19214  gasubg  19216  psgnunilem2  19409  sylow2blem2  19535  pj2f  19612  pj1ghm  19617  frgpupf  19687  frgpup3lem  19691  gsumval3  19821  gsummptfzcl  19883  dprdf2  19923  ablfac2  20005  isabvd  20729  abvpropd  20752  cygznlem2a  21506  frgpcyg  21512  psrasclcl  21918  mplasclf  22001  evlssca  22025  lply1binomsc  22227  mat1dimelbas  22387  mat2pmatbas  22642  cpmadugsumlemF  22792  cnpf2  23166  ptpjcn  23527  cnextfres1  23984  cnextfres  23985  cnmpopc  24850  pi1addf  24975  pi1xfrf  24981  pi1cof  24987  mbfmptcl  25565  iblcnlem  25718  limcres  25815  cnplimc  25816  limccnp  25820  limccnp2  25821  limcun  25824  dvidlem  25844  cpnord  25865  dvaddf  25873  dvmulf  25874  dvcmulf  25876  dvcof  25880  dvcj  25882  dvrec  25887  dvmptcl  25891  dvcnvlem  25908  dvcnv  25909  rolle  25922  cmvth  25923  cmvthOLD  25924  mvth  25925  dvlip  25926  dvlipcn  25927  c1lip2  25931  dv11cn  25934  dvivthlem1  25941  dvivthlem2  25942  dvivth  25943  dvne0  25944  lhop1lem  25946  lhop1  25947  lhop2  25948  lhop  25949  dvcnvrelem2  25951  taylthlem1  26309  taylthlem2  26310  taylthlem2OLD  26311  ulmf2  26321  ulm2  26322  ulmdv  26340  pserdv  26367  rlimcxp  26912  o1cxp  26913  dchrptlem2  27204  axlowdimlem5  28926  axlowdimlem7  28928  axlowdimlem10  28931  uhgrn0  29047  wrdupgr  29065  upgrfn  29067  wrdumgr  29077  umgrfn  29079  upgr2wlk  29647  wlkres  29649  redwlklem  29650  wlkdlem1  29661  uhgrwkspthlem2  29734  usgr2wlkneq  29736  usgr2pthlem  29743  usgr2pth  29744  crctcshwlkn0  29801  wlkiswwlks2lem3  29851  wlkiswwlks2  29855  wlkiswwlksupgr2  29857  wlknewwlksn  29867  wpthswwlks2on  29944  clwlkclwwlklem2a  29980  clwlkclwwlklem1  29981  1wlkdlem1  30119  upgr3v3e3cycl  30162  upgr4cycl4dv4e  30167  isgrpo  30479  vciOLD  30543  isvclem  30559  isnvlem  30592  ajfval  30791  acunirnmpt2  32644  acunirnmpt2f  32645  elrspunidl  33400  lbsdiflsp0  33660  smatrcl  33830  locfinref  33875  1stmbfm  34294  2ndmbfm  34295  sibfof  34374  rrvf2  34482  signshf  34622  reprsuc  34649  pfxwlk  35189  revwlk  35190  cvmliftmolem1  35346  cvmliftlem7  35356  cvmliftlem10  35359  cvmlift2lem9  35376  filnetlem4  36446  poimirlem16  37696  poimirlem19  37699  poimirlem23  37703  poimirlem24  37704  poimirlem25  37705  poimirlem29  37709  poimirlem31  37711  sdclem2  37802  sdclem1  37803  sdc  37804  fdc  37805  sstotbnd2  37834  elghomlem1OLD  37945  rngosn3  37984  sticksstones9  42267  sticksstones11  42269  sticksstones16  42275  frlmfzowrdb  42622  evlselvlem  42704  evlselv  42705  ofoafg  43471  amgm4d  44317  mnurnd  44400  mptelpm  45297  fsneqrn  45332  cncfuni  46008  cncfiooicclem1  46015  dvsubf  46036  dvdivf  46044  dvbdfbdioolem1  46050  ioodvbdlimc1lem1  46053  ioodvbdlimc1lem2  46054  ioodvbdlimc1  46055  ioodvbdlimc2lem  46056  ioodvbdlimc2  46057  dvnprodlem3  46070  itgsubsticclem  46097  fourierdlem48  46276  fourierdlem49  46277  fourierdlem58  46286  fourierdlem59  46287  fourierdlem60  46288  fourierdlem61  46289  fourierdlem69  46297  fourierdlem75  46303  fourierdlem81  46309  fourierdlem89  46317  fourierdlem91  46319  fourierdlem97  46325  fourierdlem113  46341  meaf  46575  ismeannd  46589  psmeasure  46593  omef  46618  isomennd  46653  hoidmvlelem2  46718  hoidmvlelem3  46719  ovnhoi  46725  hspmbllem2  46749  sssmf  46860  smfpimioompt  46908  smffmptf  46926  chnsubseqword  47000  2ffzoeq  47451  fundcmpsurbijinjpreimafv  47531  fargshiftf  47564  upgrimwlklem2  48022  upgrimwlklem4  48024  upgrimpths  48033  gpgprismgr4cycllem9  48227  elbigolo1  48682  naryfvalelwrdf  48758  0aryfvalel  48759  0funcg2  49209  termcfuncval  49657