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

Theorem fveq1 5540
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 4041 . . 3  |-  ( F  =  G  ->  ( A F x  <->  A G x ) )
21iotabidv 5256 . 2  |-  ( F  =  G  ->  ( iota x A F x )  =  ( iota
x A G x ) )
3 df-fv 5279 . 2  |-  ( F `
 A )  =  ( iota x A F x )
4 df-fv 5279 . 2  |-  ( G `
 A )  =  ( iota x A G x )
52, 3, 43eqtr4g 2353 1  |-  ( F  =  G  ->  ( F `  A )  =  ( G `  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   class class class wbr 4039   iotacio 5233   ` cfv 5271
This theorem is referenced by:  fveq1i  5542  fveq1d  5543  fvmptdf  5627  fvmptdv2  5629  isoeq1  5832  oveq  5880  offval  6101  ofrfval  6102  offval3  6107  smoeq  6383  recseq  6405  tfrlem3  6409  tfrlem3a  6410  tfrlem12  6421  tz7.44-2  6436  tz7.44-3  6437  rdgeq1  6440  mapsncnv  6830  elixp2  6836  resixpfo  6870  elixpsn  6871  mapsnen  6954  mapxpen  7043  ac6sfi  7117  ordtypelem7  7255  wemaplem1  7277  ixpiunwdom  7321  oemapval  7401  cantnf  7411  wemapwe  7416  cnfcom3clem  7424  infxpenc2lem2  7663  fseqenlem1  7667  dfac8clem  7675  ac5num  7679  acni  7688  acni2  7689  acnlem  7691  dfac4  7765  dfac5lem5  7770  dfac2a  7772  dfac9  7778  dfacacn  7783  dfac12lem1  7785  dfac12r  7788  cofsmo  7911  cfsmolem  7912  cfsmo  7913  cfcoflem  7914  coftr  7915  alephsing  7918  isfin3ds  7971  fin23lem17  7980  fin23lem32  7986  fin23lem39  7992  isf33lem  8008  isf34lem6  8022  axcc2lem  8078  axcc3  8080  axdc2lem  8090  axdc3lem2  8093  axdc3lem3  8094  axdc3  8096  axdc4lem  8097  axcclem  8099  ac6num  8122  axdclem2  8163  konigthlem  8206  inar1  8413  axdc4uzlem  11060  seqeq3  11067  seqof  11119  ccatfval  11444  clim  11984  rlim  11985  ello1  12005  elo1  12016  summo  12206  fsum  12209  vdwlem6  13049  vdwlem8  13051  ramcl  13092  strfvnd  13179  prdsplusgval  13388  prdsmulrval  13390  prdsleval  13392  prdsdsval  13393  prdsvscaval  13394  xpsff1o  13486  isacs2  13571  isnat  13837  yonedalem3b  14069  yonedainv  14071  ismhm  14433  prdspjmhm  14459  isgrpinv  14548  pwsmulg  14625  isghm  14699  cayleylem2  14804  efgsdm  15055  efgredlemd  15069  efgredlem  15072  efgred  15073  efgrelexlema  15074  efgrelexlemb  15075  prdsgsum  15245  isabv  15600  islmhm  15800  psrmulfval  16146  evlslem2  16265  coe1fval  16302  coe1mul2lem2  16361  coe1tm  16365  frgpcyg  16543  iscnp  16983  1stcfb  17187  ptpjpre1  17282  elpt  17283  elptr  17284  ptpjopn  17322  dfac14  17328  upxp  17333  pthaus  17348  ptrescn  17349  xkoptsub  17364  cnmptkp  17390  xkofvcn  17394  cnmptk1p  17395  cnmptk2  17396  ptunhmeo  17515  ptcmplem3  17764  ptcmplem4  17765  symgtgp  17800  prdstmdd  17822  imasdsf1olem  17953  prdsxmslem2  18091  nmoval  18240  elcncf  18409  ishtpy  18486  pcoval  18525  om1elbas  18546  elpi1i  18560  iscau  18718  mbfi1fseqlem6  19091  mbfi1flimlem  19093  isibl  19136  evlslem3  19414  evlslem1  19415  mpfrcl  19418  deg1ldg  19494  deg1leb  19497  elply2  19594  elplyr  19599  ne0p  19605  coeeu  19623  coelem  19624  coeeq  19625  coeidlem  19635  elqaalem3  19717  qaa  19719  iaa  19721  aareccl  19722  aannenlem2  19725  aaliou2  19736  dchrptlem2  20520  dchrpt  20522  dchrsum2  20523  sumdchr2  20525  dchrvmaeq0  20669  rpvmasum2  20677  dchrisum0re  20678  ostth  20804  ex-fv  20846  elghomlem2  21045  isnvlem  21182  islno  21347  nmooval  21357  nmblolbi  21394  isphg  21411  ajmoi  21453  ajval  21456  ubthlem3  21467  htthlem  21513  hcau  21779  hlimi  21783  hosmval  22331  hommval  22332  hodmval  22333  hfsmval  22334  hfmmval  22335  adjmo  22428  nmopval  22452  elcnop  22453  ellnop  22454  elunop  22468  elhmop  22469  nmfnval  22472  elcnfn  22478  ellnfn  22479  adjeu  22485  adjval  22486  eigvecval  22492  eigvalfval  22493  adj1  22529  adjeq  22531  hmopadj2  22537  lnopeq0i  22603  lnopeq  22605  elunop2  22609  lnophm  22615  hmopco  22619  nmbdoplb  22621  nmcoplb  22626  lnopcon  22631  lnfn0  22643  lnfnmul  22644  nmbdfnlb  22646  nmcfnlb  22650  lnfncon  22652  riesz4  22660  riesz1  22661  cnlnadjlem9  22671  cnlnadjeu  22674  cnlnssadj  22676  nmopcoi  22691  bra11  22704  cnvbraval  22706  pjss2coi  22760  pjssdif2i  22770  pjssdif1i  22771  pjclem4  22795  pj3si  22803  pj3cor1i  22805  isst  22809  ishst  22810  stri  22853  hstri  22861  cntnevol  23191  ismeas  23545  isrnmeas  23546  cndprobval  23651  derangenlem  23717  subfacp1lem3  23728  subfacp1lem5  23730  subfacp1lem6  23731  subfacp1  23732  sconpht  23775  cnpcon  23776  txpcon  23778  ptpcon  23779  indispcon  23780  conpcon  23781  cvxpcon  23788  cvmliftmo  23830  cvmliftlem14  23843  cvmliftlem15  23844  cvmliftiota  23847  cvmlift2  23862  cvmliftphtlem  23863  cvmlift3lem2  23866  cvmlift3lem6  23870  cvmlift3lem7  23871  cvmlift3lem9  23873  cvmlift3  23874  iseupa  23896  dfrtrclrec2  24055  rtrclreclem.refl  24056  rtrclreclem.subset  24057  rtrclreclem.min  24059  dfrtrcl2  24060  prodmo  24159  fprod  24164  poseq  24324  soseq  24325  wfrlem1  24327  wfrlem15  24341  frrlem1  24352  sltval  24372  nobndlem6  24422  brbtwn  24599  brbtwn2  24605  colinearalg  24610  axsegconlem1  24617  axsegcon  24627  ax5seglem5  24633  axpasch  24641  axlowdim  24661  axeuclidlem  24662  axcontlem1  24664  axcontlem2  24665  axcontlem5  24668  bpolylem  24855  bpolyval  24856  eqfnung2  25221  elixp2b  25257  valpr  25261  repcpwti  25264  cbicp  25269  isoriso2  25316  svli2  25587  istopx  25650  isaddrv  25749  cnegvex2  25763  rnegvex2  25764  isucv  25780  ismulcv  25784  isded  25839  dedi  25840  iscatOLD  25857  cati  25858  isfunb  25938  issrc  25970  propsrc  25971  isntr  25976  islimcat  25979  isgraphmrph2  26027  domcatsetval2  26032  domcatval2  26034  codcatval2  26040  prismorcset3  26041  idcatval2  26047  domidmor2  26052  codidmor2  26054  grphidmor2  26056  rocatval2  26063  cmp2morpcats  26064  isnword  26089  isconc1  26109  isconc2  26110  isconc3  26111  pfsubkl  26150  pgapspf  26155  pgapspf2  26156  isibcg  26294  eqfnun  26490  upixp  26506  fdc  26558  isismty  26628  rrnmval  26655  isrngohom  26699  ismrc  26879  mzpclval  26906  mzpsubst  26929  mzprename  26930  mzpcompact2lem  26932  eldioph  26940  eldioph2  26944  eldioph2b  26945  eldioph3  26948  rexrabdioph  26978  2rexfrabdioph  26980  3rexfrabdioph  26981  4rexfrabdioph  26982  6rexfrabdioph  26983  7rexfrabdioph  26984  eldioph4i  26998  rabren3dioph  27001  mzpcong  27162  jm2.27dlem1  27205  wepwsolem  27241  aomclem6  27259  aomclem8  27262  dfac11  27263  dsmmelbas  27308  uvcf1  27344  enfixsn  27360  islindf  27385  islindf4  27411  dgraalem  27453  dgraaub  27456  dgraa0p  27457  mpaaeu  27458  mpaalem  27460  aaitgo  27470  rngunsnply  27481  psgnunilem2  27521  psgnunilem3  27522  dvconstbi  27654  addrval  27774  subrval  27775  mulvval  27776  fnchoice  27803  refsum2cnlem1  27811  fmulcl  27814  fmuldfeqlem1  27815  stoweidlem2  27854  stoweidlem6  27858  stoweidlem8  27860  stoweidlem9  27861  stoweidlem15  27867  stoweidlem16  27868  stoweidlem17  27869  stoweidlem18  27870  stoweidlem21  27873  stoweidlem27  27879  stoweidlem31  27883  stoweidlem36  27888  stoweidlem37  27889  stoweidlem41  27893  stoweidlem43  27895  stoweidlem44  27896  stoweidlem45  27897  stoweidlem46  27898  stoweidlem48  27900  stoweidlem51  27903  stoweidlem55  27907  stoweidlem59  27911  stoweidlem60  27912  stoweidlem62  27914  wlks  28328  iswlk  28329  iswlkon  28332  istrl  28336  trlonprop  28341  iscrct  28369  iscycl  28370  constr3cyclpe  28409  bnj66  29208  bnj106  29216  bnj125  29220  bnj154  29226  bnj155  29227  bnj526  29236  bnj540  29240  bnj609  29265  bnj611  29266  bnj893  29276  bnj1000  29289  bnj1014  29308  bnj1015  29309  bnj1234  29359  bnj1463  29401  islfl  29872  isopos  29992  islaut  30894  ispautN  30910  isldil  30921  isltrn  30930  ltrnid  30946  ltrneq2  30959  isdilN  30965  istrnN  30968  trlval  30973  ltrneq3  31019  cdleme50ex  31370  cdleme  31371  cdlemg1a  31381  ltrniotaval  31392  ltrniotavalbN  31395  cdlemeiota  31396  cdlemg2jlemOLDN  31404  cdlemg2fvlem  31405  cdlemg2klem  31406  istendo  31571  tendoplcbv  31586  tendopl  31587  tendoicbv  31604  tendoi  31605  tendoid0  31636  tendo1ne0  31639  cdlemksv2  31658  cdlemkuv2  31678  cdlemk33N  31720  cdlemk34  31721  cdlemk36  31724  cdlemk19u  31781  cdlemk  31785  tendoex  31786  dvavsca  31828  dvhvscacbv  31910  dvhvscaval  31911  dicopelval  31989  dicelval1sta  31999  diclspsn  32006  dihmeetlem13N  32131  dih1dimatlem0  32140  dih1dimatlem  32141  dihpN  32148  islpolN  32295  hdmap1fval  32609  hdmapfval  32642
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279
  Copyright terms: Public domain W3C validator