Theorem fveq2 5661

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

Syntax hints:   -> wi 4   = wceq 1398   class class class wbr 4102   iotacio 5301   ` cfv 5343

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-v 2814  df-un 3214  df-sn 3688  df-pr 3689  df-op 3691  df-uni 3908  df-br 4103  df-iota 5303  df-fv 5351

This theorem is referenced by:  fveq2i  5664  fveq2d  5665  2fveq3  5666  fvifdc  5683  dffn5imf  5723  fvelimab  5724  ssimaex  5729  fvco4  5740  fvmptssdm  5753  fvmptf  5761  eqfnfv2f  5770  fvelrn  5799  ralrnmpt  5810  rexrnmpt  5811  ffnfvf  5827  fmptco  5834  cofmpt  5837  fcompt  5838  fcoconst  5839  fsn2g  5843  fnressn  5861  fressnfv  5862  fconstfvm  5893  foco2  5917  funiunfvdmf  5928  f1veqaeq  5933  dff13f  5934  f1fveq  5936  f1elima  5937  f1ocnvfv  5943  f1ocnvfvb  5944  fcofo  5948  cocan2  5952  fliftfun  5960  isorel  5972  isocnv  5975  isotr  5980  f1oiso2  5991  canth  5992  imbrov2fvoveq  6066  ffnov  6148  eqfnov  6151  fnovim  6153  fnrnov  6191  foov  6192  funimassov  6195  ovelimab  6196  ofvalg  6267  ofrval  6268  offval2  6273  ofrfval2  6274  ofco  6276  caofinvl  6283  op1std  6333  op2ndd  6334  1stval2  6340  2ndval2  6341  unielxp  6359  reldm  6371  oprabco  6404  2ndconst  6409  f1o2ndf1  6415  elsuppfng  6433  elsuppfn  6434  mpoxopn0yelv  6461  mpoxopoveq  6462  smoel  6522  tfrlem1  6530  tfrlem3-2d  6534  tfrlem5  6536  tfrlem9  6541  tfr0dm  6544  tfrlemiubacc  6552  tfrlemi1  6554  tfrexlem  6556  tfr1onlemsucfn  6562  tfr1onlemsucaccv  6563  tfr1onlembxssdm  6565  tfr1onlembfn  6566  tfr1onlemubacc  6568  tfr1onlemaccex  6570  tfr1onlemres  6571  tfri1dALT  6573  tfrcllemsucfn  6575  tfrcllemsucaccv  6576  tfrcllembxssdm  6578  tfrcllembfn  6579  tfrcllemubacc  6581  tfrcllemaccex  6583  tfrcllemres  6584  tfrcldm  6585  tfrcl  6586  tfri3  6589  rdgtfr  6596  rdgss  6605  rdgisuc1  6606  rdgisucinc  6607  rdgon  6608  frecabex  6620  frecabcl  6621  frecfcllem  6626  frecsuclem  6628  frecsuc  6629  frecrdg  6630  oav  6678  omv  6679  oeiv  6680  fvixp  6929  cbvixp  6941  mptelixpg  6960  elixpsn  6961  dom2lem  7002  xpcomco  7068  xpmapen  7094  fidceq  7115  fieq0  7254  ordiso2  7317  djune  7360  updjudhcoinlf  7362  updjudhcoinrg  7363  updjud  7364  omp1eom  7377  0ct  7389  ctmlemr  7390  ctssdclemn0  7392  ctssdccl  7393  ctssdc  7395  enumctlemm  7396  nninfninc  7405  nnnninfeq  7410  nnnninfeq2  7411  enomnilem  7420  finomni  7422  fodjuomnilemdc  7426  fodju0  7429  fodjuomni  7431  ismkvnex  7437  fodjumkv  7442  nninfwlporlemd  7454  nninfwlpor  7456  exmidaclem  7506  cc1  7567  cc2lem  7568  cc2  7569  cc3  7570  mulpipq2  7674  genipv  7812  genpelxp  7814  addcanprleml  7917  addcanprlemu  7918  recexprlemm  7927  recexprlemdisj  7933  recexprlemloc  7934  recexprlem1ssl  7936  recexprlem1ssu  7937  cauappcvgprlemm  7948  cauappcvgprlemdisj  7954  cauappcvgprlemloc  7955  cauappcvgprlemladdru  7959  cauappcvgprlemladdrl  7960  cauappcvgprlem1  7962  cauappcvgprlem2  7963  cauappcvgprlemlim  7964  cauappcvgpr  7965  caucvgprlemnkj  7969  caucvgprlemnbj  7970  caucvgprlemm  7971  caucvgprlemdisj  7977  caucvgprlemloc  7978  caucvgprlemcl  7979  caucvgprlemladdfu  7980  caucvgprlemladdrl  7981  caucvgprlem1  7982  caucvgprlem2  7983  caucvgpr  7985  caucvgprprlemell  7988  caucvgprprlemelu  7989  caucvgprprlemcbv  7990  caucvgprprlemval  7991  caucvgprprlemnkeqj  7993  caucvgprprlemnbj  7996  caucvgprprlemml  7997  caucvgprprlemmu  7998  caucvgprprlemopl  8000  caucvgprprlemlol  8001  caucvgprprlemopu  8002  caucvgprprlemloc  8006  caucvgprprlemclphr  8008  caucvgprprlemexbt  8009  caucvgprprlem1  8012  caucvgprprlem2  8013  caucvgsrlemcl  8092  caucvgsrlemfv  8094  caucvgsrlembound  8097  caucvgsrlemgt1  8098  caucvgsrlemoffval  8099  caucvgsrlemoffres  8103  caucvgsrlembnd  8104  caucvgsr  8105  axcaucvglemcau  8201  axcaucvglemres  8202  uz11  9863  cnref1o  9969  fzprval  10402  fztpval  10403  zsupcllemex  10576  infssuzex  10579  suprzubdc  10582  frec2uzuzd  10750  frec2uzltd  10751  frec2uzlt2d  10752  frecuzrdgrrn  10756  frec2uzrdg  10757  frecuzrdgtcl  10760  frecuzrdgg  10764  frecuzrdgfunlem  10767  frecfzennn  10774  seqeq1  10798  iseqovex  10806  seq3val  10808  seqvalcd  10809  seq3-1  10810  seqf  10812  seq3p1  10813  seqovcd  10815  seqp1cd  10818  seq3clss  10819  seq3fveq2  10823  seqfveq2g  10825  seqfveqg  10826  seq3fveq  10827  seq3feq  10828  seq3shft2  10829  seqshft2g  10830  monoord  10833  monoord2  10834  ser3mono  10835  seq3split  10836  seqsplitg  10837  seq3caopr3  10839  seqcaopr3g  10840  seq3caopr2  10841  seqcaopr2g  10842  iseqf1olemkle  10845  iseqf1olemklt  10846  iseqf1olemqval  10848  iseqf1olemqk  10855  iseqf1olemjpcl  10856  iseqf1olemqpcl  10857  iseqf1olemfvp  10858  seq3f1olemqsumkj  10859  seq3f1olemqsum  10861  seq3f1olemstep  10862  seq3f1olemp  10863  seq3f1oleml  10864  seq3f1o  10865  seqf1oglem2a  10866  seqf1og  10869  seq3id2  10874  seq3homo  10875  seq3z  10876  seqhomog  10878  seqfeq4g  10879  ser3ge0  10884  ser3le  10885  exp3vallem  10888  exp3val  10889  facp1  11078  faccl  11083  facdiv  11086  facwordi  11088  faclbnd  11089  facubnd  11093  bcval  11097  bcval5  11111  fz1eqb  11138  omgadd  11151  hashxp  11176  zfz1isolem1  11190  zfz1iso  11191  seq3coll  11192  eqwrd  11243  lswwrd  11249  lswex  11254  ccatfvalfi  11258  ccatval1  11263  ccatval2  11264  ccatalpha  11279  s1eq  11285  eqs1  11294  swrdval  11318  ccatopth2  11387  wrd2ind  11393  seq3shft  11501  reval  11512  replim  11522  cj11  11568  caucvgre  11644  cvg1nlemcau  11647  cvg1nlemres  11648  rexuz3  11653  absval  11664  resqrexlemover  11673  resqrexlemdecn  11675  resqrexlemlo  11676  resqrexlemcalc3  11679  resqrexlemnm  11681  resqrexlemcvg  11682  resqrexlemoverl  11684  resqrexlemglsq  11685  resqrexlemga  11686  resqrexlemsqa  11687  resqrexlemex  11688  abs00bd  11729  cau3lem  11777  caubnd2  11780  climconst  11953  climmpt  11963  climshftlemg  11965  climcn1  11971  climle  11997  climub  12007  climserle  12008  climcau  12010  climcvg1nlem  12012  climcvg1n  12013  serf0  12015  fsum3cvg  12042  summodclem3  12044  summodclem2a  12045  summodclem2  12046  summodc  12047  zsumdc  12048  fsum3  12051  fsumf1o  12054  fisumss  12056  fsum3cvg2  12058  fsum3ser  12061  fsumcl2lem  12062  fsumadd  12070  sumsnf  12073  isummulc2  12090  isumge0  12094  isumadd  12095  fsum2dlemstep  12098  fsummulc2  12112  fsumconst  12118  fsumrelem  12135  isumshft  12154  isum1p  12156  isumnn0nn  12157  isumrpcl  12158  isumlessdc  12160  cvgratnnlemnexp  12188  cvgratnnlemmn  12189  cvgratnnlemseq  12190  cvgratnnlemabsle  12191  cvgratnnlemfm  12193  cvgratnnlemrate  12194  cvgratnn  12195  cvgratz  12196  mertenslemi1  12199  mertenslem2  12200  mertensabs  12201  clim2prod  12203  prodfap0  12209  prodfrecap  12210  prodfdivap  12211  fproddccvg  12236  prodmodclem3  12239  prodmodclem2a  12240  prodmodclem2  12241  prodmodc  12242  zproddc  12243  fprodseq  12247  fprodf1o  12252  fprodssdc  12254  fprodmul  12255  prodsnf  12256  fprodfac  12279  fprodconst  12284  fprod2dlemstep  12286  eftvalcn  12321  ef0lem  12324  ege2le3  12335  efcj  12337  efaddlem  12338  eftlub  12354  efgt1p2  12359  reef11  12363  tanvalap  12372  efieq1re  12436  eirraplem  12441  dvdsabseq  12511  dvdsfac  12524  gcd0id  12653  nninfctlemfo  12714  nn0seqcvgd  12716  alginv  12722  algcvg  12723  algcvga  12726  algfx  12727  eucalglt  12732  lcmid  12755  qredeu  12772  prmfac1  12827  sqne2sq  12852  qnumdenbi  12867  dfphi2  12895  eulerthlemrprm  12904  eulerthlema  12905  eulerthlemh  12906  eulerthlemth  12907  phisum  12916  pcmpt  13019  pcfac  13026  1arithlem4  13042  elgz  13047  4sqlem4  13068  4sqlem12  13078  2expltfac  13115  ennnfonelemk  13125  ennnfonelemp1  13131  ennnfoneleminc  13136  ennnfonelemkh  13137  ennnfonelemhf1o  13138  ennnfonelemex  13139  ennnfonelemhom  13140  ennnfonelemrn  13144  ennnfonelemnn0  13147  ennnfonelemr  13148  ennnfonelemim  13149  ctinfomlemom  13152  ctinfom  13153  ctiunctlemfo  13164  nninfdclemlt  13176  nninfdclemf1  13177  sloteq  13191  ressvalsets  13251  topnvalg  13438  prdsbasprj  13469  prdsplusgfval  13471  prdsmulrfval  13473  imasex  13492  imasaddvallemg  13502  qusex  13512  xpsfrnel  13531  xpsfeq  13532  xpsval  13539  ismgm  13544  plusffvalg  13549  grpidvalg  13560  gsumfzval  13578  gsumval2  13584  issgrp  13590  ismnddef  13605  prdsidlem  13634  pws0g  13638  ismhm  13648  mhmex  13649  mhmlin  13654  issubm  13659  mhmeql  13679  isgrp  13693  grpn0  13722  grpinvfvalg  13729  grpsubfvalg  13732  grpsubval  13733  grpinv11  13756  grpinvnz  13758  prdsinvlem  13795  pwsinvg  13799  pwssub  13800  mhmlem  13805  mulgfvalg  13812  mulgsubcl  13827  mulgaddcomlem  13836  mulgneg2  13847  mulgass  13850  issubg  13864  subgex  13867  issubg2m  13880  issubg4m  13884  0subg  13890  isnsg  13893  releqgg  13911  eqgex  13912  eqgval  13914  isghm  13934  ghmlin  13939  ghmrn  13948  ghmeql  13958  f1ghm0to0  13963  iscmn  13984  mgpvalg  14041  isrng  14052  issrg  14083  srgfcl  14091  isring  14118  iscrng  14121  mulgass2  14176  opprvalg  14187  dvdsrvald  14212  isunitd  14225  invrfvald  14241  dvrfvald  14252  dvrvald  14253  isrhm  14277  rhmval  14292  isnzr  14300  islring  14311  issubrng  14318  issubrg  14340  rrgval  14381  rrgsupp  14385  isdomn  14389  aprval  14402  aprap  14406  islmod  14411  scaffvalg  14426  lsssetm  14476  lspfval  14508  sraval  14557  rlmvalg  14574  2idlval  14622  2idlvalg  14623  cnfldmulg  14696  zlmval  14747  znf1o  14771  psrlinv  14809  mplsubgfilemcl  14824  istps  14867  clsfval  14936  cnpval  15033  lmconst  15051  txcnp  15106  upxp  15107  uptx  15109  txlm  15114  lmcn2  15115  cnmpt11  15118  cnmpt11f  15119  cnmpt1t  15120  cnmpt21  15126  cnmpt21f  15127  cnmpt2t  15128  mopnval  15277  isxms  15286  isms  15288  comet  15334  mopnex  15340  xmetxp  15342  xmetxpbl  15343  txmetcnp  15353  txmetcn  15354  qtopbasss  15356  cncfi  15413  cncfmpt1f  15433  ivthinclemlm  15469  ivthinclemum  15470  ivthinclemlopn  15471  ivthinclemlr  15472  ivthinclemuopn  15473  ivthinclemur  15474  ivthinclemdisj  15475  ivthinclemloc  15476  ivthinc  15478  ivthdec  15479  ivthreinc  15480  cnlimci  15508  limccnpcntop  15510  eldvap  15517  dvcoapbr  15542  dvcj  15544  dvfre  15545  dvmptcjx  15559  dveflem  15561  elply2  15570  elplyd  15576  plymullem1  15583  plyadd  15586  plymul  15587  plycoeid3  15592  plycolemc  15593  plyco  15594  plycjlemc  15595  plycj  15596  dvply1  15600  sin0pilem2  15617  pilem3  15618  coseq0q4123  15669  coseq0negpitopi  15671  cos11  15688  logltb  15709  rpcxpef  15729  rplogbval  15780  pellexlem1  15815  pellexlem3  15817  mpodvdsmulf1o  15828  fsumdvdsmul  15829  zabsle1  15842  lgslem2  15844  lgslem3  15845  lgsfcl2  15849  lgsfle1  15852  lgsle1  15858  lgsdirprm  15877  lgseisenlem2  15914  lgsquadlem2  15921  2sqlem1  15957  2sqlem2  15958  mul2sq  15959  2sqlem3  15960  2sqlem9  15967  2sqlem10  15968  vtxvalg  15981  iedgvalg  15982  edgvalg  16024  edgopval  16027  edgstruct  16029  isuhgrm  16036  isushgrm  16037  isupgren  16060  isumgren  16070  isuspgren  16122  isusgren  16123  umgr2edg1  16174  usgredg2vlem1  16187  usgredg2vlem2  16188  ushgredgedg  16191  issubgr  16222  vtxdgfval  16253  vtxedgfi  16254  vtxdg0v  16259  vtxdumgrfival  16263  1loopgrvd0fi  16271  1hevtxdg0fi  16272  1hevtxdg1en  16273  wkslem1  16285  wkslem2  16286  wksfval  16287  iswlk  16288  uspgr2wlkeq  16330  uspgr2wlkeqi  16332  2wlklem  16341  trlsfvalg  16348  clwwlkg  16358  isclwwlk  16359  clwwlkccatlem  16365  clwwlkng  16370  clwwlkn2  16386  clwwlkext2edg  16387  umgr2cwwk2dif  16389  umgr2cwwkdifex  16390  clwwlknonmpo  16393  clwwlknonel  16397  clwwlknonex2lem2  16403  eupthsg  16410  iseupth  16412  eupthseg  16417  eupth2lem3lem3fi  16435  eupth2lem3lem6fi  16436  eupth2lem3lem4fi  16438  eupth2lem3fi  16441  eupth2lemsfi  16443  eupth2fi  16444  eulerpathprum  16445  konigsberglem4  16456  depindlem1  16471  depindlem2  16472  depindlem3  16473  012of  16737  2o01f  16738  subctctexmid  16744  nnsf  16753  nninfalllem1  16756  nninffeq  16768  qdencn  16777  trilpolemclim  16790  trilpolemcl  16791  trilpolemisumle  16792  trilpolemeq1  16794  trilpolemlt1  16795  trilpo  16797  iswomni0  16806  redcwlpo  16810  dceqnconst  16815  dcapnconst  16816  nconstwlpolemgt0  16819  nconstwlpolem  16820  nconstwlpo  16821  neapmkv  16823