Theorem feq2d 6701

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542  ⟶wf 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-fn 6544  df-f 6545

This theorem is referenced by:  feq12d  6703  fco  6739  ffdm  6745  fsng  7132  fsn2g  7133  fsnunf2  7181  issmo2  8346  qliftf  8796  elpm2r  8836  ralxpmap  8887  axdc3lem3  10444  axdc3lem4  10445  fseq1p1m1  13572  fseq1m1p1  13573  seqf1o  14006  iswrdi  14465  wrdf  14466  wrdffz  14482  ffz0iswrd  14488  wrdnval  14492  ccatalpha  14540  swrdf  14597  swrdwrdsymb  14609  cats1un  14668  cshwf  14747  wrdlen2i  14890  wwlktovf  14904  rlimi  15454  rlimmptrcl  15549  lo1mptrcl  15563  o1mptrcl  15564  o1fsum  15756  ram0  16952  funcres  17843  curf2cl  18181  uncfcurf  18189  yonedalem4c  18227  intopsn  18570  gsumprval  18604  resmhm  18698  gsumwsubmcl  18715  gsumsgrpccat  18718  gsumwmhm  18723  frmdup1  18742  frmdup3lem  18744  isghm  19087  resghm  19103  subgga  19159  gasubg  19161  psgnunilem2  19358  sylow2blem2  19484  pj2f  19561  pj1ghm  19566  frgpupf  19636  frgpup3lem  19640  gsumval3  19770  gsummptfzcl  19832  dprdf2  19872  ablfac2  19954  isabvd  20421  abvpropd  20443  cygznlem2a  21115  frgpcyg  21121  mplasclf  21618  evlssca  21644  lply1binomsc  21823  mat1dimelbas  21965  mat2pmatbas  22220  cpmadugsumlemF  22370  cnpf2  22746  ptpjcn  23107  cnextfres1  23564  cnextfres  23565  cnmpopc  24436  pi1addf  24555  pi1xfrf  24561  pi1cof  24567  mbfmptcl  25145  iblcnlem  25298  limcres  25395  cnplimc  25396  limccnp  25400  limccnp2  25401  limcun  25404  dvidlem  25424  cpnord  25444  dvaddf  25451  dvmulf  25452  dvcmulf  25454  dvcof  25457  dvcj  25459  dvrec  25464  dvmptcl  25468  dvcnvlem  25485  dvcnv  25486  rolle  25499  cmvth  25500  mvth  25501  dvlip  25502  dvlipcn  25503  c1lip2  25507  dv11cn  25510  dvivthlem1  25517  dvivthlem2  25518  dvivth  25519  dvne0  25520  lhop1lem  25522  lhop1  25523  lhop2  25524  lhop  25525  dvcnvrelem2  25527  taylthlem1  25877  taylthlem2  25878  ulmf2  25888  ulm2  25889  ulmdv  25907  pserdv  25933  rlimcxp  26468  o1cxp  26469  dchrptlem2  26758  axlowdimlem5  28194  axlowdimlem7  28196  axlowdimlem10  28199  uhgrn0  28317  wrdupgr  28335  upgrfn  28337  wrdumgr  28347  umgrfn  28349  upgr2wlk  28915  wlkres  28917  redwlklem  28918  wlkdlem1  28929  uhgrwkspthlem2  29001  usgr2wlkneq  29003  usgr2pthlem  29010  usgr2pth  29011  crctcshwlkn0  29065  wlkiswwlks2lem3  29115  wlkiswwlks2  29119  wlkiswwlksupgr2  29121  wlknewwlksn  29131  wpthswwlks2on  29205  clwlkclwwlklem2a  29241  clwlkclwwlklem1  29242  1wlkdlem1  29380  upgr3v3e3cycl  29423  upgr4cycl4dv4e  29428  isgrpo  29738  vciOLD  29802  isvclem  29818  isnvlem  29851  ajfval  30050  acunirnmpt2  31873  acunirnmpt2f  31874  wrdfd  32090  elrspunidl  32535  lbsdiflsp0  32700  smatrcl  32765  locfinref  32810  1stmbfm  33248  2ndmbfm  33249  sibfof  33328  rrvf2  33436  signshf  33588  reprsuc  33616  pfxwlk  34103  revwlk  34104  cvmliftmolem1  34261  cvmliftlem7  34271  cvmliftlem10  34274  cvmlift2lem9  34291  gg-cmvth  35170  filnetlem4  35255  poimirlem16  36493  poimirlem19  36496  poimirlem23  36500  poimirlem24  36501  poimirlem25  36502  poimirlem29  36506  poimirlem31  36508  sdclem2  36599  sdclem1  36600  sdc  36601  fdc  36602  sstotbnd2  36631  elghomlem1OLD  36742  rngosn3  36781  sticksstones9  40959  sticksstones11  40961  sticksstones16  40967  frlmfzowrdb  41076  evlselvlem  41156  evlselv  41157  ofoafg  42090  amgm4d  42938  mnurnd  43028  mptelpm  43858  fsneqrn  43896  cncfuni  44589  cncfiooicclem1  44596  dvsubf  44617  dvdivf  44625  dvbdfbdioolem1  44631  ioodvbdlimc1lem1  44634  ioodvbdlimc1lem2  44635  ioodvbdlimc1  44636  ioodvbdlimc2lem  44637  ioodvbdlimc2  44638  dvnprodlem3  44651  itgsubsticclem  44678  fourierdlem48  44857  fourierdlem49  44858  fourierdlem58  44867  fourierdlem59  44868  fourierdlem60  44869  fourierdlem61  44870  fourierdlem69  44878  fourierdlem75  44884  fourierdlem81  44890  fourierdlem89  44898  fourierdlem91  44900  fourierdlem97  44906  fourierdlem113  44922  meaf  45156  ismeannd  45170  psmeasure  45174  omef  45199  isomennd  45234  hoidmvlelem2  45299  hoidmvlelem3  45300  ovnhoi  45306  hspmbllem2  45330  sssmf  45441  smfpimioompt  45489  smffmptf  45507  2ffzoeq  46023  fundcmpsurbijinjpreimafv  46062  fargshiftf  46095  resmgmhm  46555  elbigolo1  47197  naryfvalelwrdf  47273  0aryfvalel  47274