Theorem feq2d 6500

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1542  ⟶wf 6345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-cleq 2731  df-fn 6352  df-f 6353

This theorem is referenced by:  feq12d  6502  fco  6538  ffdm  6544  fsng  6921  fsn2g  6922  fsnunf2  6970  issmo2  8027  qliftf  8428  elpm2r  8467  ralxpmap  8518  axdc3lem3  9964  axdc3lem4  9965  fseq1p1m1  13084  fseq1m1p1  13085  seqf1o  13515  iswrdi  13971  wrdf  13972  wrdffz  13988  ffz0iswrd  13994  wrdnval  13998  ccatalpha  14048  swrdf  14113  swrdwrdsymb  14125  cats1un  14184  cshwf  14263  wrdlen2i  14405  wwlktovf  14421  rlimi  14972  rlimmptrcl  15067  lo1mptrcl  15081  o1mptrcl  15082  o1fsum  15273  ram0  16470  funcres  17283  curf2cl  17609  uncfcurf  17617  yonedalem4c  17655  intopsn  17992  gsumprval  18026  resmhm  18113  gsumwsubmcl  18129  gsumsgrpccat  18132  gsumccatOLD  18133  gsumwmhm  18138  frmdup1  18157  frmdup3lem  18159  isghm  18488  resghm  18504  subgga  18560  gasubg  18562  psgnunilem2  18753  sylow2blem2  18876  pj2f  18954  pj1ghm  18959  frgpupf  19029  frgpup3lem  19033  gsumval3  19158  gsummptfzcl  19220  dprdf2  19260  ablfac2  19342  isabvd  19722  abvpropd  19744  cygznlem2a  20398  frgpcyg  20404  mplasclf  20889  evlssca  20915  lply1binomsc  21094  mat1dimelbas  21234  mat2pmatbas  21489  cpmadugsumlemF  21639  cnpf2  22013  ptpjcn  22374  cnextfres1  22831  cnextfres  22832  cnmpopc  23692  pi1addf  23811  pi1xfrf  23817  pi1cof  23823  mbfmptcl  24400  iblcnlem  24553  limcres  24650  cnplimc  24651  limccnp  24655  limccnp2  24656  limcun  24659  dvidlem  24679  cpnord  24699  dvaddf  24706  dvmulf  24707  dvcmulf  24709  dvcof  24712  dvcj  24714  dvrec  24719  dvmptcl  24723  dvcnvlem  24740  dvcnv  24741  rolle  24754  cmvth  24755  mvth  24756  dvlip  24757  dvlipcn  24758  c1lip2  24762  dv11cn  24765  dvivthlem1  24772  dvivthlem2  24773  dvivth  24774  dvne0  24775  lhop1lem  24777  lhop1  24778  lhop2  24779  lhop  24780  dvcnvrelem2  24782  taylthlem1  25132  taylthlem2  25133  ulmf2  25143  ulm2  25144  ulmdv  25162  pserdv  25188  rlimcxp  25723  o1cxp  25724  dchrptlem2  26013  axlowdimlem5  26904  axlowdimlem7  26906  axlowdimlem10  26909  uhgrn0  27024  wrdupgr  27042  upgrfn  27044  wrdumgr  27054  umgrfn  27056  upgr2wlk  27622  wlkres  27624  redwlklem  27625  wlkdlem1  27636  uhgrwkspthlem2  27707  usgr2wlkneq  27709  usgr2pthlem  27716  usgr2pth  27717  crctcshwlkn0  27771  wlkiswwlks2lem3  27821  wlkiswwlks2  27825  wlkiswwlksupgr2  27827  wlknewwlksn  27837  wpthswwlks2on  27911  clwlkclwwlklem2a  27947  clwlkclwwlklem1  27948  1wlkdlem1  28086  upgr3v3e3cycl  28129  upgr4cycl4dv4e  28134  isgrpo  28444  vciOLD  28508  isvclem  28524  isnvlem  28557  ajfval  28756  acunirnmpt2  30584  acunirnmpt2f  30585  wrdfd  30797  elrspunidl  31190  lbsdiflsp0  31291  smatrcl  31330  locfinref  31375  1stmbfm  31809  2ndmbfm  31810  sibfof  31889  rrvf2  31997  signshf  32149  reprsuc  32177  pfxwlk  32668  revwlk  32669  cvmliftmolem1  32826  cvmliftlem7  32836  cvmliftlem10  32839  cvmlift2lem9  32856  filnetlem4  34225  poimirlem16  35448  poimirlem19  35451  poimirlem23  35455  poimirlem24  35456  poimirlem25  35457  poimirlem29  35461  poimirlem31  35463  sdclem2  35555  sdclem1  35556  sdc  35557  fdc  35558  sstotbnd2  35587  elghomlem1OLD  35698  rngosn3  35737  sticksstones9  39748  sticksstones11  39750  frlmfzowrdb  39857  amgm4d  41398  mnurnd  41483  mptelpm  42290  fsneqrn  42329  cncfuni  43009  cncfiooicclem1  43016  dvsubf  43037  dvdivf  43045  dvbdfbdioolem1  43051  ioodvbdlimc1lem1  43054  ioodvbdlimc1lem2  43055  ioodvbdlimc1  43056  ioodvbdlimc2lem  43057  ioodvbdlimc2  43058  dvnprodlem3  43071  itgsubsticclem  43098  fourierdlem48  43277  fourierdlem49  43278  fourierdlem58  43287  fourierdlem59  43288  fourierdlem60  43289  fourierdlem61  43290  fourierdlem69  43298  fourierdlem75  43304  fourierdlem81  43310  fourierdlem89  43318  fourierdlem91  43320  fourierdlem97  43326  fourierdlem113  43342  meaf  43573  ismeannd  43587  psmeasure  43591  omef  43616  isomennd  43651  hoidmvlelem2  43716  hoidmvlelem3  43717  ovnhoi  43723  hspmbllem2  43747  sssmf  43853  smfpimioompt  43899  smffmpt  43917  2ffzoeq  44401  fundcmpsurbijinjpreimafv  44440  fargshiftf  44473  resmgmhm  44933  elbigolo1  45484  naryfvalelwrdf  45560  0aryfvalel  45561