Theorem feq2d 6679

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1563  ⟶wf 6521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-fn 6528  df-f 6529

This theorem is referenced by:  feq2dd  6681  feq12d  6683  fco  6720  ffdm  6725  fsng  7123  fsn2g  7124  fsnunf2  7174  issmo2  8324  qliftf  8791  elpm2r  8830  ralxpmap  8882  axdc3lem3  10424  axdc3lem4  10425  fseq1p1m1  13617  fseq1m1p1  13618  seqf1o  14070  iswrdi  14544  wrdf  14545  wrdfd  14546  wrdffz  14562  ffz0iswrd  14568  wrdnval  14572  ccatalpha  14621  swrdf  14678  swrdwrdsymb  14690  cats1un  14748  cshwf  14827  wrdlen2i  14969  wwlktovf  14983  rlimi  15554  rlimmptrcl  15649  lo1mptrcl  15663  o1mptrcl  15664  o1fsum  15855  ram0  17072  funcres  17943  curf2cl  18277  uncfcurf  18285  yonedalem4c  18323  intopsn  18702  gsumprval  18736  resmgmhm  18759  resmhm  18869  gsumwsubmcl  18886  gsumsgrpccat  18889  gsumwmhm  18894  frmdup1  18913  frmdup3lem  18915  resghm  19293  subgga  19361  gasubg  19363  psgnunilem2  19556  sylow2blem2  19682  pj2f  19759  pj1ghm  19764  frgpupf  19834  frgpup3lem  19838  gsumval3  19968  gsummptfzcl  20030  dprdf2  20070  ablfac2  20152  isabvd  20884  abvpropd  20907  cygznlem2a  21677  frgpcyg  21683  psrasclcl  22089  mplasclf  22176  evlssca  22205  lply1binomsc  22432  mat1dimelbas  22589  mat2pmatbas  22844  cpmadugsumlemF  22994  cnpf2  23368  ptpjcn  23729  cnextfres1  24186  cnextfres  24187  cnmpopc  25048  pi1addf  25167  pi1xfrf  25173  pi1cof  25179  mbfmptcl  25756  iblcnlem  25909  limcres  26006  cnplimc  26007  limccnp  26011  limccnp2  26012  limcun  26015  dvidlem  26035  cpnord  26055  dvaddf  26062  dvmulf  26063  dvcmulf  26065  dvcof  26068  dvcj  26070  dvrec  26075  dvmptcl  26079  dvcnvlem  26096  dvcnv  26097  rolle  26110  cmvth  26111  mvth  26112  dvlip  26113  dvlipcn  26114  c1lip2  26118  dv11cn  26121  dvivthlem1  26128  dvivthlem2  26129  dvivth  26130  dvne0  26131  lhop1lem  26133  lhop1  26134  lhop2  26135  lhop  26136  dvcnvrelem2  26138  taylthlem1  26494  taylthlem2  26495  ulmf2  26505  ulm2  26506  ulmdv  26524  pserdv  26550  rlimcxp  27096  o1cxp  27097  dchrptlem2  27387  axlowdimlem5  29205  axlowdimlem7  29207  axlowdimlem10  29210  uhgrn0  29326  wrdupgr  29344  upgrfn  29346  wrdumgr  29356  umgrfn  29358  upgr2wlk  29925  wlkres  29927  redwlklem  29928  wlkdlem1  29939  uhgrwkspthlem2  30012  usgr2wlkneq  30014  usgr2pthlem  30021  usgr2pth  30022  crctcshwlkn0  30079  wlkiswwlks2lem3  30129  wlkiswwlks2  30133  wlkiswwlksupgr2  30135  wlknewwlksn  30145  wpthswwlks2on  30222  clwlkclwwlklem2a  30258  clwlkclwwlklem1  30259  1wlkdlem1  30397  upgr3v3e3cycl  30440  upgr4cycl4dv4e  30445  isgrpo  30758  vciOLD  30822  isvclem  30838  isnvlem  30871  ajfval  31070  acunirnmpt2  32917  acunirnmpt2f  32918  elrspunidl  33652  lbsdiflsp0  33933  smatrcl  34103  locfinref  34148  1stmbfm  34567  2ndmbfm  34568  sibfof  34647  rrvf2  34755  signshf  34892  reprsuc  34919  pfxwlk  35487  revwlk  35488  cvmliftmolem1  35644  cvmliftlem7  35654  cvmliftlem10  35657  cvmlift2lem9  35674  filnetlem4  36754  poimirlem16  38147  poimirlem19  38150  poimirlem23  38154  poimirlem24  38155  poimirlem25  38156  poimirlem29  38160  poimirlem31  38162  sdclem2  38253  sdclem1  38254  sdc  38255  fdc  38256  sstotbnd2  38285  elghomlem1OLD  38396  rngosn3  38435  sticksstones9  42783  sticksstones11  42785  sticksstones16  42791  frlmfzowrdb  43138  evlselv  43183  ofoafg  43943  amgm4d  44788  mnurnd  44857  mptelpm  45752  fsneqrn  45785  cncfiooicclem1  46465  dvsubf  46486  dvdivf  46494  dvbdfbdioolem1  46500  ioodvbdlimc1lem1  46503  ioodvbdlimc1lem2  46504  ioodvbdlimc1  46505  ioodvbdlimc2lem  46506  ioodvbdlimc2  46507  dvnprodlem3  46520  itgsubsticclem  46547  fourierdlem58  46736  fourierdlem59  46737  fourierdlem60  46738  fourierdlem61  46739  fourierdlem69  46747  fourierdlem75  46753  fourierdlem81  46759  fourierdlem89  46767  fourierdlem91  46769  fourierdlem97  46775  meaf  47025  ismeannd  47039  psmeasure  47043  omef  47068  isomennd  47103  hoidmvlelem2  47168  hoidmvlelem3  47169  ovnhoi  47175  hspmbllem2  47199  smfpimioompt  47358  smffmptf  47376  chnsubseqword  47452  2ffzoeq  47920  fundcmpsurbijinjpreimafv  48011  fargshiftf  48044  upgrimwlklem2  48518  upgrimwlklem4  48520  upgrimpths  48529  gpgprismgr4cycllem9  48723  elbigolo1  49188  naryfvalelwrdf  49264  0aryfvalel  49265  0funcg2  49713  termcfuncval  50161