Theorem feq2d 6691

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570  ⟶wf 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-fn 6541  df-f 6542

This theorem is referenced by:  feq2dd  6693  feq12d  6695  fco  6732  ffdm  6737  fsng  7135  fsn2g  7136  fsnunf2  7186  issmo2  8337  qliftf  8804  elpm2r  8843  ralxpmap  8895  axdc3lem3  10437  axdc3lem4  10438  fseq1p1m1  13628  fseq1m1p1  13629  seqf1o  14081  iswrdi  14556  wrdf  14557  wrdfd  14558  wrdffz  14574  ffz0iswrd  14580  wrdnval  14584  ccatalpha  14633  swrdf  14690  swrdwrdsymb  14702  cats1un  14760  cshwf  14839  wrdlen2i  14981  wwlktovf  14995  rlimi  15566  rlimmptrcl  15661  lo1mptrcl  15675  o1mptrcl  15676  o1fsum  15867  ram0  17083  funcres  17954  curf2cl  18288  uncfcurf  18296  yonedalem4c  18334  intopsn  18713  gsumprval  18747  resmgmhm  18770  resmhm  18880  gsumwsubmcl  18897  gsumsgrpccat  18900  gsumwmhm  18905  frmdup1  18924  frmdup3lem  18926  resghm  19303  subgga  19371  gasubg  19373  psgnunilem2  19566  sylow2blem2  19692  pj2f  19769  pj1ghm  19774  frgpupf  19844  frgpup3lem  19848  gsumval3  19978  gsummptfzcl  20040  dprdf2  20080  ablfac2  20162  isabvd  20896  abvpropd  20919  cygznlem2a  21698  frgpcyg  21704  psrasclcl  22110  mplasclf  22197  evlssca  22226  lply1binomsc  22452  mat1dimelbas  22609  mat2pmatbas  22864  cpmadugsumlemF  23014  cnpf2  23388  ptpjcn  23749  cnextfres1  24206  cnextfres  24207  cnmpopc  25068  pi1addf  25187  pi1xfrf  25193  pi1cof  25199  mbfmptcl  25776  iblcnlem  25929  limcres  26026  cnplimc  26027  limccnp  26031  limccnp2  26032  limcun  26035  dvidlem  26055  cpnord  26075  dvaddf  26082  dvmulf  26083  dvcmulf  26085  dvcof  26088  dvcj  26090  dvrec  26095  dvmptcl  26099  dvcnvlem  26116  dvcnv  26117  rolle  26130  cmvth  26131  mvth  26132  dvlip  26133  dvlipcn  26134  c1lip2  26138  dv11cn  26141  dvivthlem1  26148  dvivthlem2  26149  dvivth  26150  dvne0  26151  lhop1lem  26153  lhop1  26154  lhop2  26155  lhop  26156  dvcnvrelem2  26158  taylthlem1  26514  taylthlem2  26515  ulmf2  26525  ulm2  26526  ulmdv  26544  pserdv  26570  rlimcxp  27116  o1cxp  27117  dchrptlem2  27407  axlowdimlem5  29274  axlowdimlem7  29276  axlowdimlem10  29279  uhgrn0  29395  wrdupgr  29413  upgrfn  29415  wrdumgr  29425  umgrfn  29427  upgr2wlk  29994  wlkres  29996  redwlklem  29997  wlkdlem1  30008  uhgrwkspthlem2  30081  usgr2wlkneq  30083  usgr2pthlem  30090  usgr2pth  30091  crctcshwlkn0  30148  wlkiswwlks2lem3  30198  wlkiswwlks2  30202  wlkiswwlksupgr2  30204  wlknewwlksn  30214  wpthswwlks2on  30291  clwlkclwwlklem2a  30327  clwlkclwwlklem1  30328  1wlkdlem1  30466  upgr3v3e3cycl  30509  upgr4cycl4dv4e  30514  isgrpo  30827  vciOLD  30891  isvclem  30907  isnvlem  30940  ajfval  31139  acunirnmpt2  32983  acunirnmpt2f  32984  elrspunidl  33714  lbsdiflsp0  33994  smatrcl  34164  locfinref  34209  1stmbfm  34628  2ndmbfm  34629  sibfof  34708  rrvf2  34816  signshf  34953  reprsuc  34980  pfxwlk  35594  revwlk  35595  cvmliftmolem1  35751  cvmliftlem7  35761  cvmliftlem10  35764  cvmlift2lem9  35781  filnetlem4  36870  poimirlem16  38265  poimirlem19  38268  poimirlem23  38272  poimirlem24  38273  poimirlem25  38274  poimirlem29  38278  poimirlem31  38280  sdclem2  38371  sdclem1  38372  sdc  38373  fdc  38374  sstotbnd2  38403  elghomlem1OLD  38514  rngosn3  38553  sticksstones9  42899  sticksstones11  42901  sticksstones16  42907  frlmfzowrdb  43256  evlselv  43301  ofoafg  44061  amgm4d  44906  mnurnd  44973  mptelpm  45874  fsneqrn  45907  cncfiooicclem1  46587  dvsubf  46608  dvdivf  46616  dvbdfbdioolem1  46622  ioodvbdlimc1lem1  46625  ioodvbdlimc1lem2  46626  ioodvbdlimc1  46627  ioodvbdlimc2lem  46628  ioodvbdlimc2  46629  dvnprodlem3  46642  itgsubsticclem  46669  fourierdlem58  46858  fourierdlem59  46859  fourierdlem60  46860  fourierdlem61  46861  fourierdlem69  46869  fourierdlem75  46875  fourierdlem81  46881  fourierdlem89  46889  fourierdlem91  46891  fourierdlem97  46897  meaf  47147  ismeannd  47161  psmeasure  47165  omef  47190  isomennd  47225  hoidmvlelem2  47290  hoidmvlelem3  47291  ovnhoi  47297  hspmbllem2  47321  smfpimioompt  47480  smffmptf  47498  chnsubseqword  47574  2ffzoeq  48042  fundcmpsurbijinjpreimafv  48133  fargshiftf  48166  upgrimwlklem2  48640  upgrimwlklem4  48642  upgrimpths  48651  gpgprismgr4cycllem9  48845  elbigolo1  49314  naryfvalelwrdf  49390  0aryfvalel  49391  0funcg2  49839  termcfuncval  50287