Theorem fveq2 5639

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  5642  fveq2d  5643  2fveq3  5644  fvifdc  5661  dffn5imf  5701  fvelimab  5702  ssimaex  5707  fvco4  5718  fvmptssdm  5731  fvmptf  5739  eqfnfv2f  5748  fvelrn  5778  ralrnmpt  5789  rexrnmpt  5790  ffnfvf  5806  fmptco  5813  cofmpt  5816  fcompt  5817  fcoconst  5818  fsn2g  5822  fnressn  5840  fressnfv  5841  fconstfvm  5872  foco2  5894  funiunfvdmf  5905  f1veqaeq  5910  dff13f  5911  f1fveq  5913  f1elima  5914  f1ocnvfv  5920  f1ocnvfvb  5921  fcofo  5925  cocan2  5929  fliftfun  5937  isorel  5949  isocnv  5952  isotr  5957  f1oiso2  5968  canth  5969  imbrov2fvoveq  6043  ffnov  6125  eqfnov  6128  fnovim  6130  fnrnov  6168  foov  6169  funimassov  6172  ovelimab  6173  suppssfv  6231  ofvalg  6245  ofrval  6246  offval2  6251  ofrfval2  6252  ofco  6254  caofinvl  6261  op1std  6311  op2ndd  6312  1stval2  6318  2ndval2  6319  unielxp  6337  reldm  6349  oprabco  6382  2ndconst  6387  f1o2ndf1  6393  mpoxopn0yelv  6405  mpoxopoveq  6406  smoel  6466  tfrlem1  6474  tfrlem3-2d  6478  tfrlem5  6480  tfrlem9  6485  tfr0dm  6488  tfrlemiubacc  6496  tfrlemi1  6498  tfrexlem  6500  tfr1onlemsucfn  6506  tfr1onlemsucaccv  6507  tfr1onlembxssdm  6509  tfr1onlembfn  6510  tfr1onlemubacc  6512  tfr1onlemaccex  6514  tfr1onlemres  6515  tfri1dALT  6517  tfrcllemsucfn  6519  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllembfn  6523  tfrcllemubacc  6525  tfrcllemaccex  6527  tfrcllemres  6528  tfrcldm  6529  tfrcl  6530  tfri3  6533  rdgtfr  6540  rdgss  6549  rdgisuc1  6550  rdgisucinc  6551  rdgon  6552  frecabex  6564  frecabcl  6565  frecfcllem  6570  frecsuclem  6572  frecsuc  6573  frecrdg  6574  oav  6622  omv  6623  oeiv  6624  fvixp  6872  cbvixp  6884  mptelixpg  6903  elixpsn  6904  dom2lem  6945  xpcomco  7010  xpmapen  7036  fidceq  7056  fieq0  7175  ordiso2  7234  djune  7277  updjudhcoinlf  7279  updjudhcoinrg  7280  updjud  7281  omp1eom  7294  0ct  7306  ctmlemr  7307  ctssdclemn0  7309  ctssdccl  7310  ctssdc  7312  enumctlemm  7313  nninfninc  7322  nnnninfeq  7327  nnnninfeq2  7328  enomnilem  7337  finomni  7339  fodjuomnilemdc  7343  fodju0  7346  fodjuomni  7348  ismkvnex  7354  fodjumkv  7359  nninfwlporlemd  7371  nninfwlpor  7373  exmidaclem  7423  cc1  7484  cc2lem  7485  cc2  7486  cc3  7487  mulpipq2  7591  genipv  7729  genpelxp  7731  addcanprleml  7834  addcanprlemu  7835  recexprlemm  7844  recexprlemdisj  7850  recexprlemloc  7851  recexprlem1ssl  7853  recexprlem1ssu  7854  cauappcvgprlemm  7865  cauappcvgprlemdisj  7871  cauappcvgprlemloc  7872  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgprlem1  7879  cauappcvgprlem2  7880  cauappcvgprlemlim  7881  cauappcvgpr  7882  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemm  7888  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprlemcl  7896  caucvgprlemladdfu  7897  caucvgprlemladdrl  7898  caucvgprlem1  7899  caucvgprlem2  7900  caucvgpr  7902  caucvgprprlemell  7905  caucvgprprlemelu  7906  caucvgprprlemcbv  7907  caucvgprprlemval  7908  caucvgprprlemnkeqj  7910  caucvgprprlemnbj  7913  caucvgprprlemml  7914  caucvgprprlemmu  7915  caucvgprprlemopl  7917  caucvgprprlemlol  7918  caucvgprprlemopu  7919  caucvgprprlemloc  7923  caucvgprprlemclphr  7925  caucvgprprlemexbt  7926  caucvgprprlem1  7929  caucvgprprlem2  7930  caucvgsrlemcl  8009  caucvgsrlemfv  8011  caucvgsrlembound  8014  caucvgsrlemgt1  8015  caucvgsrlemoffval  8016  caucvgsrlemoffres  8020  caucvgsrlembnd  8021  caucvgsr  8022  axcaucvglemcau  8118  axcaucvglemres  8119  uz11  9779  cnref1o  9885  fzprval  10317  fztpval  10318  zsupcllemex  10490  infssuzex  10493  suprzubdc  10496  frec2uzuzd  10664  frec2uzltd  10665  frec2uzlt2d  10666  frecuzrdgrrn  10670  frec2uzrdg  10671  frecuzrdgtcl  10674  frecuzrdgg  10678  frecuzrdgfunlem  10681  frecfzennn  10688  seqeq1  10712  iseqovex  10720  seq3val  10722  seqvalcd  10723  seq3-1  10724  seqf  10726  seq3p1  10727  seqovcd  10729  seqp1cd  10732  seq3clss  10733  seq3fveq2  10737  seqfveq2g  10739  seqfveqg  10740  seq3fveq  10741  seq3feq  10742  seq3shft2  10743  seqshft2g  10744  monoord  10747  monoord2  10748  ser3mono  10749  seq3split  10750  seqsplitg  10751  seq3caopr3  10753  seqcaopr3g  10754  seq3caopr2  10755  seqcaopr2g  10756  iseqf1olemkle  10759  iseqf1olemklt  10760  iseqf1olemqval  10762  iseqf1olemqk  10769  iseqf1olemjpcl  10770  iseqf1olemqpcl  10771  iseqf1olemfvp  10772  seq3f1olemqsumkj  10773  seq3f1olemqsum  10775  seq3f1olemstep  10776  seq3f1olemp  10777  seq3f1oleml  10778  seq3f1o  10779  seqf1oglem2a  10780  seqf1og  10783  seq3id2  10788  seq3homo  10789  seq3z  10790  seqhomog  10792  seqfeq4g  10793  ser3ge0  10798  ser3le  10799  exp3vallem  10802  exp3val  10803  facp1  10992  faccl  10997  facdiv  11000  facwordi  11002  faclbnd  11003  facubnd  11007  bcval  11011  bcval5  11025  fz1eqb  11052  omgadd  11065  hashxp  11090  zfz1isolem1  11104  zfz1iso  11105  seq3coll  11106  eqwrd  11154  lswwrd  11160  lswex  11165  ccatfvalfi  11169  ccatval1  11174  ccatval2  11175  ccatalpha  11190  s1eq  11196  eqs1  11205  swrdval  11229  ccatopth2  11298  wrd2ind  11304  seq3shft  11399  reval  11410  replim  11420  cj11  11466  caucvgre  11542  cvg1nlemcau  11545  cvg1nlemres  11546  rexuz3  11551  absval  11562  resqrexlemover  11571  resqrexlemdecn  11573  resqrexlemlo  11574  resqrexlemcalc3  11577  resqrexlemnm  11579  resqrexlemcvg  11580  resqrexlemoverl  11582  resqrexlemglsq  11583  resqrexlemga  11584  resqrexlemsqa  11585  resqrexlemex  11586  abs00bd  11627  cau3lem  11675  caubnd2  11678  climconst  11851  climmpt  11861  climshftlemg  11863  climcn1  11869  climle  11895  climub  11905  climserle  11906  climcau  11908  climcvg1nlem  11910  climcvg1n  11911  serf0  11913  fsum3cvg  11940  summodclem3  11942  summodclem2a  11943  summodclem2  11944  summodc  11945  zsumdc  11946  fsum3  11949  fsumf1o  11952  fisumss  11954  fsum3cvg2  11956  fsum3ser  11959  fsumcl2lem  11960  fsumadd  11968  sumsnf  11971  isummulc2  11988  isumge0  11992  isumadd  11993  fsum2dlemstep  11996  fsummulc2  12010  fsumconst  12016  fsumrelem  12033  isumshft  12052  isum1p  12054  isumnn0nn  12055  isumrpcl  12056  isumlessdc  12058  cvgratnnlemnexp  12086  cvgratnnlemmn  12087  cvgratnnlemseq  12088  cvgratnnlemabsle  12089  cvgratnnlemfm  12091  cvgratnnlemrate  12092  cvgratnn  12093  cvgratz  12094  mertenslemi1  12097  mertenslem2  12098  mertensabs  12099  clim2prod  12101  prodfap0  12107  prodfrecap  12108  prodfdivap  12109  fproddccvg  12134  prodmodclem3  12137  prodmodclem2a  12138  prodmodclem2  12139  prodmodc  12140  zproddc  12141  fprodseq  12145  fprodf1o  12150  fprodssdc  12152  fprodmul  12153  prodsnf  12154  fprodfac  12177  fprodconst  12182  fprod2dlemstep  12184  eftvalcn  12219  ef0lem  12222  ege2le3  12233  efcj  12235  efaddlem  12236  eftlub  12252  efgt1p2  12257  reef11  12261  tanvalap  12270  efieq1re  12334  eirraplem  12339  dvdsabseq  12409  dvdsfac  12422  gcd0id  12551  nninfctlemfo  12612  nn0seqcvgd  12614  alginv  12620  algcvg  12621  algcvga  12624  algfx  12625  eucalglt  12630  lcmid  12653  qredeu  12670  prmfac1  12725  sqne2sq  12750  qnumdenbi  12765  dfphi2  12793  eulerthlemrprm  12802  eulerthlema  12803  eulerthlemh  12804  eulerthlemth  12805  phisum  12814  pcmpt  12917  pcfac  12924  1arithlem4  12940  elgz  12945  4sqlem4  12966  4sqlem12  12976  2expltfac  13013  ennnfonelemk  13022  ennnfonelemp1  13028  ennnfoneleminc  13033  ennnfonelemkh  13034  ennnfonelemhf1o  13035  ennnfonelemex  13036  ennnfonelemhom  13037  ennnfonelemrn  13041  ennnfonelemnn0  13044  ennnfonelemr  13045  ennnfonelemim  13046  ctinfomlemom  13049  ctinfom  13050  ctiunctlemfo  13061  nninfdclemlt  13073  nninfdclemf1  13074  sloteq  13088  ressvalsets  13148  topnvalg  13335  prdsbasprj  13366  prdsplusgfval  13368  prdsmulrfval  13370  imasex  13389  imasaddvallemg  13399  qusex  13409  xpsfrnel  13428  xpsfeq  13429  xpsval  13436  ismgm  13441  plusffvalg  13446  grpidvalg  13457  gsumfzval  13475  gsumval2  13481  issgrp  13487  ismnddef  13502  prdsidlem  13531  pws0g  13535  ismhm  13545  mhmex  13546  mhmlin  13551  issubm  13556  mhmeql  13576  isgrp  13590  grpn0  13619  grpinvfvalg  13626  grpsubfvalg  13629  grpsubval  13630  grpinv11  13653  grpinvnz  13655  prdsinvlem  13692  pwsinvg  13696  pwssub  13697  mhmlem  13702  mulgfvalg  13709  mulgsubcl  13724  mulgaddcomlem  13733  mulgneg2  13744  mulgass  13747  issubg  13761  subgex  13764  issubg2m  13777  issubg4m  13781  0subg  13787  isnsg  13790  releqgg  13808  eqgex  13809  eqgval  13811  isghm  13831  ghmlin  13836  ghmrn  13845  ghmeql  13855  f1ghm0to0  13860  iscmn  13881  mgpvalg  13938  isrng  13949  issrg  13980  srgfcl  13988  isring  14015  iscrng  14018  mulgass2  14073  opprvalg  14084  dvdsrvald  14109  isunitd  14122  invrfvald  14138  dvrfvald  14149  dvrvald  14150  isrhm  14174  rhmval  14189  isnzr  14197  islring  14208  issubrng  14215  issubrg  14237  rrgval  14278  isdomn  14285  aprval  14298  aprap  14302  islmod  14307  scaffvalg  14322  lsssetm  14372  lspfval  14404  sraval  14453  rlmvalg  14470  2idlval  14518  2idlvalg  14519  cnfldmulg  14592  zlmval  14643  znf1o  14667  psrlinv  14700  mplsubgfilemcl  14715  istps  14758  clsfval  14827  cnpval  14924  lmconst  14942  txcnp  14997  upxp  14998  uptx  15000  txlm  15005  lmcn2  15006  cnmpt11  15009  cnmpt11f  15010  cnmpt1t  15011  cnmpt21  15017  cnmpt21f  15018  cnmpt2t  15019  mopnval  15168  isxms  15177  isms  15179  comet  15225  mopnex  15231  xmetxp  15233  xmetxpbl  15234  txmetcnp  15244  txmetcn  15245  qtopbasss  15247  cncfi  15304  cncfmpt1f  15324  ivthinclemlm  15360  ivthinclemum  15361  ivthinclemlopn  15362  ivthinclemlr  15363  ivthinclemuopn  15364  ivthinclemur  15365  ivthinclemdisj  15366  ivthinclemloc  15367  ivthinc  15369  ivthdec  15370  ivthreinc  15371  cnlimci  15399  limccnpcntop  15401  eldvap  15408  dvcoapbr  15433  dvcj  15435  dvfre  15436  dvmptcjx  15450  dveflem  15452  elply2  15461  elplyd  15467  plymullem1  15474  plyadd  15477  plymul  15478  plycoeid3  15483  plycolemc  15484  plyco  15485  plycjlemc  15486  plycj  15487  dvply1  15491  sin0pilem2  15508  pilem3  15509  coseq0q4123  15560  coseq0negpitopi  15562  cos11  15579  logltb  15600  rpcxpef  15620  rplogbval  15671  mpodvdsmulf1o  15716  fsumdvdsmul  15717  zabsle1  15730  lgslem2  15732  lgslem3  15733  lgsfcl2  15737  lgsfle1  15740  lgsle1  15746  lgsdirprm  15765  lgseisenlem2  15802  lgsquadlem2  15809  2sqlem1  15845  2sqlem2  15846  mul2sq  15847  2sqlem3  15848  2sqlem9  15855  2sqlem10  15856  vtxvalg  15869  iedgvalg  15870  edgvalg  15912  edgopval  15915  edgstruct  15917  isuhgrm  15924  isushgrm  15925  isupgren  15948  isumgren  15958  isuspgren  16010  isusgren  16011  umgr2edg1  16062  usgredg2vlem1  16075  usgredg2vlem2  16076  ushgredgedg  16079  issubgr  16110  vtxdgfval  16141  vtxedgfi  16142  vtxdg0v  16147  vtxdumgrfival  16151  1loopgrvd0fi  16159  1hevtxdg0fi  16160  1hevtxdg1en  16161  wkslem1  16173  wkslem2  16174  wksfval  16175  iswlk  16176  uspgr2wlkeq  16218  uspgr2wlkeqi  16220  2wlklem  16229  trlsfvalg  16236  clwwlkg  16246  isclwwlk  16247  clwwlkccatlem  16253  clwwlkng  16258  clwwlkn2  16274  clwwlkext2edg  16275  umgr2cwwk2dif  16277  umgr2cwwkdifex  16278  clwwlknonmpo  16281  clwwlknonel  16285  clwwlknonex2lem2  16291  eupthsg  16298  iseupth  16300  eupthseg  16305  012of  16595  2o01f  16596  subctctexmid  16604  nnsf  16610  nninfalllem1  16613  nninffeq  16625  qdencn  16634  trilpolemclim  16643  trilpolemcl  16644  trilpolemisumle  16645  trilpolemeq1  16647  trilpolemlt1  16648  trilpo  16650  iswomni0  16658  redcwlpo  16662  dceqnconst  16667  dcapnconst  16668  nconstwlpolemgt0  16671  nconstwlpolem  16672  nconstwlpo  16673  neapmkv  16675