Theorem fveq2 5629

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  5632  fveq2d  5633  2fveq3  5634  fvifdc  5651  dffn5imf  5691  fvelimab  5692  ssimaex  5697  fvco4  5708  fvmptssdm  5721  fvmptf  5729  eqfnfv2f  5738  fvelrn  5768  ralrnmpt  5779  rexrnmpt  5780  ffnfvf  5796  fmptco  5803  cofmpt  5806  fcompt  5807  fcoconst  5808  fnressn  5829  fressnfv  5830  fconstfvm  5861  foco2  5883  funiunfvdmf  5894  f1veqaeq  5899  dff13f  5900  f1fveq  5902  f1elima  5903  f1ocnvfv  5909  f1ocnvfvb  5910  fcofo  5914  cocan2  5918  fliftfun  5926  isorel  5938  isocnv  5941  isotr  5946  f1oiso2  5957  canth  5958  imbrov2fvoveq  6032  ffnov  6114  eqfnov  6117  fnovim  6119  fnrnov  6157  foov  6158  funimassov  6161  ovelimab  6162  suppssfv  6220  ofvalg  6234  ofrval  6235  offval2  6240  ofrfval2  6241  ofco  6243  caofinvl  6250  op1std  6300  op2ndd  6301  1stval2  6307  2ndval2  6308  unielxp  6326  reldm  6338  oprabco  6369  2ndconst  6374  f1o2ndf1  6380  mpoxopn0yelv  6391  mpoxopoveq  6392  smoel  6452  tfrlem1  6460  tfrlem3-2d  6464  tfrlem5  6466  tfrlem9  6471  tfr0dm  6474  tfrlemiubacc  6482  tfrlemi1  6484  tfrexlem  6486  tfr1onlemsucfn  6492  tfr1onlemsucaccv  6493  tfr1onlembxssdm  6495  tfr1onlembfn  6496  tfr1onlemubacc  6498  tfr1onlemaccex  6500  tfr1onlemres  6501  tfri1dALT  6503  tfrcllemsucfn  6505  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllembfn  6509  tfrcllemubacc  6511  tfrcllemaccex  6513  tfrcllemres  6514  tfrcldm  6515  tfrcl  6516  tfri3  6519  rdgtfr  6526  rdgss  6535  rdgisuc1  6536  rdgisucinc  6537  rdgon  6538  frecabex  6550  frecabcl  6551  frecfcllem  6556  frecsuclem  6558  frecsuc  6559  frecrdg  6560  oav  6608  omv  6609  oeiv  6610  fvixp  6858  cbvixp  6870  mptelixpg  6889  elixpsn  6890  dom2lem  6931  xpcomco  6993  xpmapen  7019  fidceq  7039  fieq0  7154  ordiso2  7213  djune  7256  updjudhcoinlf  7258  updjudhcoinrg  7259  updjud  7260  omp1eom  7273  0ct  7285  ctmlemr  7286  ctssdclemn0  7288  ctssdccl  7289  ctssdc  7291  enumctlemm  7292  nninfninc  7301  nnnninfeq  7306  nnnninfeq2  7307  enomnilem  7316  finomni  7318  fodjuomnilemdc  7322  fodju0  7325  fodjuomni  7327  ismkvnex  7333  fodjumkv  7338  nninfwlporlemd  7350  nninfwlpor  7352  exmidaclem  7401  cc1  7462  cc2lem  7463  cc2  7464  cc3  7465  mulpipq2  7569  genipv  7707  genpelxp  7709  addcanprleml  7812  addcanprlemu  7813  recexprlemm  7822  recexprlemdisj  7828  recexprlemloc  7829  recexprlem1ssl  7831  recexprlem1ssu  7832  cauappcvgprlemm  7843  cauappcvgprlemdisj  7849  cauappcvgprlemloc  7850  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  cauappcvgprlem1  7857  cauappcvgprlem2  7858  cauappcvgprlemlim  7859  cauappcvgpr  7860  caucvgprlemnkj  7864  caucvgprlemnbj  7865  caucvgprlemm  7866  caucvgprlemdisj  7872  caucvgprlemloc  7873  caucvgprlemcl  7874  caucvgprlemladdfu  7875  caucvgprlemladdrl  7876  caucvgprlem1  7877  caucvgprlem2  7878  caucvgpr  7880  caucvgprprlemell  7883  caucvgprprlemelu  7884  caucvgprprlemcbv  7885  caucvgprprlemval  7886  caucvgprprlemnkeqj  7888  caucvgprprlemnbj  7891  caucvgprprlemml  7892  caucvgprprlemmu  7893  caucvgprprlemopl  7895  caucvgprprlemlol  7896  caucvgprprlemopu  7897  caucvgprprlemloc  7901  caucvgprprlemclphr  7903  caucvgprprlemexbt  7904  caucvgprprlem1  7907  caucvgprprlem2  7908  caucvgsrlemcl  7987  caucvgsrlemfv  7989  caucvgsrlembound  7992  caucvgsrlemgt1  7993  caucvgsrlemoffval  7994  caucvgsrlemoffres  7998  caucvgsrlembnd  7999  caucvgsr  8000  axcaucvglemcau  8096  axcaucvglemres  8097  uz11  9757  cnref1o  9858  fzprval  10290  fztpval  10291  zsupcllemex  10462  infssuzex  10465  suprzubdc  10468  frec2uzuzd  10636  frec2uzltd  10637  frec2uzlt2d  10638  frecuzrdgrrn  10642  frec2uzrdg  10643  frecuzrdgtcl  10646  frecuzrdgg  10650  frecuzrdgfunlem  10653  frecfzennn  10660  seqeq1  10684  iseqovex  10692  seq3val  10694  seqvalcd  10695  seq3-1  10696  seqf  10698  seq3p1  10699  seqovcd  10701  seqp1cd  10704  seq3clss  10705  seq3fveq2  10709  seqfveq2g  10711  seqfveqg  10712  seq3fveq  10713  seq3feq  10714  seq3shft2  10715  seqshft2g  10716  monoord  10719  monoord2  10720  ser3mono  10721  seq3split  10722  seqsplitg  10723  seq3caopr3  10725  seqcaopr3g  10726  seq3caopr2  10727  seqcaopr2g  10728  iseqf1olemkle  10731  iseqf1olemklt  10732  iseqf1olemqval  10734  iseqf1olemqk  10741  iseqf1olemjpcl  10742  iseqf1olemqpcl  10743  iseqf1olemfvp  10744  seq3f1olemqsumkj  10745  seq3f1olemqsum  10747  seq3f1olemstep  10748  seq3f1olemp  10749  seq3f1oleml  10750  seq3f1o  10751  seqf1oglem2a  10752  seqf1og  10755  seq3id2  10760  seq3homo  10761  seq3z  10762  seqhomog  10764  seqfeq4g  10765  ser3ge0  10770  ser3le  10771  exp3vallem  10774  exp3val  10775  facp1  10964  faccl  10969  facdiv  10972  facwordi  10974  faclbnd  10975  facubnd  10979  bcval  10983  bcval5  10997  fz1eqb  11024  omgadd  11036  hashxp  11061  zfz1isolem1  11075  zfz1iso  11076  seq3coll  11077  eqwrd  11125  lswwrd  11131  lswex  11136  ccatfvalfi  11140  ccatval1  11145  ccatval2  11146  ccatalpha  11161  s1eq  11167  eqs1  11176  swrdval  11196  ccatopth2  11265  wrd2ind  11271  seq3shft  11365  reval  11376  replim  11386  cj11  11432  caucvgre  11508  cvg1nlemcau  11511  cvg1nlemres  11512  rexuz3  11517  absval  11528  resqrexlemover  11537  resqrexlemdecn  11539  resqrexlemlo  11540  resqrexlemcalc3  11543  resqrexlemnm  11545  resqrexlemcvg  11546  resqrexlemoverl  11548  resqrexlemglsq  11549  resqrexlemga  11550  resqrexlemsqa  11551  resqrexlemex  11552  abs00bd  11593  cau3lem  11641  caubnd2  11644  climconst  11817  climmpt  11827  climshftlemg  11829  climcn1  11835  climle  11861  climub  11871  climserle  11872  climcau  11874  climcvg1nlem  11876  climcvg1n  11877  serf0  11879  fsum3cvg  11905  summodclem3  11907  summodclem2a  11908  summodclem2  11909  summodc  11910  zsumdc  11911  fsum3  11914  fsumf1o  11917  fisumss  11919  fsum3cvg2  11921  fsum3ser  11924  fsumcl2lem  11925  fsumadd  11933  sumsnf  11936  isummulc2  11953  isumge0  11957  isumadd  11958  fsum2dlemstep  11961  fsummulc2  11975  fsumconst  11981  fsumrelem  11998  isumshft  12017  isum1p  12019  isumnn0nn  12020  isumrpcl  12021  isumlessdc  12023  cvgratnnlemnexp  12051  cvgratnnlemmn  12052  cvgratnnlemseq  12053  cvgratnnlemabsle  12054  cvgratnnlemfm  12056  cvgratnnlemrate  12057  cvgratnn  12058  cvgratz  12059  mertenslemi1  12062  mertenslem2  12063  mertensabs  12064  clim2prod  12066  prodfap0  12072  prodfrecap  12073  prodfdivap  12074  fproddccvg  12099  prodmodclem3  12102  prodmodclem2a  12103  prodmodclem2  12104  prodmodc  12105  zproddc  12106  fprodseq  12110  fprodf1o  12115  fprodssdc  12117  fprodmul  12118  prodsnf  12119  fprodfac  12142  fprodconst  12147  fprod2dlemstep  12149  eftvalcn  12184  ef0lem  12187  ege2le3  12198  efcj  12200  efaddlem  12201  eftlub  12217  efgt1p2  12222  reef11  12226  tanvalap  12235  efieq1re  12299  eirraplem  12304  dvdsabseq  12374  dvdsfac  12387  gcd0id  12516  nninfctlemfo  12577  nn0seqcvgd  12579  alginv  12585  algcvg  12586  algcvga  12589  algfx  12590  eucalglt  12595  lcmid  12618  qredeu  12635  prmfac1  12690  sqne2sq  12715  qnumdenbi  12730  dfphi2  12758  eulerthlemrprm  12767  eulerthlema  12768  eulerthlemh  12769  eulerthlemth  12770  phisum  12779  pcmpt  12882  pcfac  12889  1arithlem4  12905  elgz  12910  4sqlem4  12931  4sqlem12  12941  2expltfac  12978  ennnfonelemk  12987  ennnfonelemp1  12993  ennnfoneleminc  12998  ennnfonelemkh  12999  ennnfonelemhf1o  13000  ennnfonelemex  13001  ennnfonelemhom  13002  ennnfonelemrn  13006  ennnfonelemnn0  13009  ennnfonelemr  13010  ennnfonelemim  13011  ctinfomlemom  13014  ctinfom  13015  ctiunctlemfo  13026  nninfdclemlt  13038  nninfdclemf1  13039  sloteq  13053  ressvalsets  13113  topnvalg  13300  prdsbasprj  13331  prdsplusgfval  13333  prdsmulrfval  13335  imasex  13354  imasaddvallemg  13364  qusex  13374  xpsfrnel  13393  xpsfeq  13394  xpsval  13401  ismgm  13406  plusffvalg  13411  grpidvalg  13422  gsumfzval  13440  gsumval2  13446  issgrp  13452  ismnddef  13467  prdsidlem  13496  pws0g  13500  ismhm  13510  mhmex  13511  mhmlin  13516  issubm  13521  mhmeql  13541  isgrp  13555  grpn0  13584  grpinvfvalg  13591  grpsubfvalg  13594  grpsubval  13595  grpinv11  13618  grpinvnz  13620  prdsinvlem  13657  pwsinvg  13661  pwssub  13662  mhmlem  13667  mulgfvalg  13674  mulgsubcl  13689  mulgaddcomlem  13698  mulgneg2  13709  mulgass  13712  issubg  13726  subgex  13729  issubg2m  13742  issubg4m  13746  0subg  13752  isnsg  13755  releqgg  13773  eqgex  13774  eqgval  13776  isghm  13796  ghmlin  13801  ghmrn  13810  ghmeql  13820  f1ghm0to0  13825  iscmn  13846  mgpvalg  13902  isrng  13913  issrg  13944  srgfcl  13952  isring  13979  iscrng  13982  mulgass2  14037  opprvalg  14048  dvdsrvald  14073  isunitd  14086  invrfvald  14102  dvrfvald  14113  dvrvald  14114  isrhm  14138  rhmval  14153  isnzr  14161  islring  14172  issubrng  14179  issubrg  14201  rrgval  14242  isdomn  14249  aprval  14262  aprap  14266  islmod  14271  scaffvalg  14286  lsssetm  14336  lspfval  14368  sraval  14417  rlmvalg  14434  2idlval  14482  2idlvalg  14483  cnfldmulg  14556  zlmval  14607  znf1o  14631  psrlinv  14664  mplsubgfilemcl  14679  istps  14722  clsfval  14791  cnpval  14888  lmconst  14906  txcnp  14961  upxp  14962  uptx  14964  txlm  14969  lmcn2  14970  cnmpt11  14973  cnmpt11f  14974  cnmpt1t  14975  cnmpt21  14981  cnmpt21f  14982  cnmpt2t  14983  mopnval  15132  isxms  15141  isms  15143  comet  15189  mopnex  15195  xmetxp  15197  xmetxpbl  15198  txmetcnp  15208  txmetcn  15209  qtopbasss  15211  cncfi  15268  cncfmpt1f  15288  ivthinclemlm  15324  ivthinclemum  15325  ivthinclemlopn  15326  ivthinclemlr  15327  ivthinclemuopn  15328  ivthinclemur  15329  ivthinclemdisj  15330  ivthinclemloc  15331  ivthinc  15333  ivthdec  15334  ivthreinc  15335  cnlimci  15363  limccnpcntop  15365  eldvap  15372  dvcoapbr  15397  dvcj  15399  dvfre  15400  dvmptcjx  15414  dveflem  15416  elply2  15425  elplyd  15431  plymullem1  15438  plyadd  15441  plymul  15442  plycoeid3  15447  plycolemc  15448  plyco  15449  plycjlemc  15450  plycj  15451  dvply1  15455  sin0pilem2  15472  pilem3  15473  coseq0q4123  15524  coseq0negpitopi  15526  cos11  15543  logltb  15564  rpcxpef  15584  rplogbval  15635  mpodvdsmulf1o  15680  fsumdvdsmul  15681  zabsle1  15694  lgslem2  15696  lgslem3  15697  lgsfcl2  15701  lgsfle1  15704  lgsle1  15710  lgsdirprm  15729  lgseisenlem2  15766  lgsquadlem2  15773  2sqlem1  15809  2sqlem2  15810  mul2sq  15811  2sqlem3  15812  2sqlem9  15819  2sqlem10  15820  vtxvalg  15833  iedgvalg  15834  edgvalg  15876  edgopval  15878  edgstruct  15880  isuhgrm  15887  isushgrm  15888  isupgren  15911  isumgren  15921  isuspgren  15971  isusgren  15972  umgr2edg1  16023  usgredg2vlem1  16036  usgredg2vlem2  16037  ushgredgedg  16040  vtxdgfval  16048  vtxedgfi  16049  vtxdg0v  16054  vtxdumgrfival  16058  wkslem1  16066  wkslem2  16067  wksfval  16068  iswlk  16069  uspgr2wlkeq  16111  uspgr2wlkeqi  16113  2wlklem  16120  trlsfvalg  16127  clwwlkg  16136  isclwwlk  16137  clwwlkccatlem  16143  clwwlkng  16148  clwwlkn2  16163  clwwlkext2edg  16164  umgr2cwwk2dif  16166  umgr2cwwkdifex  16167  012of  16444  2o01f  16445  subctctexmid  16453  nnsf  16459  nninfalllem1  16462  nninffeq  16474  qdencn  16483  trilpolemclim  16492  trilpolemcl  16493  trilpolemisumle  16494  trilpolemeq1  16496  trilpolemlt1  16497  trilpo  16499  iswomni0  16507  redcwlpo  16511  dceqnconst  16516  dcapnconst  16517  nconstwlpolemgt0  16520  nconstwlpolem  16521  nconstwlpo  16522  neapmkv  16524