Theorem fveq2 5693

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 4131	. . 3 |- ( A = B -> ( A F x <-> B F x ) )
2	1	iotabidv 5358	. 2 |- ( A = B -> ( iota x A F x ) = ( iota x B F x ) )
3		df-fv 5383	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5383	. 2 |- ( F ` B ) = ( iota x B F x )
5	2, 3, 4	3eqtr4g 2296	1 |- ( A = B -> ( F ` A ) = ( F ` B ) )

Syntax hints:   -> wi 4   = wceq 1402   class class class wbr 4128   iotacio 5333   ` cfv 5375

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3714  df-pr 3715  df-op 3717  df-uni 3934  df-br 4129  df-iota 5335  df-fv 5383

This theorem is referenced by:  fveq2i  5696  fveq2d  5697  2fveq3  5698  fvifdc  5715  dffn5imf  5755  fvelimab  5756  ssimaex  5761  fvco4  5774  fvmptssdm  5787  fvmptf  5795  eqfnfv2f  5804  fvelrn  5833  ralrnmpt  5844  rexrnmpt  5845  ffnfvf  5861  fmptco  5868  cofmpt  5871  fcompt  5872  fcoconst  5873  fsn2g  5877  fnressn  5895  fressnfv  5896  fconstfvm  5927  dfimafnf  5948  foco2  5952  funiunfvdmf  5963  f1veqaeq  5968  dff13f  5969  f1fveq  5971  f1elima  5972  f1ocnvfv  5978  f1ocnvfvb  5979  fcofo  5983  cocan2  5987  fliftfun  5995  isorel  6007  isocnv  6010  isotr  6015  f1oiso2  6026  canth  6029  imbrov2fvoveq  6103  ffnov  6185  eqfnov  6188  fnovim  6190  fnrnov  6228  foov  6229  funimassov  6232  ovelimab  6233  ofvalg  6305  ofrval  6306  offval2  6311  ofrfval2  6312  ofco  6314  caofinvl  6321  op1std  6375  op2ndd  6376  1stval2  6382  2ndval2  6383  unielxp  6401  reldm  6413  oprabco  6446  2ndconst  6451  f1o2ndf1  6457  elsuppfng  6475  elsuppfn  6476  mpoxopn0yelv  6503  mpoxopoveq  6504  smoel  6564  tfrlem1  6572  tfrlem3-2d  6576  tfrlem5  6578  tfrlem9  6583  tfr0dm  6586  tfrlemiubacc  6594  tfrlemi1  6596  tfrexlem  6598  tfr1onlemsucfn  6604  tfr1onlemsucaccv  6605  tfr1onlembxssdm  6607  tfr1onlembfn  6608  tfr1onlemubacc  6610  tfr1onlemaccex  6612  tfr1onlemres  6613  tfri1dALT  6615  tfrcllemsucfn  6617  tfrcllemsucaccv  6618  tfrcllembxssdm  6620  tfrcllembfn  6621  tfrcllemubacc  6623  tfrcllemaccex  6625  tfrcllemres  6626  tfrcldm  6627  tfrcl  6628  tfri3  6631  rdgtfr  6638  rdgss  6647  rdgisuc1  6648  rdgisucinc  6649  rdgon  6650  frecabex  6662  frecabcl  6663  frecfcllem  6668  frecsuclem  6670  frecsuc  6671  frecrdg  6672  oav  6720  omv  6721  oeiv  6722  fvixp  6978  cbvixp  6990  mptelixpg  7009  elixpsn  7010  dom2lem  7051  xpcomco  7117  xpmapen  7143  fidceq  7164  fieq0  7303  ordiso2  7368  djune  7411  updjudhcoinlf  7413  updjudhcoinrg  7414  updjud  7415  omp1eom  7428  0ct  7440  ctmlemr  7441  ctssdclemn0  7443  ctssdccl  7444  ctssdc  7446  enumctlemm  7447  nninfninc  7456  nnnninfeq  7461  nnnninfeq2  7462  enomnilem  7471  finomni  7473  fodjuomnilemdc  7477  fodju0  7480  fodjuomni  7482  ismkvnex  7488  fodjumkv  7493  nninfwlporlemd  7505  nninfwlpor  7507  exmidaclem  7557  cc1  7624  cc2lem  7625  cc2  7626  cc3  7627  mulpipq2  7731  genipv  7869  genpelxp  7871  addcanprleml  7974  addcanprlemu  7975  recexprlemm  7984  recexprlemdisj  7990  recexprlemloc  7991  recexprlem1ssl  7993  recexprlem1ssu  7994  cauappcvgprlemm  8005  cauappcvgprlemdisj  8011  cauappcvgprlemloc  8012  cauappcvgprlemladdru  8016  cauappcvgprlemladdrl  8017  cauappcvgprlem1  8019  cauappcvgprlem2  8020  cauappcvgprlemlim  8021  cauappcvgpr  8022  caucvgprlemnkj  8026  caucvgprlemnbj  8027  caucvgprlemm  8028  caucvgprlemdisj  8034  caucvgprlemloc  8035  caucvgprlemcl  8036  caucvgprlemladdfu  8037  caucvgprlemladdrl  8038  caucvgprlem1  8039  caucvgprlem2  8040  caucvgpr  8042  caucvgprprlemell  8045  caucvgprprlemelu  8046  caucvgprprlemcbv  8047  caucvgprprlemval  8048  caucvgprprlemnkeqj  8050  caucvgprprlemnbj  8053  caucvgprprlemml  8054  caucvgprprlemmu  8055  caucvgprprlemopl  8057  caucvgprprlemlol  8058  caucvgprprlemopu  8059  caucvgprprlemloc  8063  caucvgprprlemclphr  8065  caucvgprprlemexbt  8066  caucvgprprlem1  8069  caucvgprprlem2  8070  caucvgsrlemcl  8149  caucvgsrlemfv  8151  caucvgsrlembound  8154  caucvgsrlemgt1  8155  caucvgsrlemoffval  8156  caucvgsrlemoffres  8160  caucvgsrlembnd  8161  caucvgsr  8162  axcaucvglemcau  8258  axcaucvglemres  8259  uz11  9927  cnref1o  10033  fzprval  10470  fztpval  10471  zsupcllemex  10644  infssuzex  10647  suprzubdc  10652  frec2uzuzd  10820  frec2uzltd  10821  frec2uzlt2d  10822  frecuzrdgrrn  10826  frec2uzrdg  10827  frecuzrdgtcl  10830  frecuzrdgg  10834  frecuzrdgfunlem  10837  frecfzennn  10844  seqeq1  10868  iseqovex  10876  seq3val  10878  seqvalcd  10879  seq3-1  10880  seqf  10882  seq3p1  10883  seqovcd  10885  seqp1cd  10888  seq3clss  10889  seq3fveq2  10893  seqfveq2g  10895  seqfveqg  10896  seq3fveq  10897  seq3feq  10898  seq3shft2  10899  seqshft2g  10900  monoord  10903  monoord2  10904  ser3mono  10905  seq3split  10906  seqsplitg  10907  seq3caopr3  10909  seqcaopr3g  10910  seq3caopr2  10911  seqcaopr2g  10912  iseqf1olemkle  10915  iseqf1olemklt  10916  iseqf1olemqval  10918  iseqf1olemqk  10925  iseqf1olemjpcl  10926  iseqf1olemqpcl  10927  iseqf1olemfvp  10928  seq3f1olemqsumkj  10929  seq3f1olemqsum  10931  seq3f1olemstep  10932  seq3f1olemp  10933  seq3f1oleml  10934  seq3f1o  10935  seqf1oglem2a  10936  seqf1og  10939  seq3id2  10944  seq3homo  10945  seq3z  10946  seqhomog  10948  seqfeq4g  10949  ser3ge0  10954  ser3le  10955  exp3vallem  10958  exp3val  10959  facp1  11149  faccl  11154  facdiv  11157  facwordi  11159  faclbnd  11160  facubnd  11164  bcval  11168  bcval5  11182  fz1eqb  11210  omgadd  11223  hashxp  11248  hashmap  11249  hashfibc  11264  hashf1lem1  11266  hashf1lem2  11267  hashf1  11268  zfz1isolem1  11273  zfz1iso  11274  seq3coll  11275  eqwrd  11326  lswwrd  11332  lswex  11337  ccatfvalfi  11341  ccatval1  11346  ccatval2  11347  ccatalpha  11362  s1eq  11368  eqs1  11377  swrdval  11401  ccatopth2  11470  wrd2ind  11476  seq3shft  11584  reval  11595  replim  11605  cj11  11652  caucvgre  11728  cvg1nlemcau  11731  cvg1nlemres  11732  rexuz3  11737  absval  11748  resqrexlemover  11757  resqrexlemdecn  11759  resqrexlemlo  11760  resqrexlemcalc3  11763  resqrexlemnm  11765  resqrexlemcvg  11766  resqrexlemoverl  11768  resqrexlemglsq  11769  resqrexlemga  11770  resqrexlemsqa  11771  resqrexlemex  11772  abs00bd  11813  cau3lem  11861  caubnd2  11864  climconst  12037  climmpt  12047  climshftlemg  12049  climcn1  12055  climle  12081  climub  12091  climserle  12092  climcau  12094  climcvg1nlem  12096  climcvg1n  12097  serf0  12099  fsum3cvg  12126  summodclem3  12128  summodclem2a  12129  summodclem2  12130  summodc  12131  zsumdc  12132  fsum3  12135  fsumf1o  12138  fisumss  12140  fsum3cvg2  12142  fsum3ser  12145  fsumcl2lem  12146  fsumadd  12154  sumsnf  12157  isummulc2  12174  isumge0  12178  isumadd  12179  fsum2dlemstep  12182  fsummulc2  12196  fsumconst  12202  fsumrelem  12219  isumshft  12238  isum1p  12240  isumnn0nn  12241  isumrpcl  12242  isumlessdc  12244  cvgratnnlemnexp  12272  cvgratnnlemmn  12273  cvgratnnlemseq  12274  cvgratnnlemabsle  12275  cvgratnnlemfm  12277  cvgratnnlemrate  12278  cvgratnn  12279  cvgratz  12280  mertenslemi1  12283  mertenslem2  12284  mertensabs  12285  clim2prod  12287  prodfap0  12293  prodfrecap  12294  prodfdivap  12295  fproddccvg  12320  prodmodclem3  12323  prodmodclem2a  12324  prodmodclem2  12325  prodmodc  12326  zproddc  12327  fprodseq  12331  fprodf1o  12336  fprodssdc  12338  fprodmul  12339  prodsnf  12340  fprodfac  12363  fprodconst  12368  fprod2dlemstep  12370  eftvalcn  12405  ef0lem  12408  ege2le3  12419  efcj  12421  efaddlem  12422  eftlub  12438  efgt1p2  12443  reef11  12447  tanvalap  12456  efieq1re  12520  eirraplem  12525  dvdsabseq  12595  dvdsfac  12608  gcd0id  12737  nninfctlemfo  12798  nn0seqcvgd  12800  alginv  12806  algcvg  12807  algcvga  12810  algfx  12811  eucalglt  12816  lcmid  12839  qredeu  12856  prmfac1  12911  sqne2sq  12936  qnumdenbi  12951  dfphi2  12979  eulerthlemrprm  12988  eulerthlema  12989  eulerthlemh  12990  eulerthlemth  12991  phisum  13000  pcmpt  13103  pcfac  13110  1arithlem4  13126  elgz  13131  4sqlem4  13152  4sqlem12  13162  2expltfac  13199  ballotfilem2  13209  ballotfilemfc0  13213  ballotfilemfcc  13214  ballotfileme  13217  ballotfilemefi  13218  ballotfilemodife  13221  ballotfilem4  13222  ballotfilemi  13224  ballotfilemic  13231  ballotfilem1c  13232  ballotfilemrval  13242  ballotfilemrc  13255  ballotfilemrinv  13258  ballotfilemth  13262  ballotfi  13263  ennnfonelemk  13272  ennnfonelemp1  13278  ennnfoneleminc  13283  ennnfonelemkh  13284  ennnfonelemhf1o  13285  ennnfonelemex  13286  ennnfonelemhom  13287  ennnfonelemrn  13291  ennnfonelemnn0  13294  ennnfonelemr  13295  ennnfonelemim  13296  ctinfomlemom  13299  ctinfom  13300  ctiunctlemfo  13311  nninfdclemlt  13323  nninfdclemf1  13324  sloteq  13338  ressvalsets  13398  topnvalg  13585  imasex  13606  imasaddvallemg  13616  qusex  13626  xpsfrnel  13645  xpsfeq  13646  ismgm  13657  plusffvalg  13662  grpidvalg  13673  gzsumfzval  13691  gzsumval2  13694  issgrp  13698  ismnddef  13711  ismhm  13748  mhmex  13749  mhmlin  13754  issubm  13759  mhmeql  13779  isgrp  13791  grpn0  13820  grpinvfvalg  13827  grpsubfvalg  13830  grpsubval  13831  grpinv11  13854  grpinvnz  13856  mhmlem  13897  mulgfvalg  13904  mulgsubcl  13919  mulgaddcomlem  13928  mulgneg2  13939  mulgass  13942  issubg  13956  subgex  13959  issubg2m  13972  issubg4m  13976  0subg  13982  isnsg  13985  releqgg  14003  eqgex  14004  eqgval  14006  isghm  14026  ghmlin  14031  ghmrn  14040  ghmeql  14050  f1ghm0to0  14055  iscmn  14076  gsumconstcmn  14146  prdsbasprj  14162  prdsplusgfval  14164  prdsmulrfval  14166  prdsidlem  14173  prdsinvlem  14176  xpsval  14181  pws0g  14193  pwsinvg  14195  pwssub  14196  mgpvalg  14200  isrng  14211  issrg  14246  srgfcl  14254  isring  14281  iscrng  14284  mulgass2  14339  opprvalg  14350  dvdsrvald  14376  isunitd  14389  invrfvald  14405  dvrfvald  14416  dvrvald  14417  isrhm  14441  rhmval  14456  isnzr  14464  islring  14475  issubrng  14483  issubrg  14505  rrgval  14546  rrgsupp  14550  isdomn  14554  aprval  14567  aprap  14574  aprprop  14577  isdrngtap  14582  islmod  14603  scaffvalg  14618  lsssetm  14668  lspfval  14700  sraval  14749  rlmvalg  14766  2idlval  14814  2idlvalg  14815  cnfldmulg  14888  zlmval  14937  znf1o  14961  psrlinv  15001  mplsubgfilemcl  15016  istps  15059  clsfval  15128  cnpval  15225  lmconst  15243  txcnp  15298  upxp  15299  uptx  15301  txlm  15306  lmcn2  15307  cnmpt11  15310  cnmpt11f  15311  cnmpt1t  15312  cnmpt21  15318  cnmpt21f  15319  cnmpt2t  15320  mopnval  15469  isxms  15478  isms  15480  comet  15526  mopnex  15532  xmetxp  15534  xmetxpbl  15535  txmetcnp  15545  txmetcn  15546  qtopbasss  15548  cncfi  15605  cncfmpt1f  15625  ivthinclemlm  15661  ivthinclemum  15662  ivthinclemlopn  15663  ivthinclemlr  15664  ivthinclemuopn  15665  ivthinclemur  15666  ivthinclemdisj  15667  ivthinclemloc  15668  ivthinc  15670  ivthdec  15671  ivthreinc  15672  cnlimci  15700  limccnpcntop  15702  eldvap  15709  dvcoapbr  15734  dvcj  15736  dvfre  15737  dvmptcjx  15751  dveflem  15753  elply2  15762  elplyd  15768  plymullem1  15775  plyadd  15778  plymul  15779  plycoeid3  15784  plycolemc  15785  plyco  15786  plycjlemc  15787  plycj  15788  dvply1  15792  sin0pilem2  15809  pilem3  15810  coseq0q4123  15861  coseq0negpitopi  15863  cos11  15880  logltb  15901  logfac  15921  rpcxpef  15922  rplogbval  15973  pellexlem1  16008  pellexlem3  16010  mpodvdsmulf1o  16021  fsumdvdsmul  16022  zabsle1  16035  lgslem2  16037  lgslem3  16038  lgsfcl2  16042  lgsfle1  16045  lgsle1  16051  lgsdirprm  16070  lgseisenlem2  16107  lgsquadlem2  16114  2sqlem1  16150  2sqlem2  16151  mul2sq  16152  2sqlem3  16153  2sqlem9  16160  2sqlem10  16161  vtxvalg  16174  iedgvalg  16175  edgvalg  16217  edgopval  16220  edgstruct  16222  isuhgrm  16229  isushgrm  16230  isupgren  16253  isumgren  16263  isuspgren  16315  isusgren  16316  umgr2edg1  16367  usgredg2vlem1  16380  usgredg2vlem2  16381  ushgredgedg  16384  issubgr  16415  vtxdgfval  16446  vtxedgfi  16447  vtxdg0v  16452  vtxdumgrfival  16456  1loopgrvd0fi  16464  1hevtxdg0fi  16465  1hevtxdg1en  16466  wkslem1  16478  wkslem2  16479  wksfval  16480  iswlk  16481  uspgr2wlkeq  16523  uspgr2wlkeqi  16525  2wlklem  16534  trlsfvalg  16541  clwwlkg  16551  isclwwlk  16552  clwwlkccatlem  16558  clwwlkng  16563  clwwlkn2  16579  clwwlkext2edg  16580  umgr2cwwk2dif  16582  umgr2cwwkdifex  16583  clwwlknonmpo  16586  clwwlknonel  16590  clwwlknonex2lem2  16596  eupthsg  16603  iseupth  16605  eupthseg  16610  eupth2lem3lem3fi  16628  eupth2lem3lem6fi  16629  eupth2lem3lem4fi  16631  eupth2lem3fi  16634  eupth2lemsfi  16636  eupth2fi  16637  eulerpathprum  16638  konigsberglem4  16649  depindlem1  16664  depindlem2  16665  depindlem3  16666  012of  16940  2o01f  16941  subctctexmid  16947  nnsf  16956  nninfalllem1  16959  nninffeq  16971  qdencn  16980  trilpolemclim  16993  trilpolemcl  16994  trilpolemisumle  16995  trilpolemeq1  16997  trilpolemlt1  16998  trilpo  17000  iswomni0  17009  redcwlpo  17013  dceqnconst  17018  dcapnconst  17019  nconstwlpolemgt0  17022  nconstwlpolem  17023  nconstwlpo  17024  neapmkv  17026