Theorem feq2d 6685

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

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

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 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-fn 6534  df-f 6535

This theorem is used by:  feq2dd  6687  feq12d  6689  fco  6726  ffdm  6731  fsng  7130  fsn2g  7131  fsnunf2  7183  issmo2  8341  qliftf  8810  elpm2r  8849  ralxpmap  8908  axdc3lem3  10511  axdc3lem4  10512  fseq1p1m1  13712  fseq1m1p1  13713  seqf1o  14166  iswrdi  14642  wrdf  14643  wrdfd  14644  wrdffz  14660  ffz0iswrd  14666  wrdnval  14670  ccatalpha  14720  swrdf  14778  swrdwrdsymb  14792  cats1un  14850  cshwf  14931  wrdlen2i  15073  wwlktovf  15089  rlimi  15660  rlimmptrcl  15755  lo1mptrcl  15769  o1mptrcl  15770  o1fsum  15960  ram0  17180  funcres  18051  curf2cl  18385  uncfcurf  18393  yonedalem4c  18431  intopsn  18812  gsumprval  18857  resmgmhm  18880  resmhm  18996  gsumwsubmcl  19013  gsumsgrpccat  19016  gsumwmhm  19021  frmdup1  19040  frmdup3lem  19042  resghm  19426  subgga  19494  gasubg  19496  psgnunilem2  19689  sylow2blem2  19815  pj2f  19892  pj1ghm  19897  frgpupf  19967  frgpup3lem  19971  gsumval3  20101  gsummptfzcl  20163  dprdf2  20203  ablfac2  20285  isabvd  21049  abvpropd  21072  cygznlem2a  21853  frgpcyg  21859  psrasclcl  22267  mplasclf  22354  evlssca  22383  lply1binomsc  22609  mat1dimelbas  22766  mat2pmatbas  23024  cpmadugsumlemF  23174  cnpf2  23548  ptpjcn  23910  cnextfres1  24367  cnextfres  24368  cnmpopc  25229  pi1addf  25348  pi1xfrf  25354  pi1cof  25360  mbfmptcl  25937  iblcnlem  26089  limcres  26186  cnplimc  26187  limccnp  26191  limccnp2  26192  limcun  26195  dvidlem  26215  cpnord  26235  dvaddf  26242  dvmulf  26243  dvcmulf  26245  dvcof  26248  dvcj  26250  dvrec  26255  dvmptcl  26259  dvcnvlem  26276  dvcnv  26277  rolle  26290  cmvth  26291  mvth  26292  dvlip  26293  dvlipcn  26294  c1lip2  26298  dv11cn  26301  dvivthlem1  26308  dvivthlem2  26309  dvivth  26310  dvne0  26311  lhop1lem  26313  lhop1  26314  lhop2  26315  lhop  26316  dvcnvrelem2  26318  taylthlem1  26682  taylthlem2  26683  ulmf2  26693  ulm2  26694  ulmdv  26712  pserdv  26738  rlimcxp  27283  o1cxp  27284  dchrptlem2  27574  axlowdimlem5  29506  axlowdimlem7  29508  axlowdimlem10  29511  uhgrn0  29627  wrdupgr  29645  upgrfn  29647  wrdumgr  29657  umgrfn  29659  upgr2wlk  30229  wlkres  30231  redwlklem  30232  wlkdlem1  30243  pfxwlk  30248  revwlk  30249  uhgrwkspthlem2  30322  usgr2wlkneq  30324  usgr2pthlem  30331  usgr2pth  30332  crctcshwlkn0  30392  wlkiswwlks2lem3  30442  wlkiswwlks2  30446  wlkiswwlksupgr2  30448  wlknewwlksn  30458  wpthswwlks2on  30535  clwlkclwwlklem2a  30571  clwlkclwwlklem1  30572  1wlkdlem1  30710  upgr3v3e3cycl  30763  upgr4cycl4dv4e  30768  isgrpo  31081  vciOLD  31145  isvclem  31161  isnvlem  31194  ajfval  31393  acunirnmpt2  33236  acunirnmpt2f  33237  elrspunidl  33960  lbsdiflsp0  34240  smatrcl  34410  locfinref  34455  1stmbfm  34875  2ndmbfm  34876  sibfof  34955  rrvf2  35063  signshf  35200  reprsuc  35227  cvmliftmolem1  36015  cvmliftlem7  36025  cvmliftlem10  36028  cvmlift2lem9  36045  filnetlem4  37139  poimirlem16  38522  poimirlem19  38525  poimirlem23  38529  poimirlem24  38530  poimirlem25  38531  poimirlem29  38535  poimirlem31  38537  sdclem2  38644  sdclem1  38645  sdc  38646  fdc  38647  sstotbnd2  38676  elghomlem1OLD  38787  rngosn3  38826  sticksstones9  43172  sticksstones11  43174  sticksstones16  43180  frlmfzowrdb  43536  evlselv  43579  ofoafg  44314  amgm4d  45159  mnurnd  45226  mptelpm  46134  fsneqrn  46167  cncfiooicclem1  46847  dvsubf  46868  dvdivf  46876  dvbdfbdioolem1  46882  ioodvbdlimc1lem1  46885  ioodvbdlimc1lem2  46886  ioodvbdlimc1  46887  ioodvbdlimc2lem  46888  ioodvbdlimc2  46889  dvnprodlem3  46902  itgsubsticclem  46929  fourierdlem58  47118  fourierdlem59  47119  fourierdlem60  47120  fourierdlem61  47121  fourierdlem69  47129  fourierdlem75  47135  fourierdlem81  47141  fourierdlem89  47149  fourierdlem91  47151  fourierdlem97  47157  meaf  47407  ismeannd  47421  psmeasure  47425  omef  47450  isomennd  47485  hoidmvlelem2  47550  hoidmvlelem3  47551  ovnhoi  47557  hspmbllem2  47581  smfpimioompt  47740  smffmptf  47758  chnsubseqword  47832  2ffzoeq  48342  fundcmpsurbijinjpreimafv  48433  fargshiftf  48466  upgrimwlklem2  48940  upgrimwlklem4  48942  upgrimpths  48951  gpgprismgr4cycllem9  49145  elbigolo1  49613  naryfvalelwrdf  49689  0aryfvalel  49690  0funcg2  50136  termcfuncval  50584