Theorem feq2d 6646

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

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

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 6495  df-f 6496

This theorem is referenced by:  feq2dd  6648  feq12d  6650  fco  6686  ffdm  6691  fsng  7084  fsn2g  7085  fsnunf2  7134  issmo2  8282  qliftf  8745  elpm2r  8785  ralxpmap  8837  axdc3lem3  10365  axdc3lem4  10366  fseq1p1m1  13543  fseq1m1p1  13544  seqf1o  13996  iswrdi  14470  wrdf  14471  wrdfd  14472  wrdffz  14488  ffz0iswrd  14494  wrdnval  14498  ccatalpha  14547  swrdf  14604  swrdwrdsymb  14616  cats1un  14674  cshwf  14753  wrdlen2i  14895  wwlktovf  14909  rlimi  15466  rlimmptrcl  15561  lo1mptrcl  15575  o1mptrcl  15576  o1fsum  15767  ram0  16984  funcres  17854  curf2cl  18188  uncfcurf  18196  yonedalem4c  18234  intopsn  18613  gsumprval  18647  resmgmhm  18670  resmhm  18779  gsumwsubmcl  18796  gsumsgrpccat  18799  gsumwmhm  18804  frmdup1  18823  frmdup3lem  18825  isghmOLD  19182  resghm  19198  subgga  19266  gasubg  19268  psgnunilem2  19461  sylow2blem2  19587  pj2f  19664  pj1ghm  19669  frgpupf  19739  frgpup3lem  19743  gsumval3  19873  gsummptfzcl  19935  dprdf2  19975  ablfac2  20057  isabvd  20780  abvpropd  20803  cygznlem2a  21557  frgpcyg  21563  psrasclcl  21968  mplasclf  22053  evlssca  22082  lply1binomsc  22286  mat1dimelbas  22446  mat2pmatbas  22701  cpmadugsumlemF  22851  cnpf2  23225  ptpjcn  23586  cnextfres1  24043  cnextfres  24044  cnmpopc  24905  pi1addf  25024  pi1xfrf  25030  pi1cof  25036  mbfmptcl  25613  iblcnlem  25766  limcres  25863  cnplimc  25864  limccnp  25868  limccnp2  25869  limcun  25872  dvidlem  25892  cpnord  25912  dvaddf  25919  dvmulf  25920  dvcmulf  25922  dvcof  25925  dvcj  25927  dvrec  25932  dvmptcl  25936  dvcnvlem  25953  dvcnv  25954  rolle  25967  cmvth  25968  mvth  25969  dvlip  25970  dvlipcn  25971  c1lip2  25975  dv11cn  25978  dvivthlem1  25985  dvivthlem2  25986  dvivth  25987  dvne0  25988  lhop1lem  25990  lhop1  25991  lhop2  25992  lhop  25993  dvcnvrelem2  25995  taylthlem1  26350  taylthlem2  26351  taylthlem2OLD  26352  ulmf2  26362  ulm2  26363  ulmdv  26381  pserdv  26407  rlimcxp  26951  o1cxp  26952  dchrptlem2  27242  axlowdimlem5  29029  axlowdimlem7  29031  axlowdimlem10  29034  uhgrn0  29150  wrdupgr  29168  upgrfn  29170  wrdumgr  29180  umgrfn  29182  upgr2wlk  29750  wlkres  29752  redwlklem  29753  wlkdlem1  29764  uhgrwkspthlem2  29837  usgr2wlkneq  29839  usgr2pthlem  29846  usgr2pth  29847  crctcshwlkn0  29904  wlkiswwlks2lem3  29954  wlkiswwlks2  29958  wlkiswwlksupgr2  29960  wlknewwlksn  29970  wpthswwlks2on  30047  clwlkclwwlklem2a  30083  clwlkclwwlklem1  30084  1wlkdlem1  30222  upgr3v3e3cycl  30265  upgr4cycl4dv4e  30270  isgrpo  30583  vciOLD  30647  isvclem  30663  isnvlem  30696  ajfval  30895  acunirnmpt2  32748  acunirnmpt2f  32749  elrspunidl  33503  lbsdiflsp0  33786  smatrcl  33956  locfinref  34001  1stmbfm  34420  2ndmbfm  34421  sibfof  34500  rrvf2  34608  signshf  34748  reprsuc  34775  pfxwlk  35322  revwlk  35323  cvmliftmolem1  35479  cvmliftlem7  35489  cvmliftlem10  35492  cvmlift2lem9  35509  filnetlem4  36579  poimirlem16  37971  poimirlem19  37974  poimirlem23  37978  poimirlem24  37979  poimirlem25  37980  poimirlem29  37984  poimirlem31  37986  sdclem2  38077  sdclem1  38078  sdc  38079  fdc  38080  sstotbnd2  38109  elghomlem1OLD  38220  rngosn3  38259  sticksstones9  42607  sticksstones11  42609  sticksstones16  42615  frlmfzowrdb  42963  evlselvlem  43033  evlselv  43034  ofoafg  43800  amgm4d  44645  mnurnd  44728  mptelpm  45624  fsneqrn  45658  cncfuni  46332  cncfiooicclem1  46339  dvsubf  46360  dvdivf  46368  dvbdfbdioolem1  46374  ioodvbdlimc1lem1  46377  ioodvbdlimc1lem2  46378  ioodvbdlimc1  46379  ioodvbdlimc2lem  46380  ioodvbdlimc2  46381  dvnprodlem3  46394  itgsubsticclem  46421  fourierdlem48  46600  fourierdlem49  46601  fourierdlem58  46610  fourierdlem59  46611  fourierdlem60  46612  fourierdlem61  46613  fourierdlem69  46621  fourierdlem75  46627  fourierdlem81  46633  fourierdlem89  46641  fourierdlem91  46643  fourierdlem97  46649  fourierdlem113  46665  meaf  46899  ismeannd  46913  psmeasure  46917  omef  46942  isomennd  46977  hoidmvlelem2  47042  hoidmvlelem3  47043  ovnhoi  47049  hspmbllem2  47073  sssmf  47184  smfpimioompt  47232  smffmptf  47250  chnsubseqword  47324  2ffzoeq  47788  fundcmpsurbijinjpreimafv  47879  fargshiftf  47912  upgrimwlklem2  48386  upgrimwlklem4  48388  upgrimpths  48397  gpgprismgr4cycllem9  48591  elbigolo1  49045  naryfvalelwrdf  49121  0aryfvalel  49122  0funcg2  49571  termcfuncval  50019