Theorem fveq2 5640

Description: Equality theorem for function value. (Contributed by NM, 29-Dec-1996.)

Assertion

Ref	Expression
fveq2	|- ( A = B -> ( F ` A ) = ( F ` B ) )

Proof of Theorem fveq2

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq1 4091	. . 3 |- ( A = B -> ( A F x <-> B F x ) )
2	1	iotabidv 5309	. 2 |- ( A = B -> ( iota x A F x ) = ( iota x B F x ) )
3		df-fv 5334	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5334	. 2 |- ( F ` B ) = ( iota x B F x )
5	2, 3, 4	3eqtr4g 2289	1 |- ( A = B -> ( F ` A ) = ( F ` B ) )

Syntax hints:   -> wi 4   = wceq 1397   class class class wbr 4088   iotacio 5284   ` cfv 5326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334

This theorem is referenced by:  fveq2i  5643  fveq2d  5644  2fveq3  5645  fvifdc  5662  dffn5imf  5702  fvelimab  5703  ssimaex  5708  fvco4  5719  fvmptssdm  5732  fvmptf  5740  eqfnfv2f  5749  fvelrn  5779  ralrnmpt  5790  rexrnmpt  5791  ffnfvf  5807  fmptco  5814  cofmpt  5817  fcompt  5818  fcoconst  5819  fsn2g  5823  fnressn  5841  fressnfv  5842  fconstfvm  5873  foco2  5897  funiunfvdmf  5908  f1veqaeq  5913  dff13f  5914  f1fveq  5916  f1elima  5917  f1ocnvfv  5923  f1ocnvfvb  5924  fcofo  5928  cocan2  5932  fliftfun  5940  isorel  5952  isocnv  5955  isotr  5960  f1oiso2  5971  canth  5972  imbrov2fvoveq  6046  ffnov  6128  eqfnov  6131  fnovim  6133  fnrnov  6171  foov  6172  funimassov  6175  ovelimab  6176  suppssfv  6234  ofvalg  6248  ofrval  6249  offval2  6254  ofrfval2  6255  ofco  6257  caofinvl  6264  op1std  6314  op2ndd  6315  1stval2  6321  2ndval2  6322  unielxp  6340  reldm  6352  oprabco  6385  2ndconst  6390  f1o2ndf1  6396  mpoxopn0yelv  6408  mpoxopoveq  6409  smoel  6469  tfrlem1  6477  tfrlem3-2d  6481  tfrlem5  6483  tfrlem9  6488  tfr0dm  6491  tfrlemiubacc  6499  tfrlemi1  6501  tfrexlem  6503  tfr1onlemsucfn  6509  tfr1onlemsucaccv  6510  tfr1onlembxssdm  6512  tfr1onlembfn  6513  tfr1onlemubacc  6515  tfr1onlemaccex  6517  tfr1onlemres  6518  tfri1dALT  6520  tfrcllemsucfn  6522  tfrcllemsucaccv  6523  tfrcllembxssdm  6525  tfrcllembfn  6526  tfrcllemubacc  6528  tfrcllemaccex  6530  tfrcllemres  6531  tfrcldm  6532  tfrcl  6533  tfri3  6536  rdgtfr  6543  rdgss  6552  rdgisuc1  6553  rdgisucinc  6554  rdgon  6555  frecabex  6567  frecabcl  6568  frecfcllem  6573  frecsuclem  6575  frecsuc  6576  frecrdg  6577  oav  6625  omv  6626  oeiv  6627  fvixp  6875  cbvixp  6887  mptelixpg  6906  elixpsn  6907  dom2lem  6948  xpcomco  7013  xpmapen  7039  fidceq  7059  fieq0  7178  ordiso2  7237  djune  7280  updjudhcoinlf  7282  updjudhcoinrg  7283  updjud  7284  omp1eom  7297  0ct  7309  ctmlemr  7310  ctssdclemn0  7312  ctssdccl  7313  ctssdc  7315  enumctlemm  7316  nninfninc  7325  nnnninfeq  7330  nnnninfeq2  7331  enomnilem  7340  finomni  7342  fodjuomnilemdc  7346  fodju0  7349  fodjuomni  7351  ismkvnex  7357  fodjumkv  7362  nninfwlporlemd  7374  nninfwlpor  7376  exmidaclem  7426  cc1  7487  cc2lem  7488  cc2  7489  cc3  7490  mulpipq2  7594  genipv  7732  genpelxp  7734  addcanprleml  7837  addcanprlemu  7838  recexprlemm  7847  recexprlemdisj  7853  recexprlemloc  7854  recexprlem1ssl  7856  recexprlem1ssu  7857  cauappcvgprlemm  7868  cauappcvgprlemdisj  7874  cauappcvgprlemloc  7875  cauappcvgprlemladdru  7879  cauappcvgprlemladdrl  7880  cauappcvgprlem1  7882  cauappcvgprlem2  7883  cauappcvgprlemlim  7884  cauappcvgpr  7885  caucvgprlemnkj  7889  caucvgprlemnbj  7890  caucvgprlemm  7891  caucvgprlemdisj  7897  caucvgprlemloc  7898  caucvgprlemcl  7899  caucvgprlemladdfu  7900  caucvgprlemladdrl  7901  caucvgprlem1  7902  caucvgprlem2  7903  caucvgpr  7905  caucvgprprlemell  7908  caucvgprprlemelu  7909  caucvgprprlemcbv  7910  caucvgprprlemval  7911  caucvgprprlemnkeqj  7913  caucvgprprlemnbj  7916  caucvgprprlemml  7917  caucvgprprlemmu  7918  caucvgprprlemopl  7920  caucvgprprlemlol  7921  caucvgprprlemopu  7922  caucvgprprlemloc  7926  caucvgprprlemclphr  7928  caucvgprprlemexbt  7929  caucvgprprlem1  7932  caucvgprprlem2  7933  caucvgsrlemcl  8012  caucvgsrlemfv  8014  caucvgsrlembound  8017  caucvgsrlemgt1  8018  caucvgsrlemoffval  8019  caucvgsrlemoffres  8023  caucvgsrlembnd  8024  caucvgsr  8025  axcaucvglemcau  8121  axcaucvglemres  8122  uz11  9782  cnref1o  9888  fzprval  10320  fztpval  10321  zsupcllemex  10494  infssuzex  10497  suprzubdc  10500  frec2uzuzd  10668  frec2uzltd  10669  frec2uzlt2d  10670  frecuzrdgrrn  10674  frec2uzrdg  10675  frecuzrdgtcl  10678  frecuzrdgg  10682  frecuzrdgfunlem  10685  frecfzennn  10692  seqeq1  10716  iseqovex  10724  seq3val  10726  seqvalcd  10727  seq3-1  10728  seqf  10730  seq3p1  10731  seqovcd  10733  seqp1cd  10736  seq3clss  10737  seq3fveq2  10741  seqfveq2g  10743  seqfveqg  10744  seq3fveq  10745  seq3feq  10746  seq3shft2  10747  seqshft2g  10748  monoord  10751  monoord2  10752  ser3mono  10753  seq3split  10754  seqsplitg  10755  seq3caopr3  10757  seqcaopr3g  10758  seq3caopr2  10759  seqcaopr2g  10760  iseqf1olemkle  10763  iseqf1olemklt  10764  iseqf1olemqval  10766  iseqf1olemqk  10773  iseqf1olemjpcl  10774  iseqf1olemqpcl  10775  iseqf1olemfvp  10776  seq3f1olemqsumkj  10777  seq3f1olemqsum  10779  seq3f1olemstep  10780  seq3f1olemp  10781  seq3f1oleml  10782  seq3f1o  10783  seqf1oglem2a  10784  seqf1og  10787  seq3id2  10792  seq3homo  10793  seq3z  10794  seqhomog  10796  seqfeq4g  10797  ser3ge0  10802  ser3le  10803  exp3vallem  10806  exp3val  10807  facp1  10996  faccl  11001  facdiv  11004  facwordi  11006  faclbnd  11007  facubnd  11011  bcval  11015  bcval5  11029  fz1eqb  11056  omgadd  11069  hashxp  11094  zfz1isolem1  11108  zfz1iso  11109  seq3coll  11110  eqwrd  11161  lswwrd  11167  lswex  11172  ccatfvalfi  11176  ccatval1  11181  ccatval2  11182  ccatalpha  11197  s1eq  11203  eqs1  11212  swrdval  11236  ccatopth2  11305  wrd2ind  11311  seq3shft  11419  reval  11430  replim  11440  cj11  11486  caucvgre  11562  cvg1nlemcau  11565  cvg1nlemres  11566  rexuz3  11571  absval  11582  resqrexlemover  11591  resqrexlemdecn  11593  resqrexlemlo  11594  resqrexlemcalc3  11597  resqrexlemnm  11599  resqrexlemcvg  11600  resqrexlemoverl  11602  resqrexlemglsq  11603  resqrexlemga  11604  resqrexlemsqa  11605  resqrexlemex  11606  abs00bd  11647  cau3lem  11695  caubnd2  11698  climconst  11871  climmpt  11881  climshftlemg  11883  climcn1  11889  climle  11915  climub  11925  climserle  11926  climcau  11928  climcvg1nlem  11930  climcvg1n  11931  serf0  11933  fsum3cvg  11960  summodclem3  11962  summodclem2a  11963  summodclem2  11964  summodc  11965  zsumdc  11966  fsum3  11969  fsumf1o  11972  fisumss  11974  fsum3cvg2  11976  fsum3ser  11979  fsumcl2lem  11980  fsumadd  11988  sumsnf  11991  isummulc2  12008  isumge0  12012  isumadd  12013  fsum2dlemstep  12016  fsummulc2  12030  fsumconst  12036  fsumrelem  12053  isumshft  12072  isum1p  12074  isumnn0nn  12075  isumrpcl  12076  isumlessdc  12078  cvgratnnlemnexp  12106  cvgratnnlemmn  12107  cvgratnnlemseq  12108  cvgratnnlemabsle  12109  cvgratnnlemfm  12111  cvgratnnlemrate  12112  cvgratnn  12113  cvgratz  12114  mertenslemi1  12117  mertenslem2  12118  mertensabs  12119  clim2prod  12121  prodfap0  12127  prodfrecap  12128  prodfdivap  12129  fproddccvg  12154  prodmodclem3  12157  prodmodclem2a  12158  prodmodclem2  12159  prodmodc  12160  zproddc  12161  fprodseq  12165  fprodf1o  12170  fprodssdc  12172  fprodmul  12173  prodsnf  12174  fprodfac  12197  fprodconst  12202  fprod2dlemstep  12204  eftvalcn  12239  ef0lem  12242  ege2le3  12253  efcj  12255  efaddlem  12256  eftlub  12272  efgt1p2  12277  reef11  12281  tanvalap  12290  efieq1re  12354  eirraplem  12359  dvdsabseq  12429  dvdsfac  12442  gcd0id  12571  nninfctlemfo  12632  nn0seqcvgd  12634  alginv  12640  algcvg  12641  algcvga  12644  algfx  12645  eucalglt  12650  lcmid  12673  qredeu  12690  prmfac1  12745  sqne2sq  12770  qnumdenbi  12785  dfphi2  12813  eulerthlemrprm  12822  eulerthlema  12823  eulerthlemh  12824  eulerthlemth  12825  phisum  12834  pcmpt  12937  pcfac  12944  1arithlem4  12960  elgz  12965  4sqlem4  12986  4sqlem12  12996  2expltfac  13033  ennnfonelemk  13042  ennnfonelemp1  13048  ennnfoneleminc  13053  ennnfonelemkh  13054  ennnfonelemhf1o  13055  ennnfonelemex  13056  ennnfonelemhom  13057  ennnfonelemrn  13061  ennnfonelemnn0  13064  ennnfonelemr  13065  ennnfonelemim  13066  ctinfomlemom  13069  ctinfom  13070  ctiunctlemfo  13081  nninfdclemlt  13093  nninfdclemf1  13094  sloteq  13108  ressvalsets  13168  topnvalg  13355  prdsbasprj  13386  prdsplusgfval  13388  prdsmulrfval  13390  imasex  13409  imasaddvallemg  13419  qusex  13429  xpsfrnel  13448  xpsfeq  13449  xpsval  13456  ismgm  13461  plusffvalg  13466  grpidvalg  13477  gsumfzval  13495  gsumval2  13501  issgrp  13507  ismnddef  13522  prdsidlem  13551  pws0g  13555  ismhm  13565  mhmex  13566  mhmlin  13571  issubm  13576  mhmeql  13596  isgrp  13610  grpn0  13639  grpinvfvalg  13646  grpsubfvalg  13649  grpsubval  13650  grpinv11  13673  grpinvnz  13675  prdsinvlem  13712  pwsinvg  13716  pwssub  13717  mhmlem  13722  mulgfvalg  13729  mulgsubcl  13744  mulgaddcomlem  13753  mulgneg2  13764  mulgass  13767  issubg  13781  subgex  13784  issubg2m  13797  issubg4m  13801  0subg  13807  isnsg  13810  releqgg  13828  eqgex  13829  eqgval  13831  isghm  13851  ghmlin  13856  ghmrn  13865  ghmeql  13875  f1ghm0to0  13880  iscmn  13901  mgpvalg  13958  isrng  13969  issrg  14000  srgfcl  14008  isring  14035  iscrng  14038  mulgass2  14093  opprvalg  14104  dvdsrvald  14129  isunitd  14142  invrfvald  14158  dvrfvald  14169  dvrvald  14170  isrhm  14194  rhmval  14209  isnzr  14217  islring  14228  issubrng  14235  issubrg  14257  rrgval  14298  isdomn  14305  aprval  14318  aprap  14322  islmod  14327  scaffvalg  14342  lsssetm  14392  lspfval  14424  sraval  14473  rlmvalg  14490  2idlval  14538  2idlvalg  14539  cnfldmulg  14612  zlmval  14663  znf1o  14687  psrlinv  14725  mplsubgfilemcl  14740  istps  14783  clsfval  14852  cnpval  14949  lmconst  14967  txcnp  15022  upxp  15023  uptx  15025  txlm  15030  lmcn2  15031  cnmpt11  15034  cnmpt11f  15035  cnmpt1t  15036  cnmpt21  15042  cnmpt21f  15043  cnmpt2t  15044  mopnval  15193  isxms  15202  isms  15204  comet  15250  mopnex  15256  xmetxp  15258  xmetxpbl  15259  txmetcnp  15269  txmetcn  15270  qtopbasss  15272  cncfi  15329  cncfmpt1f  15349  ivthinclemlm  15385  ivthinclemum  15386  ivthinclemlopn  15387  ivthinclemlr  15388  ivthinclemuopn  15389  ivthinclemur  15390  ivthinclemdisj  15391  ivthinclemloc  15392  ivthinc  15394  ivthdec  15395  ivthreinc  15396  cnlimci  15424  limccnpcntop  15426  eldvap  15433  dvcoapbr  15458  dvcj  15460  dvfre  15461  dvmptcjx  15475  dveflem  15477  elply2  15486  elplyd  15492  plymullem1  15499  plyadd  15502  plymul  15503  plycoeid3  15508  plycolemc  15509  plyco  15510  plycjlemc  15511  plycj  15512  dvply1  15516  sin0pilem2  15533  pilem3  15534  coseq0q4123  15585  coseq0negpitopi  15587  cos11  15604  logltb  15625  rpcxpef  15645  rplogbval  15696  mpodvdsmulf1o  15741  fsumdvdsmul  15742  zabsle1  15755  lgslem2  15757  lgslem3  15758  lgsfcl2  15762  lgsfle1  15765  lgsle1  15771  lgsdirprm  15790  lgseisenlem2  15827  lgsquadlem2  15834  2sqlem1  15870  2sqlem2  15871  mul2sq  15872  2sqlem3  15873  2sqlem9  15880  2sqlem10  15881  vtxvalg  15894  iedgvalg  15895  edgvalg  15937  edgopval  15940  edgstruct  15942  isuhgrm  15949  isushgrm  15950  isupgren  15973  isumgren  15983  isuspgren  16035  isusgren  16036  umgr2edg1  16087  usgredg2vlem1  16100  usgredg2vlem2  16101  ushgredgedg  16104  issubgr  16135  vtxdgfval  16166  vtxedgfi  16167  vtxdg0v  16172  vtxdumgrfival  16176  1loopgrvd0fi  16184  1hevtxdg0fi  16185  1hevtxdg1en  16186  wkslem1  16198  wkslem2  16199  wksfval  16200  iswlk  16201  uspgr2wlkeq  16243  uspgr2wlkeqi  16245  2wlklem  16254  trlsfvalg  16261  clwwlkg  16271  isclwwlk  16272  clwwlkccatlem  16278  clwwlkng  16283  clwwlkn2  16299  clwwlkext2edg  16300  umgr2cwwk2dif  16302  umgr2cwwkdifex  16303  clwwlknonmpo  16306  clwwlknonel  16310  clwwlknonex2lem2  16316  eupthsg  16323  iseupth  16325  eupthseg  16330  eupth2lem3lem3fi  16348  eupth2lem3lem6fi  16349  eupth2lem3lem4fi  16351  eupth2lem3fi  16354  eupth2lemsfi  16356  eupth2fi  16357  eulerpathprum  16358  konigsberglem4  16369  depindlem1  16384  depindlem2  16385  depindlem3  16386  012of  16651  2o01f  16652  subctctexmid  16660  nnsf  16666  nninfalllem1  16669  nninffeq  16681  qdencn  16690  trilpolemclim  16699  trilpolemcl  16700  trilpolemisumle  16701  trilpolemeq1  16703  trilpolemlt1  16704  trilpo  16706  iswomni0  16715  redcwlpo  16719  dceqnconst  16724  dcapnconst  16725  nconstwlpolemgt0  16728  nconstwlpolem  16729  nconstwlpo  16730  neapmkv  16732