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

Theorem fveq1 5718
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 4206 . . 3  |-  ( F  =  G  ->  ( A F x  <->  A G x ) )
21iotabidv 5430 . 2  |-  ( F  =  G  ->  ( iota x A F x )  =  ( iota
x A G x ) )
3 df-fv 5453 . 2  |-  ( F `
 A )  =  ( iota x A F x )
4 df-fv 5453 . 2  |-  ( G `
 A )  =  ( iota x A G x )
52, 3, 43eqtr4g 2492 1  |-  ( F  =  G  ->  ( F `  A )  =  ( G `  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   class class class wbr 4204   iotacio 5407   ` cfv 5445
This theorem is referenced by:  fveq1i  5720  fveq1d  5721  fvmptdf  5807  fvmptdv2  5809  isoeq1  6030  oveq  6078  offval  6303  ofrfval  6304  offval3  6309  bropopvvv  6417  smoeq  6603  recseq  6625  tfrlem3  6629  tfrlem3a  6630  tfrlem12  6641  tz7.44-2  6656  tz7.44-3  6657  rdgeq1  6660  mapsncnv  7051  elixp2  7057  resixpfo  7091  elixpsn  7092  mapsnen  7175  mapxpen  7264  ac6sfi  7342  ordtypelem7  7482  wemaplem1  7504  ixpiunwdom  7548  oemapval  7628  cantnf  7638  wemapwe  7643  cnfcom3clem  7651  infxpenc2lem2  7890  fseqenlem1  7894  dfac8clem  7902  ac5num  7906  acni  7915  acni2  7916  acnlem  7918  dfac4  7992  dfac5lem5  7997  dfac2a  7999  dfac9  8005  dfacacn  8010  dfac12lem1  8012  dfac12r  8015  cofsmo  8138  cfsmolem  8139  cfsmo  8140  cfcoflem  8141  coftr  8142  alephsing  8145  isfin3ds  8198  fin23lem17  8207  fin23lem32  8213  fin23lem39  8219  isf33lem  8235  isf34lem6  8249  axcc2lem  8305  axcc3  8307  axdc2lem  8317  axdc3lem2  8320  axdc3lem3  8321  axdc3  8323  axdc4lem  8324  axcclem  8326  ac6num  8348  axdclem2  8389  konigthlem  8432  inar1  8639  1fv  11108  axdc4uzlem  11309  seqeq3  11316  seqof  11368  ccatfval  11730  clim  12276  rlim  12277  ello1  12297  elo1  12308  summo  12499  fsum  12502  vdwlem6  13342  vdwlem8  13344  ramcl  13385  strfvnd  13472  prdsplusgval  13683  prdsmulrval  13685  prdsleval  13687  prdsdsval  13688  prdsvscaval  13689  xpsff1o  13781  isacs2  13866  isnat  14132  yonedalem3b  14364  yonedainv  14366  ismhm  14728  prdspjmhm  14754  isgrpinv  14843  pwsmulg  14920  isghm  14994  cayleylem2  15099  efgsdm  15350  efgredlemd  15364  efgredlem  15367  efgred  15368  efgrelexlema  15369  efgrelexlemb  15370  prdsgsum  15540  isabv  15895  islmhm  16091  psrmulfval  16437  evlslem2  16556  coe1fval  16591  coe1mul2lem2  16649  coe1tm  16653  frgpcyg  16842  iscnp  17289  1stcfb  17496  ptpjpre1  17591  elpt  17592  elptr  17593  ptpjopn  17632  dfac14  17638  upxp  17643  pthaus  17658  ptrescn  17659  xkoptsub  17674  cnmptkp  17700  xkofvcn  17704  cnmptk1p  17705  cnmptk2  17706  ptunhmeo  17828  ptcmplem3  18073  ptcmplem4  18074  symgtgp  18119  prdstmdd  18141  isucn  18296  imasdsf1olem  18391  prdsxmslem2  18547  nmoval  18737  elcncf  18907  ishtpy  18985  pcoval  19024  om1elbas  19045  elpi1i  19059  iscau  19217  mbfi1fseqlem6  19600  mbfi1flimlem  19602  isibl  19645  evlslem3  19923  evlslem1  19924  mpfrcl  19927  deg1ldg  20003  deg1leb  20006  elply2  20103  elplyr  20108  ne0p  20114  coeeu  20132  coelem  20133  coeeq  20134  coeidlem  20144  elqaalem3  20226  qaa  20228  iaa  20230  aareccl  20231  aannenlem2  20234  aaliou2  20245  dchrptlem2  21037  dchrpt  21039  dchrsum2  21040  sumdchr2  21042  dchrvmaeq0  21186  rpvmasum2  21194  dchrisum0re  21195  ostth  21321  wlks  21514  iswlk  21515  iswlkon  21519  istrl  21525  constr1trl  21576  2wlklem1  21585  iscrct  21599  iscycl  21600  constr3cyclpe  21638  iseupa  21675  ex-fv  21739  elghomlem2  21938  isnvlem  22077  islno  22242  nmooval  22252  nmblolbi  22289  isphg  22306  ajmoi  22348  ajval  22351  ubthlem3  22362  htthlem  22408  hcau  22674  hlimi  22678  hosmval  23226  hommval  23227  hodmval  23228  hfsmval  23229  hfmmval  23230  adjmo  23323  nmopval  23347  elcnop  23348  ellnop  23349  elunop  23363  elhmop  23364  nmfnval  23367  elcnfn  23373  ellnfn  23374  adjeu  23380  adjval  23381  eigvecval  23387  eigvalfval  23388  adj1  23424  adjeq  23426  hmopadj2  23432  lnopeq0i  23498  lnopeq  23500  elunop2  23504  lnophm  23510  hmopco  23514  nmbdoplb  23516  nmcoplb  23521  lnopcon  23526  lnfn0  23538  lnfnmul  23539  nmbdfnlb  23541  nmcfnlb  23545  lnfncon  23547  riesz4  23555  riesz1  23556  cnlnadjlem9  23566  cnlnadjeu  23569  cnlnssadj  23571  nmopcoi  23586  bra11  23599  cnvbraval  23601  pjss2coi  23655  pjssdif2i  23665  pjssdif1i  23666  pjclem4  23690  pj3si  23698  pj3cor1i  23700  isst  23704  ishst  23705  stri  23748  hstri  23756  ismeas  24541  isrnmeas  24542  cntnevol  24570  sitgval  24635  cndprobval  24679  derangenlem  24845  subfacp1lem3  24856  subfacp1lem5  24858  subfacp1lem6  24859  subfacp1  24860  sconpht  24904  cnpcon  24905  txpcon  24907  ptpcon  24908  indispcon  24909  conpcon  24910  cvxpcon  24917  cvmliftmo  24959  cvmliftlem14  24972  cvmliftlem15  24973  cvmliftiota  24976  cvmlift2  24991  cvmliftphtlem  24992  cvmlift3lem2  24995  cvmlift3lem6  24999  cvmlift3lem7  25000  cvmlift3lem9  25002  cvmlift3  25003  dfrtrclrec2  25131  rtrclreclem.refl  25132  rtrclreclem.subset  25133  rtrclreclem.min  25135  dfrtrcl2  25136  shftvalg  25196  prodmo  25251  fprod  25256  poseq  25508  soseq  25509  wfrlem1  25511  wfrlem15  25525  frrlem1  25536  sltval  25556  nobndlem6  25606  brbtwn  25786  brbtwn2  25792  colinearalg  25797  axsegconlem1  25804  axsegcon  25814  ax5seglem5  25820  axpasch  25828  axlowdim  25848  axeuclidlem  25849  axcontlem1  25851  axcontlem2  25852  axcontlem5  25855  bpolylem  26042  bpolyval  26043  voliunnfl  26196  volsupnfl  26197  itg2addnclem  26202  itg2addnclem3  26204  itg2addnc  26205  eqfnun  26360  upixp  26368  fdc  26386  isismty  26447  rrnmval  26474  isrngohom  26518  ismrc  26692  mzpclval  26719  mzpsubst  26742  mzprename  26743  mzpcompact2lem  26745  eldioph  26753  eldioph2  26757  eldioph2b  26758  eldioph3  26761  rexrabdioph  26791  2rexfrabdioph  26793  3rexfrabdioph  26794  4rexfrabdioph  26795  6rexfrabdioph  26796  7rexfrabdioph  26797  eldioph4i  26810  rabren3dioph  26813  mzpcong  26974  jm2.27dlem1  27017  wepwsolem  27053  aomclem6  27071  aomclem8  27074  dfac11  27075  dsmmelbas  27120  uvcf1  27156  enfixsn  27172  islindf  27197  islindf4  27223  dgraalem  27265  dgraaub  27268  dgraa0p  27269  mpaaeu  27270  mpaalem  27272  aaitgo  27282  rngunsnply  27293  psgnunilem2  27333  psgnunilem3  27334  dvconstbi  27466  addrval  27585  subrval  27586  mulvval  27587  fnchoice  27614  refsum2cnlem1  27622  fmulcl  27625  fmuldfeqlem1  27626  stoweidlem2  27665  stoweidlem6  27669  stoweidlem8  27671  stoweidlem9  27672  stoweidlem15  27678  stoweidlem16  27679  stoweidlem17  27680  stoweidlem18  27681  stoweidlem21  27684  stoweidlem27  27690  stoweidlem31  27694  stoweidlem36  27699  stoweidlem37  27700  stoweidlem41  27704  stoweidlem43  27706  stoweidlem44  27707  stoweidlem45  27708  stoweidlem46  27709  stoweidlem48  27711  stoweidlem51  27714  stoweidlem55  27718  stoweidlem59  27722  stoweidlem60  27723  stoweidlem62  27725  shwrdeqrep  28160  usg2wlk  28193  bnj66  29085  bnj106  29093  bnj125  29097  bnj154  29103  bnj155  29104  bnj526  29113  bnj540  29117  bnj609  29142  bnj611  29143  bnj893  29153  bnj1000  29166  bnj1014  29185  bnj1015  29186  bnj1234  29236  bnj1463  29278  islfl  29697  isopos  29817  islaut  30719  ispautN  30735  isldil  30746  isltrn  30755  ltrnid  30771  ltrneq2  30784  isdilN  30790  istrnN  30793  trlval  30798  ltrneq3  30844  cdleme50ex  31195  cdleme  31196  cdlemg1a  31206  ltrniotaval  31217  ltrniotavalbN  31220  cdlemeiota  31221  cdlemg2jlemOLDN  31229  cdlemg2fvlem  31230  cdlemg2klem  31231  istendo  31396  tendoplcbv  31411  tendopl  31412  tendoicbv  31429  tendoi  31430  tendoid0  31461  tendo1ne0  31464  cdlemksv2  31483  cdlemkuv2  31503  cdlemk33N  31545  cdlemk34  31546  cdlemk36  31549  cdlemk19u  31606  cdlemk  31610  tendoex  31611  dvavsca  31653  dvhvscacbv  31735  dvhvscaval  31736  dicopelval  31814  dicelval1sta  31824  diclspsn  31831  dihmeetlem13N  31956  dih1dimatlem0  31965  dih1dimatlem  31966  dihpN  31973  islpolN  32120  hdmap1fval  32434  hdmapfval  32467
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rex 2703  df-uni 4008  df-br 4205  df-iota 5409  df-fv 5453
  Copyright terms: Public domain W3C validator