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

Theorem fveq1 5524
Description: Equality theorem for function value. (Contributed by NM, 29-Dec-1996.)
Assertion
Ref Expression
fveq1  |-  ( F  =  G  ->  ( F `  A )  =  ( G `  A ) )

Proof of Theorem fveq1
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 breq 4025 . . 3  |-  ( F  =  G  ->  ( A F x  <->  A G x ) )
21iotabidv 5240 . 2  |-  ( F  =  G  ->  ( iota x A F x )  =  ( iota
x A G x ) )
3 df-fv 5263 . 2  |-  ( F `
 A )  =  ( iota x A F x )
4 df-fv 5263 . 2  |-  ( G `
 A )  =  ( iota x A G x )
52, 3, 43eqtr4g 2340 1  |-  ( F  =  G  ->  ( F `  A )  =  ( G `  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   class class class wbr 4023   iotacio 5217   ` cfv 5255
This theorem is referenced by:  fveq1i  5526  fveq1d  5527  fvmptdf  5611  fvmptdv2  5613  isoeq1  5816  oveq  5864  offval  6085  ofrfval  6086  offval3  6091  smoeq  6367  recseq  6389  tfrlem3  6393  tfrlem3a  6394  tfrlem12  6405  tz7.44-2  6420  tz7.44-3  6421  rdgeq1  6424  mapsncnv  6814  elixp2  6820  resixpfo  6854  elixpsn  6855  mapsnen  6938  mapxpen  7027  ac6sfi  7101  ordtypelem7  7239  wemaplem1  7261  ixpiunwdom  7305  oemapval  7385  cantnf  7395  wemapwe  7400  cnfcom3clem  7408  infxpenc2lem2  7647  fseqenlem1  7651  dfac8clem  7659  ac5num  7663  acni  7672  acni2  7673  acnlem  7675  dfac4  7749  dfac5lem5  7754  dfac2a  7756  dfac9  7762  dfacacn  7767  dfac12lem1  7769  dfac12r  7772  cofsmo  7895  cfsmolem  7896  cfsmo  7897  cfcoflem  7898  coftr  7899  alephsing  7902  isfin3ds  7955  fin23lem17  7964  fin23lem32  7970  fin23lem39  7976  isf33lem  7992  isf34lem6  8006  axcc2lem  8062  axcc3  8064  axdc2lem  8074  axdc3lem2  8077  axdc3lem3  8078  axdc3  8080  axdc4lem  8081  axcclem  8083  ac6num  8106  axdclem2  8147  konigthlem  8190  inar1  8397  axdc4uzlem  11044  seqeq3  11051  seqof  11103  ccatfval  11428  clim  11968  rlim  11969  ello1  11989  elo1  12000  summo  12190  fsum  12193  vdwlem6  13033  vdwlem8  13035  ramcl  13076  strfvnd  13163  prdsplusgval  13372  prdsmulrval  13374  prdsleval  13376  prdsdsval  13377  prdsvscaval  13378  xpsff1o  13470  isacs2  13555  isnat  13821  yonedalem3b  14053  yonedainv  14055  ismhm  14417  prdspjmhm  14443  isgrpinv  14532  pwsmulg  14609  isghm  14683  cayleylem2  14788  efgsdm  15039  efgredlemd  15053  efgredlem  15056  efgred  15057  efgrelexlema  15058  efgrelexlemb  15059  prdsgsum  15229  isabv  15584  islmhm  15784  psrmulfval  16130  evlslem2  16249  coe1fval  16286  coe1mul2lem2  16345  coe1tm  16349  frgpcyg  16527  iscnp  16967  1stcfb  17171  ptpjpre1  17266  elpt  17267  elptr  17268  ptpjopn  17306  dfac14  17312  upxp  17317  pthaus  17332  ptrescn  17333  xkoptsub  17348  cnmptkp  17374  xkofvcn  17378  cnmptk1p  17379  cnmptk2  17380  ptunhmeo  17499  ptcmplem3  17748  ptcmplem4  17749  symgtgp  17784  prdstmdd  17806  imasdsf1olem  17937  prdsxmslem2  18075  nmoval  18224  elcncf  18393  ishtpy  18470  pcoval  18509  om1elbas  18530  elpi1i  18544  iscau  18702  mbfi1fseqlem6  19075  mbfi1flimlem  19077  isibl  19120  evlslem3  19398  evlslem1  19399  mpfrcl  19402  deg1ldg  19478  deg1leb  19481  elply2  19578  elplyr  19583  ne0p  19589  coeeu  19607  coelem  19608  coeeq  19609  coeidlem  19619  elqaalem3  19701  qaa  19703  iaa  19705  aareccl  19706  aannenlem2  19709  aaliou2  19720  dchrptlem2  20504  dchrpt  20506  dchrsum2  20507  sumdchr2  20509  dchrvmaeq0  20653  rpvmasum2  20661  dchrisum0re  20662  ostth  20788  ex-fv  20830  elghomlem2  21029  isnvlem  21166  islno  21331  nmooval  21341  nmblolbi  21378  isphg  21395  ajmoi  21437  ajval  21440  ubthlem3  21451  htthlem  21497  hcau  21763  hlimi  21767  hosmval  22315  hommval  22316  hodmval  22317  hfsmval  22318  hfmmval  22319  adjmo  22412  nmopval  22436  elcnop  22437  ellnop  22438  elunop  22452  elhmop  22453  nmfnval  22456  elcnfn  22462  ellnfn  22463  adjeu  22469  adjval  22470  eigvecval  22476  eigvalfval  22477  adj1  22513  adjeq  22515  hmopadj2  22521  lnopeq0i  22587  lnopeq  22589  elunop2  22593  lnophm  22599  hmopco  22603  nmbdoplb  22605  nmcoplb  22610  lnopcon  22615  lnfn0  22627  lnfnmul  22628  nmbdfnlb  22630  nmcfnlb  22634  lnfncon  22636  riesz4  22644  riesz1  22645  cnlnadjlem9  22655  cnlnadjeu  22658  cnlnssadj  22660  nmopcoi  22675  bra11  22688  cnvbraval  22690  pjss2coi  22744  pjssdif2i  22754  pjssdif1i  22755  pjclem4  22779  pj3si  22787  pj3cor1i  22789  isst  22793  ishst  22794  stri  22837  hstri  22845  cntnevol  23175  ismeas  23530  isrnmeas  23531  cndprobval  23636  derangenlem  23702  subfacp1lem3  23713  subfacp1lem5  23715  subfacp1lem6  23716  subfacp1  23717  sconpht  23760  cnpcon  23761  txpcon  23763  ptpcon  23764  indispcon  23765  conpcon  23766  cvxpcon  23773  cvmliftmo  23815  cvmliftlem14  23828  cvmliftlem15  23829  cvmliftiota  23832  cvmlift2  23847  cvmliftphtlem  23848  cvmlift3lem2  23851  cvmlift3lem6  23855  cvmlift3lem7  23856  cvmlift3lem9  23858  cvmlift3  23859  iseupa  23881  dfrtrclrec2  24040  rtrclreclem.refl  24041  rtrclreclem.subset  24042  rtrclreclem.min  24044  dfrtrcl2  24045  poseq  24253  soseq  24254  wfrlem1  24256  wfrlem15  24270  frrlem1  24281  sltval  24301  nobndlem6  24351  brbtwn  24527  brbtwn2  24533  colinearalg  24538  axsegconlem1  24545  axsegcon  24555  ax5seglem5  24561  axpasch  24569  axlowdim  24589  axeuclidlem  24590  axcontlem1  24592  axcontlem2  24593  axcontlem5  24596  bpolylem  24783  bpolyval  24784  eqfnung2  25118  elixp2b  25154  valpr  25158  repcpwti  25161  cbicp  25166  isoriso2  25213  svli2  25484  istopx  25547  isaddrv  25646  cnegvex2  25660  rnegvex2  25661  isucv  25677  ismulcv  25681  isded  25736  dedi  25737  iscatOLD  25754  cati  25755  isfunb  25835  issrc  25867  propsrc  25868  isntr  25873  islimcat  25876  isgraphmrph2  25924  domcatsetval2  25929  domcatval2  25931  codcatval2  25937  prismorcset3  25938  idcatval2  25944  domidmor2  25949  codidmor2  25951  grphidmor2  25953  rocatval2  25960  cmp2morpcats  25961  isnword  25986  isconc1  26006  isconc2  26007  isconc3  26008  pfsubkl  26047  pgapspf  26052  pgapspf2  26053  isibcg  26191  eqfnun  26387  upixp  26403  fdc  26455  isismty  26525  rrnmval  26552  isrngohom  26596  ismrc  26776  mzpclval  26803  mzpsubst  26826  mzprename  26827  mzpcompact2lem  26829  eldioph  26837  eldioph2  26841  eldioph2b  26842  eldioph3  26845  rexrabdioph  26875  2rexfrabdioph  26877  3rexfrabdioph  26878  4rexfrabdioph  26879  6rexfrabdioph  26880  7rexfrabdioph  26881  eldioph4i  26895  rabren3dioph  26898  mzpcong  27059  jm2.27dlem1  27102  wepwsolem  27138  aomclem6  27156  aomclem8  27159  dfac11  27160  dsmmelbas  27205  uvcf1  27241  enfixsn  27257  islindf  27282  islindf4  27308  dgraalem  27350  dgraaub  27353  dgraa0p  27354  mpaaeu  27355  mpaalem  27357  aaitgo  27367  rngunsnply  27378  psgnunilem2  27418  psgnunilem3  27419  dvconstbi  27551  addrval  27671  subrval  27672  mulvval  27673  fnchoice  27700  refsum2cnlem1  27708  fmulcl  27711  fmuldfeqlem1  27712  stoweidlem2  27751  stoweidlem6  27755  stoweidlem8  27757  stoweidlem9  27758  stoweidlem15  27764  stoweidlem16  27765  stoweidlem17  27766  stoweidlem18  27767  stoweidlem21  27770  stoweidlem27  27776  stoweidlem31  27780  stoweidlem36  27785  stoweidlem37  27786  stoweidlem41  27790  stoweidlem43  27792  stoweidlem44  27793  stoweidlem45  27794  stoweidlem46  27795  stoweidlem48  27797  stoweidlem51  27800  stoweidlem55  27804  stoweidlem59  27808  stoweidlem60  27809  stoweidlem62  27811  bnj66  28892  bnj106  28900  bnj125  28904  bnj154  28910  bnj155  28911  bnj526  28920  bnj540  28924  bnj609  28949  bnj611  28950  bnj893  28960  bnj1000  28973  bnj1014  28992  bnj1015  28993  bnj1234  29043  bnj1463  29085  islfl  29250  isopos  29370  islaut  30272  ispautN  30288  isldil  30299  isltrn  30308  ltrnid  30324  ltrneq2  30337  isdilN  30343  istrnN  30346  trlval  30351  ltrneq3  30397  cdleme50ex  30748  cdleme  30749  cdlemg1a  30759  ltrniotaval  30770  ltrniotavalbN  30773  cdlemeiota  30774  cdlemg2jlemOLDN  30782  cdlemg2fvlem  30783  cdlemg2klem  30784  istendo  30949  tendoplcbv  30964  tendopl  30965  tendoicbv  30982  tendoi  30983  tendoid0  31014  tendo1ne0  31017  cdlemksv2  31036  cdlemkuv2  31056  cdlemk33N  31098  cdlemk34  31099  cdlemk36  31102  cdlemk19u  31159  cdlemk  31163  tendoex  31164  dvavsca  31206  dvhvscacbv  31288  dvhvscaval  31289  dicopelval  31367  dicelval1sta  31377  diclspsn  31384  dihmeetlem13N  31509  dih1dimatlem0  31518  dih1dimatlem  31519  dihpN  31526  islpolN  31673  hdmap1fval  31987  hdmapfval  32020
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263
  Copyright terms: Public domain W3C validator