Theorem feq2d 6696

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ⟶wf 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-fn 6546  df-f 6547

This theorem is used by:  feq2dd  6698  feq12d  6700  fco  6737  ffdm  6742  fsng  7140  fsn2g  7141  fsnunf2  7191  issmo2  8345  qliftf  8812  elpm2r  8851  ralxpmap  8903  axdc3lem3  10454  axdc3lem4  10455  fseq1p1m1  13645  fseq1m1p1  13646  seqf1o  14099  iswrdi  14574  wrdf  14575  wrdfd  14576  wrdffz  14592  ffz0iswrd  14598  wrdnval  14602  ccatalpha  14652  swrdf  14710  swrdwrdsymb  14724  cats1un  14782  cshwf  14863  wrdlen2i  15005  wwlktovf  15019  rlimi  15590  rlimmptrcl  15685  lo1mptrcl  15699  o1mptrcl  15700  o1fsum  15891  ram0  17107  funcres  17978  curf2cl  18312  uncfcurf  18320  yonedalem4c  18358  intopsn  18737  gsumprval  18775  resmgmhm  18798  resmhm  18910  gsumwsubmcl  18927  gsumsgrpccat  18930  gsumwmhm  18935  frmdup1  18954  frmdup3lem  18956  resghm  19333  subgga  19401  gasubg  19403  psgnunilem2  19596  sylow2blem2  19722  pj2f  19799  pj1ghm  19804  frgpupf  19874  frgpup3lem  19878  gsumval3  20008  gsummptfzcl  20070  dprdf2  20110  ablfac2  20192  isabvd  20952  abvpropd  20975  cygznlem2a  21754  frgpcyg  21760  psrasclcl  22166  mplasclf  22253  evlssca  22282  lply1binomsc  22508  mat1dimelbas  22665  mat2pmatbas  22920  cpmadugsumlemF  23070  cnpf2  23444  ptpjcn  23805  cnextfres1  24262  cnextfres  24263  cnmpopc  25124  pi1addf  25243  pi1xfrf  25249  pi1cof  25255  mbfmptcl  25832  iblcnlem  25985  limcres  26082  cnplimc  26083  limccnp  26087  limccnp2  26088  limcun  26091  dvidlem  26111  cpnord  26131  dvaddf  26138  dvmulf  26139  dvcmulf  26141  dvcof  26144  dvcj  26146  dvrec  26151  dvmptcl  26155  dvcnvlem  26172  dvcnv  26173  rolle  26186  cmvth  26187  mvth  26188  dvlip  26189  dvlipcn  26190  c1lip2  26194  dv11cn  26197  dvivthlem1  26204  dvivthlem2  26205  dvivth  26206  dvne0  26207  lhop1lem  26209  lhop1  26210  lhop2  26211  lhop  26212  dvcnvrelem2  26214  taylthlem1  26573  taylthlem2  26574  ulmf2  26584  ulm2  26585  ulmdv  26603  pserdv  26629  rlimcxp  27175  o1cxp  27176  dchrptlem2  27466  axlowdimlem5  29333  axlowdimlem7  29335  axlowdimlem10  29338  uhgrn0  29454  wrdupgr  29472  upgrfn  29474  wrdumgr  29484  umgrfn  29486  upgr2wlk  30053  wlkres  30055  redwlklem  30056  wlkdlem1  30067  uhgrwkspthlem2  30140  usgr2wlkneq  30142  usgr2pthlem  30149  usgr2pth  30150  crctcshwlkn0  30207  wlkiswwlks2lem3  30257  wlkiswwlks2  30261  wlkiswwlksupgr2  30263  wlknewwlksn  30273  wpthswwlks2on  30350  clwlkclwwlklem2a  30386  clwlkclwwlklem1  30387  1wlkdlem1  30525  upgr3v3e3cycl  30568  upgr4cycl4dv4e  30573  isgrpo  30886  vciOLD  30950  isvclem  30966  isnvlem  30999  ajfval  31198  acunirnmpt2  33042  acunirnmpt2f  33043  elrspunidl  33767  lbsdiflsp0  34047  smatrcl  34217  locfinref  34262  1stmbfm  34681  2ndmbfm  34682  sibfof  34761  rrvf2  34869  signshf  35006  reprsuc  35033  pfxwlk  35636  revwlk  35637  cvmliftmolem1  35793  cvmliftlem7  35803  cvmliftlem10  35806  cvmlift2lem9  35823  filnetlem4  36932  poimirlem16  38327  poimirlem19  38330  poimirlem23  38334  poimirlem24  38335  poimirlem25  38336  poimirlem29  38340  poimirlem31  38342  sdclem2  38433  sdclem1  38434  sdc  38435  fdc  38436  sstotbnd2  38465  elghomlem1OLD  38576  rngosn3  38615  sticksstones9  42961  sticksstones11  42963  sticksstones16  42969  frlmfzowrdb  43318  evlselv  43361  ofoafg  44121  amgm4d  44966  mnurnd  45033  mptelpm  45934  fsneqrn  45967  cncfiooicclem1  46647  dvsubf  46668  dvdivf  46676  dvbdfbdioolem1  46682  ioodvbdlimc1lem1  46685  ioodvbdlimc1lem2  46686  ioodvbdlimc1  46687  ioodvbdlimc2lem  46688  ioodvbdlimc2  46689  dvnprodlem3  46702  itgsubsticclem  46729  fourierdlem58  46918  fourierdlem59  46919  fourierdlem60  46920  fourierdlem61  46921  fourierdlem69  46929  fourierdlem75  46935  fourierdlem81  46941  fourierdlem89  46949  fourierdlem91  46951  fourierdlem97  46957  meaf  47207  ismeannd  47221  psmeasure  47225  omef  47250  isomennd  47285  hoidmvlelem2  47350  hoidmvlelem3  47351  ovnhoi  47357  hspmbllem2  47381  smfpimioompt  47540  smffmptf  47558  chnsubseqword  47634  2ffzoeq  48105  fundcmpsurbijinjpreimafv  48196  fargshiftf  48229  upgrimwlklem2  48703  upgrimwlklem4  48705  upgrimpths  48714  gpgprismgr4cycllem9  48908  elbigolo1  49377  naryfvalelwrdf  49453  0aryfvalel  49454  0funcg2  49902  termcfuncval  50350