Theorem fveq2 5627

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 4086	. . 3 |- ( A = B -> ( A F x <-> B F x ) )
2	1	iotabidv 5301	. 2 |- ( A = B -> ( iota x A F x ) = ( iota x B F x ) )
3		df-fv 5326	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5326	. 2 |- ( F ` B ) = ( iota x B F x )
5	2, 3, 4	3eqtr4g 2287	1 |- ( A = B -> ( F ` A ) = ( F ` B ) )

Syntax hints:   -> wi 4   = wceq 1395   class class class wbr 4083   iotacio 5276   ` cfv 5318

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326

This theorem is referenced by:  fveq2i  5630  fveq2d  5631  2fveq3  5632  fvifdc  5649  dffn5imf  5689  fvelimab  5690  ssimaex  5695  fvco4  5706  fvmptssdm  5719  fvmptf  5727  eqfnfv2f  5736  fvelrn  5766  ralrnmpt  5777  rexrnmpt  5778  ffnfvf  5794  fmptco  5801  cofmpt  5804  fcompt  5805  fcoconst  5806  fnressn  5825  fressnfv  5826  fconstfvm  5857  foco2  5877  funiunfvdmf  5888  f1veqaeq  5893  dff13f  5894  f1fveq  5896  f1elima  5897  f1ocnvfv  5903  f1ocnvfvb  5904  fcofo  5908  cocan2  5912  fliftfun  5920  isorel  5932  isocnv  5935  isotr  5940  f1oiso2  5951  canth  5952  imbrov2fvoveq  6026  ffnov  6108  eqfnov  6111  fnovim  6113  fnrnov  6151  foov  6152  funimassov  6155  ovelimab  6156  suppssfv  6214  ofvalg  6228  ofrval  6229  offval2  6234  ofrfval2  6235  ofco  6237  caofinvl  6244  op1std  6294  op2ndd  6295  1stval2  6301  2ndval2  6302  unielxp  6320  reldm  6332  oprabco  6363  2ndconst  6368  f1o2ndf1  6374  mpoxopn0yelv  6385  mpoxopoveq  6386  smoel  6446  tfrlem1  6454  tfrlem3-2d  6458  tfrlem5  6460  tfrlem9  6465  tfr0dm  6468  tfrlemiubacc  6476  tfrlemi1  6478  tfrexlem  6480  tfr1onlemsucfn  6486  tfr1onlemsucaccv  6487  tfr1onlembxssdm  6489  tfr1onlembfn  6490  tfr1onlemubacc  6492  tfr1onlemaccex  6494  tfr1onlemres  6495  tfri1dALT  6497  tfrcllemsucfn  6499  tfrcllemsucaccv  6500  tfrcllembxssdm  6502  tfrcllembfn  6503  tfrcllemubacc  6505  tfrcllemaccex  6507  tfrcllemres  6508  tfrcldm  6509  tfrcl  6510  tfri3  6513  rdgtfr  6520  rdgss  6529  rdgisuc1  6530  rdgisucinc  6531  rdgon  6532  frecabex  6544  frecabcl  6545  frecfcllem  6550  frecsuclem  6552  frecsuc  6553  frecrdg  6554  oav  6600  omv  6601  oeiv  6602  fvixp  6850  cbvixp  6862  mptelixpg  6881  elixpsn  6882  dom2lem  6923  xpcomco  6985  xpmapen  7011  fidceq  7031  fieq0  7143  ordiso2  7202  djune  7245  updjudhcoinlf  7247  updjudhcoinrg  7248  updjud  7249  omp1eom  7262  0ct  7274  ctmlemr  7275  ctssdclemn0  7277  ctssdccl  7278  ctssdc  7280  enumctlemm  7281  nninfninc  7290  nnnninfeq  7295  nnnninfeq2  7296  enomnilem  7305  finomni  7307  fodjuomnilemdc  7311  fodju0  7314  fodjuomni  7316  ismkvnex  7322  fodjumkv  7327  nninfwlporlemd  7339  nninfwlpor  7341  exmidaclem  7390  cc1  7451  cc2lem  7452  cc2  7453  cc3  7454  mulpipq2  7558  genipv  7696  genpelxp  7698  addcanprleml  7801  addcanprlemu  7802  recexprlemm  7811  recexprlemdisj  7817  recexprlemloc  7818  recexprlem1ssl  7820  recexprlem1ssu  7821  cauappcvgprlemm  7832  cauappcvgprlemdisj  7838  cauappcvgprlemloc  7839  cauappcvgprlemladdru  7843  cauappcvgprlemladdrl  7844  cauappcvgprlem1  7846  cauappcvgprlem2  7847  cauappcvgprlemlim  7848  cauappcvgpr  7849  caucvgprlemnkj  7853  caucvgprlemnbj  7854  caucvgprlemm  7855  caucvgprlemdisj  7861  caucvgprlemloc  7862  caucvgprlemcl  7863  caucvgprlemladdfu  7864  caucvgprlemladdrl  7865  caucvgprlem1  7866  caucvgprlem2  7867  caucvgpr  7869  caucvgprprlemell  7872  caucvgprprlemelu  7873  caucvgprprlemcbv  7874  caucvgprprlemval  7875  caucvgprprlemnkeqj  7877  caucvgprprlemnbj  7880  caucvgprprlemml  7881  caucvgprprlemmu  7882  caucvgprprlemopl  7884  caucvgprprlemlol  7885  caucvgprprlemopu  7886  caucvgprprlemloc  7890  caucvgprprlemclphr  7892  caucvgprprlemexbt  7893  caucvgprprlem1  7896  caucvgprprlem2  7897  caucvgsrlemcl  7976  caucvgsrlemfv  7978  caucvgsrlembound  7981  caucvgsrlemgt1  7982  caucvgsrlemoffval  7983  caucvgsrlemoffres  7987  caucvgsrlembnd  7988  caucvgsr  7989  axcaucvglemcau  8085  axcaucvglemres  8086  uz11  9745  cnref1o  9846  fzprval  10278  fztpval  10279  zsupcllemex  10450  infssuzex  10453  suprzubdc  10456  frec2uzuzd  10624  frec2uzltd  10625  frec2uzlt2d  10626  frecuzrdgrrn  10630  frec2uzrdg  10631  frecuzrdgtcl  10634  frecuzrdgg  10638  frecuzrdgfunlem  10641  frecfzennn  10648  seqeq1  10672  iseqovex  10680  seq3val  10682  seqvalcd  10683  seq3-1  10684  seqf  10686  seq3p1  10687  seqovcd  10689  seqp1cd  10692  seq3clss  10693  seq3fveq2  10697  seqfveq2g  10699  seqfveqg  10700  seq3fveq  10701  seq3feq  10702  seq3shft2  10703  seqshft2g  10704  monoord  10707  monoord2  10708  ser3mono  10709  seq3split  10710  seqsplitg  10711  seq3caopr3  10713  seqcaopr3g  10714  seq3caopr2  10715  seqcaopr2g  10716  iseqf1olemkle  10719  iseqf1olemklt  10720  iseqf1olemqval  10722  iseqf1olemqk  10729  iseqf1olemjpcl  10730  iseqf1olemqpcl  10731  iseqf1olemfvp  10732  seq3f1olemqsumkj  10733  seq3f1olemqsum  10735  seq3f1olemstep  10736  seq3f1olemp  10737  seq3f1oleml  10738  seq3f1o  10739  seqf1oglem2a  10740  seqf1og  10743  seq3id2  10748  seq3homo  10749  seq3z  10750  seqhomog  10752  seqfeq4g  10753  ser3ge0  10758  ser3le  10759  exp3vallem  10762  exp3val  10763  facp1  10952  faccl  10957  facdiv  10960  facwordi  10962  faclbnd  10963  facubnd  10967  bcval  10971  bcval5  10985  fz1eqb  11012  omgadd  11024  hashxp  11048  zfz1isolem1  11062  zfz1iso  11063  seq3coll  11064  eqwrd  11112  lswwrd  11118  lswex  11123  ccatfvalfi  11127  ccatval1  11132  ccatval2  11133  s1eq  11152  eqs1  11161  swrdval  11180  ccatopth2  11249  wrd2ind  11255  seq3shft  11349  reval  11360  replim  11370  cj11  11416  caucvgre  11492  cvg1nlemcau  11495  cvg1nlemres  11496  rexuz3  11501  absval  11512  resqrexlemover  11521  resqrexlemdecn  11523  resqrexlemlo  11524  resqrexlemcalc3  11527  resqrexlemnm  11529  resqrexlemcvg  11530  resqrexlemoverl  11532  resqrexlemglsq  11533  resqrexlemga  11534  resqrexlemsqa  11535  resqrexlemex  11536  abs00bd  11577  cau3lem  11625  caubnd2  11628  climconst  11801  climmpt  11811  climshftlemg  11813  climcn1  11819  climle  11845  climub  11855  climserle  11856  climcau  11858  climcvg1nlem  11860  climcvg1n  11861  serf0  11863  fsum3cvg  11889  summodclem3  11891  summodclem2a  11892  summodclem2  11893  summodc  11894  zsumdc  11895  fsum3  11898  fsumf1o  11901  fisumss  11903  fsum3cvg2  11905  fsum3ser  11908  fsumcl2lem  11909  fsumadd  11917  sumsnf  11920  isummulc2  11937  isumge0  11941  isumadd  11942  fsum2dlemstep  11945  fsummulc2  11959  fsumconst  11965  fsumrelem  11982  isumshft  12001  isum1p  12003  isumnn0nn  12004  isumrpcl  12005  isumlessdc  12007  cvgratnnlemnexp  12035  cvgratnnlemmn  12036  cvgratnnlemseq  12037  cvgratnnlemabsle  12038  cvgratnnlemfm  12040  cvgratnnlemrate  12041  cvgratnn  12042  cvgratz  12043  mertenslemi1  12046  mertenslem2  12047  mertensabs  12048  clim2prod  12050  prodfap0  12056  prodfrecap  12057  prodfdivap  12058  fproddccvg  12083  prodmodclem3  12086  prodmodclem2a  12087  prodmodclem2  12088  prodmodc  12089  zproddc  12090  fprodseq  12094  fprodf1o  12099  fprodssdc  12101  fprodmul  12102  prodsnf  12103  fprodfac  12126  fprodconst  12131  fprod2dlemstep  12133  eftvalcn  12168  ef0lem  12171  ege2le3  12182  efcj  12184  efaddlem  12185  eftlub  12201  efgt1p2  12206  reef11  12210  tanvalap  12219  efieq1re  12283  eirraplem  12288  dvdsabseq  12358  dvdsfac  12371  gcd0id  12500  nninfctlemfo  12561  nn0seqcvgd  12563  alginv  12569  algcvg  12570  algcvga  12573  algfx  12574  eucalglt  12579  lcmid  12602  qredeu  12619  prmfac1  12674  sqne2sq  12699  qnumdenbi  12714  dfphi2  12742  eulerthlemrprm  12751  eulerthlema  12752  eulerthlemh  12753  eulerthlemth  12754  phisum  12763  pcmpt  12866  pcfac  12873  1arithlem4  12889  elgz  12894  4sqlem4  12915  4sqlem12  12925  2expltfac  12962  ennnfonelemk  12971  ennnfonelemp1  12977  ennnfoneleminc  12982  ennnfonelemkh  12983  ennnfonelemhf1o  12984  ennnfonelemex  12985  ennnfonelemhom  12986  ennnfonelemrn  12990  ennnfonelemnn0  12993  ennnfonelemr  12994  ennnfonelemim  12995  ctinfomlemom  12998  ctinfom  12999  ctiunctlemfo  13010  nninfdclemlt  13022  nninfdclemf1  13023  sloteq  13037  ressvalsets  13097  topnvalg  13284  prdsbasprj  13315  prdsplusgfval  13317  prdsmulrfval  13319  imasex  13338  imasaddvallemg  13348  qusex  13358  xpsfrnel  13377  xpsfeq  13378  xpsval  13385  ismgm  13390  plusffvalg  13395  grpidvalg  13406  gsumfzval  13424  gsumval2  13430  issgrp  13436  ismnddef  13451  prdsidlem  13480  pws0g  13484  ismhm  13494  mhmex  13495  mhmlin  13500  issubm  13505  mhmeql  13525  isgrp  13539  grpn0  13568  grpinvfvalg  13575  grpsubfvalg  13578  grpsubval  13579  grpinv11  13602  grpinvnz  13604  prdsinvlem  13641  pwsinvg  13645  pwssub  13646  mhmlem  13651  mulgfvalg  13658  mulgsubcl  13673  mulgaddcomlem  13682  mulgneg2  13693  mulgass  13696  issubg  13710  subgex  13713  issubg2m  13726  issubg4m  13730  0subg  13736  isnsg  13739  releqgg  13757  eqgex  13758  eqgval  13760  isghm  13780  ghmlin  13785  ghmrn  13794  ghmeql  13804  f1ghm0to0  13809  iscmn  13830  mgpvalg  13886  isrng  13897  issrg  13928  srgfcl  13936  isring  13963  iscrng  13966  mulgass2  14021  opprvalg  14032  dvdsrvald  14057  isunitd  14070  invrfvald  14086  dvrfvald  14097  dvrvald  14098  isrhm  14122  rhmval  14137  isnzr  14145  islring  14156  issubrng  14163  issubrg  14185  rrgval  14226  isdomn  14233  aprval  14246  aprap  14250  islmod  14255  scaffvalg  14270  lsssetm  14320  lspfval  14352  sraval  14401  rlmvalg  14418  2idlval  14466  2idlvalg  14467  cnfldmulg  14540  zlmval  14591  znf1o  14615  psrlinv  14648  mplsubgfilemcl  14663  istps  14706  clsfval  14775  cnpval  14872  lmconst  14890  txcnp  14945  upxp  14946  uptx  14948  txlm  14953  lmcn2  14954  cnmpt11  14957  cnmpt11f  14958  cnmpt1t  14959  cnmpt21  14965  cnmpt21f  14966  cnmpt2t  14967  mopnval  15116  isxms  15125  isms  15127  comet  15173  mopnex  15179  xmetxp  15181  xmetxpbl  15182  txmetcnp  15192  txmetcn  15193  qtopbasss  15195  cncfi  15252  cncfmpt1f  15272  ivthinclemlm  15308  ivthinclemum  15309  ivthinclemlopn  15310  ivthinclemlr  15311  ivthinclemuopn  15312  ivthinclemur  15313  ivthinclemdisj  15314  ivthinclemloc  15315  ivthinc  15317  ivthdec  15318  ivthreinc  15319  cnlimci  15347  limccnpcntop  15349  eldvap  15356  dvcoapbr  15381  dvcj  15383  dvfre  15384  dvmptcjx  15398  dveflem  15400  elply2  15409  elplyd  15415  plymullem1  15422  plyadd  15425  plymul  15426  plycoeid3  15431  plycolemc  15432  plyco  15433  plycjlemc  15434  plycj  15435  dvply1  15439  sin0pilem2  15456  pilem3  15457  coseq0q4123  15508  coseq0negpitopi  15510  cos11  15527  logltb  15548  rpcxpef  15568  rplogbval  15619  mpodvdsmulf1o  15664  fsumdvdsmul  15665  zabsle1  15678  lgslem2  15680  lgslem3  15681  lgsfcl2  15685  lgsfle1  15688  lgsle1  15694  lgsdirprm  15713  lgseisenlem2  15750  lgsquadlem2  15757  2sqlem1  15793  2sqlem2  15794  mul2sq  15795  2sqlem3  15796  2sqlem9  15803  2sqlem10  15804  vtxvalg  15817  iedgvalg  15818  edgvalg  15860  edgopval  15862  edgstruct  15864  isuhgrm  15871  isushgrm  15872  isupgren  15895  isumgren  15905  isuspgren  15955  isusgren  15956  umgr2edg1  16007  usgredg2vlem1  16020  usgredg2vlem2  16021  ushgredgedg  16024  wkslem1  16033  wkslem2  16034  wksfval  16035  iswlk  16036  uspgr2wlkeq  16076  uspgr2wlkeqi  16078  012of  16357  2o01f  16358  subctctexmid  16366  nnsf  16371  nninfalllem1  16374  nninffeq  16386  qdencn  16395  trilpolemclim  16404  trilpolemcl  16405  trilpolemisumle  16406  trilpolemeq1  16408  trilpolemlt1  16409  trilpo  16411  iswomni0  16419  redcwlpo  16423  dceqnconst  16428  dcapnconst  16429  nconstwlpolemgt0  16432  nconstwlpolem  16433  nconstwlpo  16434  neapmkv  16436