Theorem fveq2 5578

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 4048	. . 3 |- ( A = B -> ( A F x <-> B F x ) )
2	1	iotabidv 5255	. 2 |- ( A = B -> ( iota x A F x ) = ( iota x B F x ) )
3		df-fv 5280	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5280	. 2 |- ( F ` B ) = ( iota x B F x )
5	2, 3, 4	3eqtr4g 2263	1 |- ( A = B -> ( F ` A ) = ( F ` B ) )

Syntax hints:   -> wi 4   = wceq 1373   class class class wbr 4045   iotacio 5231   ` cfv 5272

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4046  df-iota 5233  df-fv 5280

This theorem is referenced by:  fveq2i  5581  fveq2d  5582  2fveq3  5583  fvifdc  5600  dffn5imf  5636  fvelimab  5637  ssimaex  5642  fvco4  5653  fvmptssdm  5666  fvmptf  5674  eqfnfv2f  5683  fvelrn  5713  ralrnmpt  5724  rexrnmpt  5725  ffnfvf  5741  fmptco  5748  cofmpt  5751  fcompt  5752  fcoconst  5753  fnressn  5772  fressnfv  5773  fconstfvm  5804  foco2  5824  funiunfvdmf  5835  f1veqaeq  5840  dff13f  5841  f1fveq  5843  f1elima  5844  f1ocnvfv  5850  f1ocnvfvb  5851  fcofo  5855  cocan2  5859  fliftfun  5867  isorel  5879  isocnv  5882  isotr  5887  f1oiso2  5898  canth  5899  imbrov2fvoveq  5971  ffnov  6051  eqfnov  6054  fnovim  6056  fnrnov  6094  foov  6095  funimassov  6098  ovelimab  6099  suppssfv  6156  ofvalg  6170  ofrval  6171  offval2  6176  ofrfval2  6177  ofco  6179  caofinvl  6186  op1std  6236  op2ndd  6237  1stval2  6243  2ndval2  6244  unielxp  6262  reldm  6274  oprabco  6305  2ndconst  6310  f1o2ndf1  6316  mpoxopn0yelv  6327  mpoxopoveq  6328  smoel  6388  tfrlem1  6396  tfrlem3-2d  6400  tfrlem5  6402  tfrlem9  6407  tfr0dm  6410  tfrlemiubacc  6418  tfrlemi1  6420  tfrexlem  6422  tfr1onlemsucfn  6428  tfr1onlemsucaccv  6429  tfr1onlembxssdm  6431  tfr1onlembfn  6432  tfr1onlemubacc  6434  tfr1onlemaccex  6436  tfr1onlemres  6437  tfri1dALT  6439  tfrcllemsucfn  6441  tfrcllemsucaccv  6442  tfrcllembxssdm  6444  tfrcllembfn  6445  tfrcllemubacc  6447  tfrcllemaccex  6449  tfrcllemres  6450  tfrcldm  6451  tfrcl  6452  tfri3  6455  rdgtfr  6462  rdgss  6471  rdgisuc1  6472  rdgisucinc  6473  rdgon  6474  frecabex  6486  frecabcl  6487  frecfcllem  6492  frecsuclem  6494  frecsuc  6495  frecrdg  6496  oav  6542  omv  6543  oeiv  6544  fvixp  6792  cbvixp  6804  mptelixpg  6823  elixpsn  6824  dom2lem  6865  xpcomco  6923  xpmapen  6949  fidceq  6968  fieq0  7080  ordiso2  7139  djune  7182  updjudhcoinlf  7184  updjudhcoinrg  7185  updjud  7186  omp1eom  7199  0ct  7211  ctmlemr  7212  ctssdclemn0  7214  ctssdccl  7215  ctssdc  7217  enumctlemm  7218  nninfninc  7227  nnnninfeq  7232  nnnninfeq2  7233  enomnilem  7242  finomni  7244  fodjuomnilemdc  7248  fodju0  7251  fodjuomni  7253  ismkvnex  7259  fodjumkv  7264  nninfwlporlemd  7276  nninfwlpor  7278  exmidaclem  7322  cc1  7379  cc2lem  7380  cc2  7381  cc3  7382  mulpipq2  7486  genipv  7624  genpelxp  7626  addcanprleml  7729  addcanprlemu  7730  recexprlemm  7739  recexprlemdisj  7745  recexprlemloc  7746  recexprlem1ssl  7748  recexprlem1ssu  7749  cauappcvgprlemm  7760  cauappcvgprlemdisj  7766  cauappcvgprlemloc  7767  cauappcvgprlemladdru  7771  cauappcvgprlemladdrl  7772  cauappcvgprlem1  7774  cauappcvgprlem2  7775  cauappcvgprlemlim  7776  cauappcvgpr  7777  caucvgprlemnkj  7781  caucvgprlemnbj  7782  caucvgprlemm  7783  caucvgprlemdisj  7789  caucvgprlemloc  7790  caucvgprlemcl  7791  caucvgprlemladdfu  7792  caucvgprlemladdrl  7793  caucvgprlem1  7794  caucvgprlem2  7795  caucvgpr  7797  caucvgprprlemell  7800  caucvgprprlemelu  7801  caucvgprprlemcbv  7802  caucvgprprlemval  7803  caucvgprprlemnkeqj  7805  caucvgprprlemnbj  7808  caucvgprprlemml  7809  caucvgprprlemmu  7810  caucvgprprlemopl  7812  caucvgprprlemlol  7813  caucvgprprlemopu  7814  caucvgprprlemloc  7818  caucvgprprlemclphr  7820  caucvgprprlemexbt  7821  caucvgprprlem1  7824  caucvgprprlem2  7825  caucvgsrlemcl  7904  caucvgsrlemfv  7906  caucvgsrlembound  7909  caucvgsrlemgt1  7910  caucvgsrlemoffval  7911  caucvgsrlemoffres  7915  caucvgsrlembnd  7916  caucvgsr  7917  axcaucvglemcau  8013  axcaucvglemres  8014  uz11  9673  cnref1o  9774  fzprval  10206  fztpval  10207  zsupcllemex  10375  infssuzex  10378  suprzubdc  10381  frec2uzuzd  10549  frec2uzltd  10550  frec2uzlt2d  10551  frecuzrdgrrn  10555  frec2uzrdg  10556  frecuzrdgtcl  10559  frecuzrdgg  10563  frecuzrdgfunlem  10566  frecfzennn  10573  seqeq1  10597  iseqovex  10605  seq3val  10607  seqvalcd  10608  seq3-1  10609  seqf  10611  seq3p1  10612  seqovcd  10614  seqp1cd  10617  seq3clss  10618  seq3fveq2  10622  seqfveq2g  10624  seqfveqg  10625  seq3fveq  10626  seq3feq  10627  seq3shft2  10628  seqshft2g  10629  monoord  10632  monoord2  10633  ser3mono  10634  seq3split  10635  seqsplitg  10636  seq3caopr3  10638  seqcaopr3g  10639  seq3caopr2  10640  seqcaopr2g  10641  iseqf1olemkle  10644  iseqf1olemklt  10645  iseqf1olemqval  10647  iseqf1olemqk  10654  iseqf1olemjpcl  10655  iseqf1olemqpcl  10656  iseqf1olemfvp  10657  seq3f1olemqsumkj  10658  seq3f1olemqsum  10660  seq3f1olemstep  10661  seq3f1olemp  10662  seq3f1oleml  10663  seq3f1o  10664  seqf1oglem2a  10665  seqf1og  10668  seq3id2  10673  seq3homo  10674  seq3z  10675  seqhomog  10677  seqfeq4g  10678  ser3ge0  10683  ser3le  10684  exp3vallem  10687  exp3val  10688  facp1  10877  faccl  10882  facdiv  10885  facwordi  10887  faclbnd  10888  facubnd  10892  bcval  10896  bcval5  10910  fz1eqb  10937  omgadd  10949  hashxp  10973  zfz1isolem1  10987  zfz1iso  10988  seq3coll  10989  eqwrd  11036  lswwrd  11042  lswex  11047  ccatfvalfi  11051  ccatval1  11056  ccatval2  11057  s1eq  11076  eqs1  11085  swrdval  11104  seq3shft  11182  reval  11193  replim  11203  cj11  11249  caucvgre  11325  cvg1nlemcau  11328  cvg1nlemres  11329  rexuz3  11334  absval  11345  resqrexlemover  11354  resqrexlemdecn  11356  resqrexlemlo  11357  resqrexlemcalc3  11360  resqrexlemnm  11362  resqrexlemcvg  11363  resqrexlemoverl  11365  resqrexlemglsq  11366  resqrexlemga  11367  resqrexlemsqa  11368  resqrexlemex  11369  abs00bd  11410  cau3lem  11458  caubnd2  11461  climconst  11634  climmpt  11644  climshftlemg  11646  climcn1  11652  climle  11678  climub  11688  climserle  11689  climcau  11691  climcvg1nlem  11693  climcvg1n  11694  serf0  11696  fsum3cvg  11722  summodclem3  11724  summodclem2a  11725  summodclem2  11726  summodc  11727  zsumdc  11728  fsum3  11731  fsumf1o  11734  fisumss  11736  fsum3cvg2  11738  fsum3ser  11741  fsumcl2lem  11742  fsumadd  11750  sumsnf  11753  isummulc2  11770  isumge0  11774  isumadd  11775  fsum2dlemstep  11778  fsummulc2  11792  fsumconst  11798  fsumrelem  11815  isumshft  11834  isum1p  11836  isumnn0nn  11837  isumrpcl  11838  isumlessdc  11840  cvgratnnlemnexp  11868  cvgratnnlemmn  11869  cvgratnnlemseq  11870  cvgratnnlemabsle  11871  cvgratnnlemfm  11873  cvgratnnlemrate  11874  cvgratnn  11875  cvgratz  11876  mertenslemi1  11879  mertenslem2  11880  mertensabs  11881  clim2prod  11883  prodfap0  11889  prodfrecap  11890  prodfdivap  11891  fproddccvg  11916  prodmodclem3  11919  prodmodclem2a  11920  prodmodclem2  11921  prodmodc  11922  zproddc  11923  fprodseq  11927  fprodf1o  11932  fprodssdc  11934  fprodmul  11935  prodsnf  11936  fprodfac  11959  fprodconst  11964  fprod2dlemstep  11966  eftvalcn  12001  ef0lem  12004  ege2le3  12015  efcj  12017  efaddlem  12018  eftlub  12034  efgt1p2  12039  reef11  12043  tanvalap  12052  efieq1re  12116  eirraplem  12121  dvdsabseq  12191  dvdsfac  12204  gcd0id  12333  nninfctlemfo  12394  nn0seqcvgd  12396  alginv  12402  algcvg  12403  algcvga  12406  algfx  12407  eucalglt  12412  lcmid  12435  qredeu  12452  prmfac1  12507  sqne2sq  12532  qnumdenbi  12547  dfphi2  12575  eulerthlemrprm  12584  eulerthlema  12585  eulerthlemh  12586  eulerthlemth  12587  phisum  12596  pcmpt  12699  pcfac  12706  1arithlem4  12722  elgz  12727  4sqlem4  12748  4sqlem12  12758  2expltfac  12795  ennnfonelemk  12804  ennnfonelemp1  12810  ennnfoneleminc  12815  ennnfonelemkh  12816  ennnfonelemhf1o  12817  ennnfonelemex  12818  ennnfonelemhom  12819  ennnfonelemrn  12823  ennnfonelemnn0  12826  ennnfonelemr  12827  ennnfonelemim  12828  ctinfomlemom  12831  ctinfom  12832  ctiunctlemfo  12843  nninfdclemlt  12855  nninfdclemf1  12856  sloteq  12870  ressvalsets  12929  topnvalg  13116  prdsbasprj  13147  prdsplusgfval  13149  prdsmulrfval  13151  imasex  13170  imasaddvallemg  13180  qusex  13190  xpsfrnel  13209  xpsfeq  13210  xpsval  13217  ismgm  13222  plusffvalg  13227  grpidvalg  13238  gsumfzval  13256  gsumval2  13262  issgrp  13268  ismnddef  13283  prdsidlem  13312  pws0g  13316  ismhm  13326  mhmex  13327  mhmlin  13332  issubm  13337  mhmeql  13357  isgrp  13371  grpn0  13400  grpinvfvalg  13407  grpsubfvalg  13410  grpsubval  13411  grpinv11  13434  grpinvnz  13436  prdsinvlem  13473  pwsinvg  13477  pwssub  13478  mhmlem  13483  mulgfvalg  13490  mulgsubcl  13505  mulgaddcomlem  13514  mulgneg2  13525  mulgass  13528  issubg  13542  subgex  13545  issubg2m  13558  issubg4m  13562  0subg  13568  isnsg  13571  releqgg  13589  eqgex  13590  eqgval  13592  isghm  13612  ghmlin  13617  ghmrn  13626  ghmeql  13636  f1ghm0to0  13641  iscmn  13662  mgpvalg  13718  isrng  13729  issrg  13760  srgfcl  13768  isring  13795  iscrng  13798  mulgass2  13853  opprvalg  13864  reldvdsrsrg  13887  dvdsrvald  13888  isunitd  13901  invrfvald  13917  dvrfvald  13928  dvrvald  13929  isrhm  13953  rhmval  13968  isnzr  13976  islring  13987  issubrng  13994  issubrg  14016  rrgval  14057  isdomn  14064  aprval  14077  aprap  14081  islmod  14086  scaffvalg  14101  lsssetm  14151  lspfval  14183  sraval  14232  rlmvalg  14249  2idlval  14297  2idlvalg  14298  cnfldmulg  14371  zlmval  14422  znf1o  14446  psrlinv  14479  mplsubgfilemcl  14494  istps  14537  clsfval  14606  cnpval  14703  lmconst  14721  txcnp  14776  upxp  14777  uptx  14779  txlm  14784  lmcn2  14785  cnmpt11  14788  cnmpt11f  14789  cnmpt1t  14790  cnmpt21  14796  cnmpt21f  14797  cnmpt2t  14798  mopnval  14947  isxms  14956  isms  14958  comet  15004  mopnex  15010  xmetxp  15012  xmetxpbl  15013  txmetcnp  15023  txmetcn  15024  qtopbasss  15026  cncfi  15083  cncfmpt1f  15103  ivthinclemlm  15139  ivthinclemum  15140  ivthinclemlopn  15141  ivthinclemlr  15142  ivthinclemuopn  15143  ivthinclemur  15144  ivthinclemdisj  15145  ivthinclemloc  15146  ivthinc  15148  ivthdec  15149  ivthreinc  15150  cnlimci  15178  limccnpcntop  15180  eldvap  15187  dvcoapbr  15212  dvcj  15214  dvfre  15215  dvmptcjx  15229  dveflem  15231  elply2  15240  elplyd  15246  plymullem1  15253  plyadd  15256  plymul  15257  plycoeid3  15262  plycolemc  15263  plyco  15264  plycjlemc  15265  plycj  15266  dvply1  15270  sin0pilem2  15287  pilem3  15288  coseq0q4123  15339  coseq0negpitopi  15341  cos11  15358  logltb  15379  rpcxpef  15399  rplogbval  15450  mpodvdsmulf1o  15495  fsumdvdsmul  15496  zabsle1  15509  lgslem2  15511  lgslem3  15512  lgsfcl2  15516  lgsfle1  15519  lgsle1  15525  lgsdirprm  15544  lgseisenlem2  15581  lgsquadlem2  15588  2sqlem1  15624  2sqlem2  15625  mul2sq  15626  2sqlem3  15627  2sqlem9  15634  2sqlem10  15635  vtxvalg  15648  iedgvalg  15649  edgvalg  15687  edgopval  15689  edgstruct  15691  012of  15967  2o01f  15968  subctctexmid  15974  nnsf  15979  nninfalllem1  15982  nninffeq  15994  qdencn  16003  trilpolemclim  16012  trilpolemcl  16013  trilpolemisumle  16014  trilpolemeq1  16016  trilpolemlt1  16017  trilpo  16019  iswomni0  16027  redcwlpo  16031  dceqnconst  16036  dcapnconst  16037  nconstwlpolemgt0  16040  nconstwlpolem  16041  nconstwlpo  16042  neapmkv  16044