Theorem fveq2 5672

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 4114	. . 3 |- ( A = B -> ( A F x <-> B F x ) )
2	1	iotabidv 5337	. 2 |- ( A = B -> ( iota x A F x ) = ( iota x B F x ) )
3		df-fv 5362	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5362	. 2 |- ( F ` B ) = ( iota x B F x )
5	2, 3, 4	3eqtr4g 2292	1 |- ( A = B -> ( F ` A ) = ( F ` B ) )

Syntax hints:   -> wi 4   = wceq 1398   class class class wbr 4111   iotacio 5312   ` cfv 5354

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 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-v 2817  df-un 3217  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-br 4112  df-iota 5314  df-fv 5362

This theorem is referenced by:  fveq2i  5675  fveq2d  5676  2fveq3  5677  fvifdc  5694  dffn5imf  5734  fvelimab  5735  ssimaex  5740  fvco4  5751  fvmptssdm  5764  fvmptf  5772  eqfnfv2f  5781  fvelrn  5810  ralrnmpt  5821  rexrnmpt  5822  ffnfvf  5838  fmptco  5845  cofmpt  5848  fcompt  5849  fcoconst  5850  fsn2g  5854  fnressn  5872  fressnfv  5873  fconstfvm  5904  foco2  5928  funiunfvdmf  5939  f1veqaeq  5944  dff13f  5945  f1fveq  5947  f1elima  5948  f1ocnvfv  5954  f1ocnvfvb  5955  fcofo  5959  cocan2  5963  fliftfun  5971  isorel  5983  isocnv  5986  isotr  5991  f1oiso2  6002  canth  6003  imbrov2fvoveq  6077  ffnov  6159  eqfnov  6162  fnovim  6164  fnrnov  6202  foov  6203  funimassov  6206  ovelimab  6207  ofvalg  6278  ofrval  6279  offval2  6284  ofrfval2  6285  ofco  6287  caofinvl  6294  op1std  6344  op2ndd  6345  1stval2  6351  2ndval2  6352  unielxp  6370  reldm  6382  oprabco  6415  2ndconst  6420  f1o2ndf1  6426  elsuppfng  6444  elsuppfn  6445  mpoxopn0yelv  6472  mpoxopoveq  6473  smoel  6533  tfrlem1  6541  tfrlem3-2d  6545  tfrlem5  6547  tfrlem9  6552  tfr0dm  6555  tfrlemiubacc  6563  tfrlemi1  6565  tfrexlem  6567  tfr1onlemsucfn  6573  tfr1onlemsucaccv  6574  tfr1onlembxssdm  6576  tfr1onlembfn  6577  tfr1onlemubacc  6579  tfr1onlemaccex  6581  tfr1onlemres  6582  tfri1dALT  6584  tfrcllemsucfn  6586  tfrcllemsucaccv  6587  tfrcllembxssdm  6589  tfrcllembfn  6590  tfrcllemubacc  6592  tfrcllemaccex  6594  tfrcllemres  6595  tfrcldm  6596  tfrcl  6597  tfri3  6600  rdgtfr  6607  rdgss  6616  rdgisuc1  6617  rdgisucinc  6618  rdgon  6619  frecabex  6631  frecabcl  6632  frecfcllem  6637  frecsuclem  6639  frecsuc  6640  frecrdg  6641  oav  6689  omv  6690  oeiv  6691  fvixp  6940  cbvixp  6952  mptelixpg  6971  elixpsn  6972  dom2lem  7013  xpcomco  7079  xpmapen  7105  fidceq  7126  fieq0  7265  ordiso2  7328  djune  7371  updjudhcoinlf  7373  updjudhcoinrg  7374  updjud  7375  omp1eom  7388  0ct  7400  ctmlemr  7401  ctssdclemn0  7403  ctssdccl  7404  ctssdc  7406  enumctlemm  7407  nninfninc  7416  nnnninfeq  7421  nnnninfeq2  7422  enomnilem  7431  finomni  7433  fodjuomnilemdc  7437  fodju0  7440  fodjuomni  7442  ismkvnex  7448  fodjumkv  7453  nninfwlporlemd  7465  nninfwlpor  7467  exmidaclem  7517  cc1  7581  cc2lem  7582  cc2  7583  cc3  7584  mulpipq2  7688  genipv  7826  genpelxp  7828  addcanprleml  7931  addcanprlemu  7932  recexprlemm  7941  recexprlemdisj  7947  recexprlemloc  7948  recexprlem1ssl  7950  recexprlem1ssu  7951  cauappcvgprlemm  7962  cauappcvgprlemdisj  7968  cauappcvgprlemloc  7969  cauappcvgprlemladdru  7973  cauappcvgprlemladdrl  7974  cauappcvgprlem1  7976  cauappcvgprlem2  7977  cauappcvgprlemlim  7978  cauappcvgpr  7979  caucvgprlemnkj  7983  caucvgprlemnbj  7984  caucvgprlemm  7985  caucvgprlemdisj  7991  caucvgprlemloc  7992  caucvgprlemcl  7993  caucvgprlemladdfu  7994  caucvgprlemladdrl  7995  caucvgprlem1  7996  caucvgprlem2  7997  caucvgpr  7999  caucvgprprlemell  8002  caucvgprprlemelu  8003  caucvgprprlemcbv  8004  caucvgprprlemval  8005  caucvgprprlemnkeqj  8007  caucvgprprlemnbj  8010  caucvgprprlemml  8011  caucvgprprlemmu  8012  caucvgprprlemopl  8014  caucvgprprlemlol  8015  caucvgprprlemopu  8016  caucvgprprlemloc  8020  caucvgprprlemclphr  8022  caucvgprprlemexbt  8023  caucvgprprlem1  8026  caucvgprprlem2  8027  caucvgsrlemcl  8106  caucvgsrlemfv  8108  caucvgsrlembound  8111  caucvgsrlemgt1  8112  caucvgsrlemoffval  8113  caucvgsrlemoffres  8117  caucvgsrlembnd  8118  caucvgsr  8119  axcaucvglemcau  8215  axcaucvglemres  8216  uz11  9880  cnref1o  9986  fzprval  10420  fztpval  10421  zsupcllemex  10594  infssuzex  10597  suprzubdc  10600  frec2uzuzd  10768  frec2uzltd  10769  frec2uzlt2d  10770  frecuzrdgrrn  10774  frec2uzrdg  10775  frecuzrdgtcl  10778  frecuzrdgg  10782  frecuzrdgfunlem  10785  frecfzennn  10792  seqeq1  10816  iseqovex  10824  seq3val  10826  seqvalcd  10827  seq3-1  10828  seqf  10830  seq3p1  10831  seqovcd  10833  seqp1cd  10836  seq3clss  10837  seq3fveq2  10841  seqfveq2g  10843  seqfveqg  10844  seq3fveq  10845  seq3feq  10846  seq3shft2  10847  seqshft2g  10848  monoord  10851  monoord2  10852  ser3mono  10853  seq3split  10854  seqsplitg  10855  seq3caopr3  10857  seqcaopr3g  10858  seq3caopr2  10859  seqcaopr2g  10860  iseqf1olemkle  10863  iseqf1olemklt  10864  iseqf1olemqval  10866  iseqf1olemqk  10873  iseqf1olemjpcl  10874  iseqf1olemqpcl  10875  iseqf1olemfvp  10876  seq3f1olemqsumkj  10877  seq3f1olemqsum  10879  seq3f1olemstep  10880  seq3f1olemp  10881  seq3f1oleml  10882  seq3f1o  10883  seqf1oglem2a  10884  seqf1og  10887  seq3id2  10892  seq3homo  10893  seq3z  10894  seqhomog  10896  seqfeq4g  10897  ser3ge0  10902  ser3le  10903  exp3vallem  10906  exp3val  10907  facp1  11096  faccl  11101  facdiv  11104  facwordi  11106  faclbnd  11107  facubnd  11111  bcval  11115  bcval5  11129  fz1eqb  11157  omgadd  11170  hashxp  11195  hashmap  11196  hashfibc  11211  zfz1isolem1  11216  zfz1iso  11217  seq3coll  11218  eqwrd  11269  lswwrd  11275  lswex  11280  ccatfvalfi  11284  ccatval1  11289  ccatval2  11290  ccatalpha  11305  s1eq  11311  eqs1  11320  swrdval  11344  ccatopth2  11413  wrd2ind  11419  seq3shft  11527  reval  11538  replim  11548  cj11  11594  caucvgre  11670  cvg1nlemcau  11673  cvg1nlemres  11674  rexuz3  11679  absval  11690  resqrexlemover  11699  resqrexlemdecn  11701  resqrexlemlo  11702  resqrexlemcalc3  11705  resqrexlemnm  11707  resqrexlemcvg  11708  resqrexlemoverl  11710  resqrexlemglsq  11711  resqrexlemga  11712  resqrexlemsqa  11713  resqrexlemex  11714  abs00bd  11755  cau3lem  11803  caubnd2  11806  climconst  11979  climmpt  11989  climshftlemg  11991  climcn1  11997  climle  12023  climub  12033  climserle  12034  climcau  12036  climcvg1nlem  12038  climcvg1n  12039  serf0  12041  fsum3cvg  12068  summodclem3  12070  summodclem2a  12071  summodclem2  12072  summodc  12073  zsumdc  12074  fsum3  12077  fsumf1o  12080  fisumss  12082  fsum3cvg2  12084  fsum3ser  12087  fsumcl2lem  12088  fsumadd  12096  sumsnf  12099  isummulc2  12116  isumge0  12120  isumadd  12121  fsum2dlemstep  12124  fsummulc2  12138  fsumconst  12144  fsumrelem  12161  isumshft  12180  isum1p  12182  isumnn0nn  12183  isumrpcl  12184  isumlessdc  12186  cvgratnnlemnexp  12214  cvgratnnlemmn  12215  cvgratnnlemseq  12216  cvgratnnlemabsle  12217  cvgratnnlemfm  12219  cvgratnnlemrate  12220  cvgratnn  12221  cvgratz  12222  mertenslemi1  12225  mertenslem2  12226  mertensabs  12227  clim2prod  12229  prodfap0  12235  prodfrecap  12236  prodfdivap  12237  fproddccvg  12262  prodmodclem3  12265  prodmodclem2a  12266  prodmodclem2  12267  prodmodc  12268  zproddc  12269  fprodseq  12273  fprodf1o  12278  fprodssdc  12280  fprodmul  12281  prodsnf  12282  fprodfac  12305  fprodconst  12310  fprod2dlemstep  12312  eftvalcn  12347  ef0lem  12350  ege2le3  12361  efcj  12363  efaddlem  12364  eftlub  12380  efgt1p2  12385  reef11  12389  tanvalap  12398  efieq1re  12462  eirraplem  12467  dvdsabseq  12537  dvdsfac  12550  gcd0id  12679  nninfctlemfo  12740  nn0seqcvgd  12742  alginv  12748  algcvg  12749  algcvga  12752  algfx  12753  eucalglt  12758  lcmid  12781  qredeu  12798  prmfac1  12853  sqne2sq  12878  qnumdenbi  12893  dfphi2  12921  eulerthlemrprm  12930  eulerthlema  12931  eulerthlemh  12932  eulerthlemth  12933  phisum  12942  pcmpt  13045  pcfac  13052  1arithlem4  13068  elgz  13073  4sqlem4  13094  4sqlem12  13104  2expltfac  13141  ballotfilem2  13149  ballotfilemfc0  13153  ballotfilemfcc  13154  ballotfileme  13157  ballotfilemodife  13158  ballotfilem4  13159  ennnfonelemk  13168  ennnfonelemp1  13174  ennnfoneleminc  13179  ennnfonelemkh  13180  ennnfonelemhf1o  13181  ennnfonelemex  13182  ennnfonelemhom  13183  ennnfonelemrn  13187  ennnfonelemnn0  13190  ennnfonelemr  13191  ennnfonelemim  13192  ctinfomlemom  13195  ctinfom  13196  ctiunctlemfo  13207  nninfdclemlt  13219  nninfdclemf1  13220  sloteq  13234  ressvalsets  13294  topnvalg  13481  prdsbasprj  13512  prdsplusgfval  13514  prdsmulrfval  13516  imasex  13535  imasaddvallemg  13545  qusex  13555  xpsfrnel  13574  xpsfeq  13575  xpsval  13582  ismgm  13587  plusffvalg  13592  grpidvalg  13603  gsumfzval  13621  gsumval2  13627  issgrp  13633  ismnddef  13648  prdsidlem  13677  pws0g  13681  ismhm  13691  mhmex  13692  mhmlin  13697  issubm  13702  mhmeql  13722  isgrp  13736  grpn0  13765  grpinvfvalg  13772  grpsubfvalg  13775  grpsubval  13776  grpinv11  13799  grpinvnz  13801  prdsinvlem  13838  pwsinvg  13842  pwssub  13843  mhmlem  13848  mulgfvalg  13855  mulgsubcl  13870  mulgaddcomlem  13879  mulgneg2  13890  mulgass  13893  issubg  13907  subgex  13910  issubg2m  13923  issubg4m  13927  0subg  13933  isnsg  13936  releqgg  13954  eqgex  13955  eqgval  13957  isghm  13977  ghmlin  13982  ghmrn  13991  ghmeql  14001  f1ghm0to0  14006  iscmn  14027  mgpvalg  14084  isrng  14095  issrg  14126  srgfcl  14134  isring  14161  iscrng  14164  mulgass2  14219  opprvalg  14230  dvdsrvald  14255  isunitd  14268  invrfvald  14284  dvrfvald  14295  dvrvald  14296  isrhm  14320  rhmval  14335  isnzr  14343  islring  14354  issubrng  14361  issubrg  14383  rrgval  14424  rrgsupp  14428  isdomn  14432  aprval  14445  aprap  14449  islmod  14456  scaffvalg  14471  lsssetm  14521  lspfval  14553  sraval  14602  rlmvalg  14619  2idlval  14667  2idlvalg  14668  cnfldmulg  14741  zlmval  14792  znf1o  14816  psrlinv  14856  mplsubgfilemcl  14871  istps  14914  clsfval  14983  cnpval  15080  lmconst  15098  txcnp  15153  upxp  15154  uptx  15156  txlm  15161  lmcn2  15162  cnmpt11  15165  cnmpt11f  15166  cnmpt1t  15167  cnmpt21  15173  cnmpt21f  15174  cnmpt2t  15175  mopnval  15324  isxms  15333  isms  15335  comet  15381  mopnex  15387  xmetxp  15389  xmetxpbl  15390  txmetcnp  15400  txmetcn  15401  qtopbasss  15403  cncfi  15460  cncfmpt1f  15480  ivthinclemlm  15516  ivthinclemum  15517  ivthinclemlopn  15518  ivthinclemlr  15519  ivthinclemuopn  15520  ivthinclemur  15521  ivthinclemdisj  15522  ivthinclemloc  15523  ivthinc  15525  ivthdec  15526  ivthreinc  15527  cnlimci  15555  limccnpcntop  15557  eldvap  15564  dvcoapbr  15589  dvcj  15591  dvfre  15592  dvmptcjx  15606  dveflem  15608  elply2  15617  elplyd  15623  plymullem1  15630  plyadd  15633  plymul  15634  plycoeid3  15639  plycolemc  15640  plyco  15641  plycjlemc  15642  plycj  15643  dvply1  15647  sin0pilem2  15664  pilem3  15665  coseq0q4123  15716  coseq0negpitopi  15718  cos11  15735  logltb  15756  rpcxpef  15776  rplogbval  15827  pellexlem1  15862  pellexlem3  15864  mpodvdsmulf1o  15875  fsumdvdsmul  15876  zabsle1  15889  lgslem2  15891  lgslem3  15892  lgsfcl2  15896  lgsfle1  15899  lgsle1  15905  lgsdirprm  15924  lgseisenlem2  15961  lgsquadlem2  15968  2sqlem1  16004  2sqlem2  16005  mul2sq  16006  2sqlem3  16007  2sqlem9  16014  2sqlem10  16015  vtxvalg  16028  iedgvalg  16029  edgvalg  16071  edgopval  16074  edgstruct  16076  isuhgrm  16083  isushgrm  16084  isupgren  16107  isumgren  16117  isuspgren  16169  isusgren  16170  umgr2edg1  16221  usgredg2vlem1  16234  usgredg2vlem2  16235  ushgredgedg  16238  issubgr  16269  vtxdgfval  16300  vtxedgfi  16301  vtxdg0v  16306  vtxdumgrfival  16310  1loopgrvd0fi  16318  1hevtxdg0fi  16319  1hevtxdg1en  16320  wkslem1  16332  wkslem2  16333  wksfval  16334  iswlk  16335  uspgr2wlkeq  16377  uspgr2wlkeqi  16379  2wlklem  16388  trlsfvalg  16395  clwwlkg  16405  isclwwlk  16406  clwwlkccatlem  16412  clwwlkng  16417  clwwlkn2  16433  clwwlkext2edg  16434  umgr2cwwk2dif  16436  umgr2cwwkdifex  16437  clwwlknonmpo  16440  clwwlknonel  16444  clwwlknonex2lem2  16450  eupthsg  16457  iseupth  16459  eupthseg  16464  eupth2lem3lem3fi  16482  eupth2lem3lem6fi  16483  eupth2lem3lem4fi  16485  eupth2lem3fi  16488  eupth2lemsfi  16490  eupth2fi  16491  eulerpathprum  16492  konigsberglem4  16503  depindlem1  16518  depindlem2  16519  depindlem3  16520  012of  16784  2o01f  16785  subctctexmid  16791  nnsf  16800  nninfalllem1  16803  nninffeq  16815  qdencn  16824  trilpolemclim  16837  trilpolemcl  16838  trilpolemisumle  16839  trilpolemeq1  16841  trilpolemlt1  16842  trilpo  16844  iswomni0  16853  redcwlpo  16857  dceqnconst  16863  dcapnconst  16864  nconstwlpolemgt0  16867  nconstwlpolem  16868  nconstwlpo  16869  neapmkv  16871