Theorem feq2d 6635

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ⟶wf 6477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-fn 6484  df-f 6485

This theorem is referenced by:  feq2dd  6637  feq12d  6639  fco  6675  ffdm  6680  fsng  7070  fsn2g  7071  fsnunf2  7120  issmo2  8269  qliftf  8729  elpm2r  8769  ralxpmap  8820  axdc3lem3  10340  axdc3lem4  10341  fseq1p1m1  13495  fseq1m1p1  13496  seqf1o  13947  iswrdi  14421  wrdf  14422  wrdfd  14423  wrdffz  14439  ffz0iswrd  14445  wrdnval  14449  ccatalpha  14498  swrdf  14555  swrdwrdsymb  14567  cats1un  14625  cshwf  14704  wrdlen2i  14846  wwlktovf  14860  rlimi  15417  rlimmptrcl  15512  lo1mptrcl  15526  o1mptrcl  15527  o1fsum  15717  ram0  16931  funcres  17800  curf2cl  18134  uncfcurf  18142  yonedalem4c  18180  intopsn  18559  gsumprval  18593  resmgmhm  18616  resmhm  18725  gsumwsubmcl  18742  gsumsgrpccat  18745  gsumwmhm  18750  frmdup1  18769  frmdup3lem  18771  isghmOLD  19126  resghm  19142  subgga  19210  gasubg  19212  psgnunilem2  19405  sylow2blem2  19531  pj2f  19608  pj1ghm  19613  frgpupf  19683  frgpup3lem  19687  gsumval3  19817  gsummptfzcl  19879  dprdf2  19919  ablfac2  20001  isabvd  20725  abvpropd  20748  cygznlem2a  21502  frgpcyg  21508  psrasclcl  21915  mplasclf  21998  evlssca  22022  lply1binomsc  22224  mat1dimelbas  22384  mat2pmatbas  22639  cpmadugsumlemF  22789  cnpf2  23163  ptpjcn  23524  cnextfres1  23981  cnextfres  23982  cnmpopc  24847  pi1addf  24972  pi1xfrf  24978  pi1cof  24984  mbfmptcl  25562  iblcnlem  25715  limcres  25812  cnplimc  25813  limccnp  25817  limccnp2  25818  limcun  25821  dvidlem  25841  cpnord  25862  dvaddf  25870  dvmulf  25871  dvcmulf  25873  dvcof  25877  dvcj  25879  dvrec  25884  dvmptcl  25888  dvcnvlem  25905  dvcnv  25906  rolle  25919  cmvth  25920  cmvthOLD  25921  mvth  25922  dvlip  25923  dvlipcn  25924  c1lip2  25928  dv11cn  25931  dvivthlem1  25938  dvivthlem2  25939  dvivth  25940  dvne0  25941  lhop1lem  25943  lhop1  25944  lhop2  25945  lhop  25946  dvcnvrelem2  25948  taylthlem1  26306  taylthlem2  26307  taylthlem2OLD  26308  ulmf2  26318  ulm2  26319  ulmdv  26337  pserdv  26364  rlimcxp  26909  o1cxp  26910  dchrptlem2  27201  axlowdimlem5  28922  axlowdimlem7  28924  axlowdimlem10  28927  uhgrn0  29043  wrdupgr  29061  upgrfn  29063  wrdumgr  29073  umgrfn  29075  upgr2wlk  29643  wlkres  29645  redwlklem  29646  wlkdlem1  29657  uhgrwkspthlem2  29730  usgr2wlkneq  29732  usgr2pthlem  29739  usgr2pth  29740  crctcshwlkn0  29797  wlkiswwlks2lem3  29847  wlkiswwlks2  29851  wlkiswwlksupgr2  29853  wlknewwlksn  29863  wpthswwlks2on  29937  clwlkclwwlklem2a  29973  clwlkclwwlklem1  29974  1wlkdlem1  30112  upgr3v3e3cycl  30155  upgr4cycl4dv4e  30160  isgrpo  30472  vciOLD  30536  isvclem  30552  isnvlem  30585  ajfval  30784  acunirnmpt2  32637  acunirnmpt2f  32638  elrspunidl  33388  lbsdiflsp0  33634  smatrcl  33804  locfinref  33849  1stmbfm  34268  2ndmbfm  34269  sibfof  34348  rrvf2  34456  signshf  34596  reprsuc  34623  pfxwlk  35156  revwlk  35157  cvmliftmolem1  35313  cvmliftlem7  35323  cvmliftlem10  35326  cvmlift2lem9  35343  filnetlem4  36414  poimirlem16  37675  poimirlem19  37678  poimirlem23  37682  poimirlem24  37683  poimirlem25  37684  poimirlem29  37688  poimirlem31  37690  sdclem2  37781  sdclem1  37782  sdc  37783  fdc  37784  sstotbnd2  37813  elghomlem1OLD  37924  rngosn3  37963  sticksstones9  42186  sticksstones11  42188  sticksstones16  42194  frlmfzowrdb  42536  evlselvlem  42618  evlselv  42619  ofoafg  43386  amgm4d  44232  mnurnd  44315  mptelpm  45212  fsneqrn  45247  cncfuni  45923  cncfiooicclem1  45930  dvsubf  45951  dvdivf  45959  dvbdfbdioolem1  45965  ioodvbdlimc1lem1  45968  ioodvbdlimc1lem2  45969  ioodvbdlimc1  45970  ioodvbdlimc2lem  45971  ioodvbdlimc2  45972  dvnprodlem3  45985  itgsubsticclem  46012  fourierdlem48  46191  fourierdlem49  46192  fourierdlem58  46201  fourierdlem59  46202  fourierdlem60  46203  fourierdlem61  46204  fourierdlem69  46212  fourierdlem75  46218  fourierdlem81  46224  fourierdlem89  46232  fourierdlem91  46234  fourierdlem97  46240  fourierdlem113  46256  meaf  46490  ismeannd  46504  psmeasure  46508  omef  46533  isomennd  46568  hoidmvlelem2  46633  hoidmvlelem3  46634  ovnhoi  46640  hspmbllem2  46664  sssmf  46775  smfpimioompt  46823  smffmptf  46841  2ffzoeq  47357  fundcmpsurbijinjpreimafv  47437  fargshiftf  47470  upgrimwlklem2  47928  upgrimwlklem4  47930  upgrimpths  47939  gpgprismgr4cycllem9  48133  elbigolo1  48588  naryfvalelwrdf  48664  0aryfvalel  48665  0funcg2  49115  termcfuncval  49563