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

Theorem fveq1 5686
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 4174 . . 3  |-  ( F  =  G  ->  ( A F x  <->  A G x ) )
21iotabidv 5398 . 2  |-  ( F  =  G  ->  ( iota x A F x )  =  ( iota
x A G x ) )
3 df-fv 5421 . 2  |-  ( F `
 A )  =  ( iota x A F x )
4 df-fv 5421 . 2  |-  ( G `
 A )  =  ( iota x A G x )
52, 3, 43eqtr4g 2461 1  |-  ( F  =  G  ->  ( F `  A )  =  ( G `  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   class class class wbr 4172   iotacio 5375   ` cfv 5413
This theorem is referenced by:  fveq1i  5688  fveq1d  5689  fvmptdf  5775  fvmptdv2  5777  isoeq1  5998  oveq  6046  offval  6271  ofrfval  6272  offval3  6277  bropopvvv  6385  smoeq  6571  recseq  6593  tfrlem3  6597  tfrlem3a  6598  tfrlem12  6609  tz7.44-2  6624  tz7.44-3  6625  rdgeq1  6628  mapsncnv  7019  elixp2  7025  resixpfo  7059  elixpsn  7060  mapsnen  7143  mapxpen  7232  ac6sfi  7310  ordtypelem7  7449  wemaplem1  7471  ixpiunwdom  7515  oemapval  7595  cantnf  7605  wemapwe  7610  cnfcom3clem  7618  infxpenc2lem2  7857  fseqenlem1  7861  dfac8clem  7869  ac5num  7873  acni  7882  acni2  7883  acnlem  7885  dfac4  7959  dfac5lem5  7964  dfac2a  7966  dfac9  7972  dfacacn  7977  dfac12lem1  7979  dfac12r  7982  cofsmo  8105  cfsmolem  8106  cfsmo  8107  cfcoflem  8108  coftr  8109  alephsing  8112  isfin3ds  8165  fin23lem17  8174  fin23lem32  8180  fin23lem39  8186  isf33lem  8202  isf34lem6  8216  axcc2lem  8272  axcc3  8274  axdc2lem  8284  axdc3lem2  8287  axdc3lem3  8288  axdc3  8290  axdc4lem  8291  axcclem  8293  ac6num  8315  axdclem2  8356  konigthlem  8399  inar1  8606  1fv  11075  axdc4uzlem  11276  seqeq3  11283  seqof  11335  ccatfval  11697  clim  12243  rlim  12244  ello1  12264  elo1  12275  summo  12466  fsum  12469  vdwlem6  13309  vdwlem8  13311  ramcl  13352  strfvnd  13439  prdsplusgval  13650  prdsmulrval  13652  prdsleval  13654  prdsdsval  13655  prdsvscaval  13656  xpsff1o  13748  isacs2  13833  isnat  14099  yonedalem3b  14331  yonedainv  14333  ismhm  14695  prdspjmhm  14721  isgrpinv  14810  pwsmulg  14887  isghm  14961  cayleylem2  15066  efgsdm  15317  efgredlemd  15331  efgredlem  15334  efgred  15335  efgrelexlema  15336  efgrelexlemb  15337  prdsgsum  15507  isabv  15862  islmhm  16058  psrmulfval  16404  evlslem2  16523  coe1fval  16558  coe1mul2lem2  16616  coe1tm  16620  frgpcyg  16809  iscnp  17255  1stcfb  17461  ptpjpre1  17556  elpt  17557  elptr  17558  ptpjopn  17597  dfac14  17603  upxp  17608  pthaus  17623  ptrescn  17624  xkoptsub  17639  cnmptkp  17665  xkofvcn  17669  cnmptk1p  17670  cnmptk2  17671  ptunhmeo  17793  ptcmplem3  18038  ptcmplem4  18039  symgtgp  18084  prdstmdd  18106  isucn  18261  imasdsf1olem  18356  prdsxmslem2  18512  nmoval  18702  elcncf  18872  ishtpy  18950  pcoval  18989  om1elbas  19010  elpi1i  19024  iscau  19182  mbfi1fseqlem6  19565  mbfi1flimlem  19567  isibl  19610  evlslem3  19888  evlslem1  19889  mpfrcl  19892  deg1ldg  19968  deg1leb  19971  elply2  20068  elplyr  20073  ne0p  20079  coeeu  20097  coelem  20098  coeeq  20099  coeidlem  20109  elqaalem3  20191  qaa  20193  iaa  20195  aareccl  20196  aannenlem2  20199  aaliou2  20210  dchrptlem2  21002  dchrpt  21004  dchrsum2  21005  sumdchr2  21007  dchrvmaeq0  21151  rpvmasum2  21159  dchrisum0re  21160  ostth  21286  wlks  21479  iswlk  21480  iswlkon  21484  istrl  21490  constr1trl  21541  2wlklem1  21550  iscrct  21564  iscycl  21565  constr3cyclpe  21603  iseupa  21640  ex-fv  21704  elghomlem2  21903  isnvlem  22042  islno  22207  nmooval  22217  nmblolbi  22254  isphg  22271  ajmoi  22313  ajval  22316  ubthlem3  22327  htthlem  22373  hcau  22639  hlimi  22643  hosmval  23191  hommval  23192  hodmval  23193  hfsmval  23194  hfmmval  23195  adjmo  23288  nmopval  23312  elcnop  23313  ellnop  23314  elunop  23328  elhmop  23329  nmfnval  23332  elcnfn  23338  ellnfn  23339  adjeu  23345  adjval  23346  eigvecval  23352  eigvalfval  23353  adj1  23389  adjeq  23391  hmopadj2  23397  lnopeq0i  23463  lnopeq  23465  elunop2  23469  lnophm  23475  hmopco  23479  nmbdoplb  23481  nmcoplb  23486  lnopcon  23491  lnfn0  23503  lnfnmul  23504  nmbdfnlb  23506  nmcfnlb  23510  lnfncon  23512  riesz4  23520  riesz1  23521  cnlnadjlem9  23531  cnlnadjeu  23534  cnlnssadj  23536  nmopcoi  23551  bra11  23564  cnvbraval  23566  pjss2coi  23620  pjssdif2i  23630  pjssdif1i  23631  pjclem4  23655  pj3si  23663  pj3cor1i  23665  isst  23669  ishst  23670  stri  23713  hstri  23721  ismeas  24506  isrnmeas  24507  cntnevol  24535  sitgval  24600  cndprobval  24644  derangenlem  24810  subfacp1lem3  24821  subfacp1lem5  24823  subfacp1lem6  24824  subfacp1  24825  sconpht  24869  cnpcon  24870  txpcon  24872  ptpcon  24873  indispcon  24874  conpcon  24875  cvxpcon  24882  cvmliftmo  24924  cvmliftlem14  24937  cvmliftlem15  24938  cvmliftiota  24941  cvmlift2  24956  cvmliftphtlem  24957  cvmlift3lem2  24960  cvmlift3lem6  24964  cvmlift3lem7  24965  cvmlift3lem9  24967  cvmlift3  24968  dfrtrclrec2  25096  rtrclreclem.refl  25097  rtrclreclem.subset  25098  rtrclreclem.min  25100  dfrtrcl2  25101  shftvalg  25161  prodmo  25215  fprod  25220  poseq  25467  soseq  25468  wfrlem1  25470  wfrlem15  25484  frrlem1  25495  sltval  25515  nobndlem6  25565  brbtwn  25742  brbtwn2  25748  colinearalg  25753  axsegconlem1  25760  axsegcon  25770  ax5seglem5  25776  axpasch  25784  axlowdim  25804  axeuclidlem  25805  axcontlem1  25807  axcontlem2  25808  axcontlem5  25811  bpolylem  25998  bpolyval  25999  voliunnfl  26149  volsupnfl  26150  itg2addnclem  26155  itg2addnclem3  26157  itg2addnc  26158  eqfnun  26313  upixp  26321  fdc  26339  isismty  26400  rrnmval  26427  isrngohom  26471  ismrc  26645  mzpclval  26672  mzpsubst  26695  mzprename  26696  mzpcompact2lem  26698  eldioph  26706  eldioph2  26710  eldioph2b  26711  eldioph3  26714  rexrabdioph  26744  2rexfrabdioph  26746  3rexfrabdioph  26747  4rexfrabdioph  26748  6rexfrabdioph  26749  7rexfrabdioph  26750  eldioph4i  26763  rabren3dioph  26766  mzpcong  26927  jm2.27dlem1  26970  wepwsolem  27006  aomclem6  27024  aomclem8  27027  dfac11  27028  dsmmelbas  27073  uvcf1  27109  enfixsn  27125  islindf  27150  islindf4  27176  dgraalem  27218  dgraaub  27221  dgraa0p  27222  mpaaeu  27223  mpaalem  27225  aaitgo  27235  rngunsnply  27246  psgnunilem2  27286  psgnunilem3  27287  dvconstbi  27419  addrval  27538  subrval  27539  mulvval  27540  fnchoice  27567  refsum2cnlem1  27575  fmulcl  27578  fmuldfeqlem1  27579  stoweidlem2  27618  stoweidlem6  27622  stoweidlem8  27624  stoweidlem9  27625  stoweidlem15  27631  stoweidlem16  27632  stoweidlem17  27633  stoweidlem18  27634  stoweidlem21  27637  stoweidlem27  27643  stoweidlem31  27647  stoweidlem36  27652  stoweidlem37  27653  stoweidlem41  27657  stoweidlem43  27659  stoweidlem44  27660  stoweidlem45  27661  stoweidlem46  27662  stoweidlem48  27664  stoweidlem51  27667  stoweidlem55  27671  stoweidlem59  27675  stoweidlem60  27676  stoweidlem62  27678  usg2wlk  28049  bnj66  28937  bnj106  28945  bnj125  28949  bnj154  28955  bnj155  28956  bnj526  28965  bnj540  28969  bnj609  28994  bnj611  28995  bnj893  29005  bnj1000  29018  bnj1014  29037  bnj1015  29038  bnj1234  29088  bnj1463  29130  islfl  29543  isopos  29663  islaut  30565  ispautN  30581  isldil  30592  isltrn  30601  ltrnid  30617  ltrneq2  30630  isdilN  30636  istrnN  30639  trlval  30644  ltrneq3  30690  cdleme50ex  31041  cdleme  31042  cdlemg1a  31052  ltrniotaval  31063  ltrniotavalbN  31066  cdlemeiota  31067  cdlemg2jlemOLDN  31075  cdlemg2fvlem  31076  cdlemg2klem  31077  istendo  31242  tendoplcbv  31257  tendopl  31258  tendoicbv  31275  tendoi  31276  tendoid0  31307  tendo1ne0  31310  cdlemksv2  31329  cdlemkuv2  31349  cdlemk33N  31391  cdlemk34  31392  cdlemk36  31395  cdlemk19u  31452  cdlemk  31456  tendoex  31457  dvavsca  31499  dvhvscacbv  31581  dvhvscaval  31582  dicopelval  31660  dicelval1sta  31670  diclspsn  31677  dihmeetlem13N  31802  dih1dimatlem0  31811  dih1dimatlem  31812  dihpN  31819  islpolN  31966  hdmap1fval  32280  hdmapfval  32313
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421
  Copyright terms: Public domain W3C validator