MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  feq2d Structured version   Visualization version   Unicode version

Theorem feq2d 5737
Description: Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
feq2d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
feq2d  |-  ( ph  ->  ( F : A --> C 
<->  F : B --> C ) )

Proof of Theorem feq2d
StepHypRef Expression
1 feq2d.1 . 2  |-  ( ph  ->  A  =  B )
2 feq2 5733 . 2  |-  ( A  =  B  ->  ( F : A --> C  <->  F : B
--> C ) )
31, 2syl 17 1  |-  ( ph  ->  ( F : A --> C 
<->  F : B --> C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    = wceq 1455   -->wf 5597
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-cleq 2455  df-fn 5604  df-f 5605
This theorem is referenced by:  feq12d  5739  ffdm  5766  fsng  6087  fsn2g  6088  fsnunf2  6127  issmo2  7094  qliftf  7477  elpm2r  7515  ralxpmap  7547  ordtypelem5  8063  axdc3lem3  8908  axdc3lem4  8909  fseq1p1m1  11897  fseq1m1p1  11898  seqf1o  12286  iswrdi  12708  wrdf  12709  snopiswrd  12714  wrdffz  12724  ffz0iswrd  12730  wrdnval  12733  swrdf  12818  swrd0f  12820  cats1un  12869  cshwf  12939  wrdlen2i  13067  wwlktovf  13080  rlimi  13626  rlimmptrcl  13720  lo1mptrcl  13734  o1mptrcl  13735  o1fsum  13922  ram0  15029  funcres  15850  curf2cl  16165  uncfcurf  16173  yonedalem4c  16211  intopsn  16547  gsumprval  16573  resmhm  16655  gsumwsubmcl  16671  gsumccat  16674  gsumwmhm  16678  frmdup1  16697  frmdup3lem  16699  isghm  16932  resghm  16948  subgga  17003  gasubg  17005  psgnunilem2  17185  sylow2blem2  17322  pj2f  17397  pj1ghm  17402  frgpupf  17472  frgpup3lem  17476  gsumval3  17590  gsummptfzcl  17650  dprdf2  17688  ablfaclem2  17768  ablfac2  17771  isabvd  18097  abvpropd  18119  mplasclf  18769  evlssca  18794  lply1binomsc  18950  cygznlem2a  19187  frgpcyg  19193  mat1dimelbas  19545  mat2pmatbas  19799  cpmadugsumlemF  19949  cnpf2  20315  lmcnp  20369  ptpjcn  20675  pt1hmeo  20870  cnextfres1  21132  cnextfres  21133  cnmpt2pc  22005  pi1addf  22127  pi1xfrf  22133  pi1cof  22139  mbfmptcl  22642  iblcnlem  22795  limcres  22890  cnplimc  22891  limccnp  22895  limccnp2  22896  limcun  22899  dvidlem  22919  cpnord  22938  dvaddf  22945  dvmulf  22946  dvcmulf  22948  dvcof  22951  dvcj  22953  dvrec  22958  dvmptcl  22962  dvcnvlem  22977  dvcnv  22978  rolle  22991  cmvth  22992  mvth  22993  dvlip  22994  dvlipcn  22995  c1lip2  22999  dv11cn  23002  dvivthlem1  23009  dvivthlem2  23010  dvivth  23011  dvne0  23012  lhop1lem  23014  lhop1  23015  lhop2  23016  lhop  23017  dvcnvrelem2  23019  taylthlem1  23377  taylthlem2  23378  ulmf2  23388  ulm2  23389  ulmdv  23407  pserdv  23433  rlimcxp  23948  o1cxp  23949  dchrptlem2  24242  axlowdimlem5  25025  axlowdimlem7  25027  axlowdimlem10  25030  uhgraun  25087  wrdumgra  25092  umgraf  25094  umgra1  25102  umgraun  25104  wlkelwrd  25307  2trllemH  25331  2trllemG  25337  is2wlk  25344  redwlk  25385  usgra2adedgwlkonALT  25393  usgra2wlkspthlem1  25396  usgra2wlkspthlem2  25397  fargshiftf  25413  3v3e3cycl1  25421  4cycl4v4e  25443  4cycl4dv  25444  4cycl4dv4e  25445  wlkiswwlk2lem3  25470  wlkiswwlk2  25474  vfwlkniswwlkn  25483  clwlkisclwwlklem2a  25562  clwlkisclwwlklem2  25563  clwlkfclwwlk2wrd  25617  clwlkf1clwwlklem3  25625  el2wlkonotlem  25639  eupai  25744  eupatrl  25745  eupa0  25751  eupares  25752  eupap1  25753  isgrpo  25973  elghomlem1OLD  26138  rngosn3  26203  vci  26216  isvclem  26245  vcoprnelem  26246  isnvlem  26278  ajfval  26499  acunirnmpt2  28311  acunirnmpt2f  28312  smatrcl  28671  locfinref  28717  1stmbfm  29131  2ndmbfm  29132  sibfof  29222  rrvf2  29330  signshf  29526  cvmliftmolem1  30053  cvmliftlem7  30063  cvmliftlem10  30066  cvmlift2lem9  30083  filnetlem4  31086  poimirlem16  32001  poimirlem19  32004  poimirlem23  32008  poimirlem24  32009  poimirlem25  32010  poimirlem29  32014  poimirlem31  32016  sdclem2  32116  sdclem1  32117  sdc  32118  fdc  32119  sstotbnd2  32151  amgm4d  36696  mptelpm  37479  cncfuni  37802  cncfiooicclem1  37809  dvsubf  37822  dvdivf  37832  dvbdfbdioolem1  37838  ioodvbdlimc1lem1  37841  ioodvbdlimc1lem2  37842  ioodvbdlimc1lem1OLD  37843  ioodvbdlimc1lem2OLD  37844  ioodvbdlimc1  37845  ioodvbdlimc2lem  37846  ioodvbdlimc2lemOLD  37847  ioodvbdlimc2  37848  dvnprodlem3  37861  itgsubsticclem  37890  fourierdlem48  38056  fourierdlem49  38057  fourierdlem58  38066  fourierdlem59  38067  fourierdlem60  38068  fourierdlem61  38069  fourierdlem69  38077  fourierdlem75  38083  fourierdlem81  38089  fourierdlem89  38097  fourierdlem91  38099  fourierdlem97  38105  fourierdlem113  38121  meaf  38329  ismeannd  38343  psmeasure  38347  omef  38355  isomennd  38390  hoidmvlelem2  38456  hoidmvlelem3  38457  ovnhoi  38463  hspmbllem2  38487  fdisjdmun  38668  2ffzoeq  39106  uhgrn0  39204  uhgrun  39214  wrdupgr  39224  upgrfn  39226  wrdumgr  39234  umgrfn  39236  upgr1e  39249  upgrun  39254  umgrun  39256  upgrres1  39430  umgrres1  39431  umgr2v2e  39612  seqvtx1wlk  39682  upgr2wlk  39715  red1wlklem  39716  1wlkdlem1  39725  uhgr1wlkspthlem2  39786  usgr2wlkneq  39788  11wlkdlem1  39852  upgr3v3e3cycl  39921  upgr4cycl4dv4e  39926  usgra2pthspth  39938  usgra2pthlem1  39940  usgra2pth  39941  uhgun  39965  resmgmhm  40071  elbigolo1  40641
  Copyright terms: Public domain W3C validator