Theorem fveq2 5695

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   class class class wbr 4130   iotacio 5335   ` cfv 5377

This proof depends on 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 proof 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 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385

This theorem is used by:  fveq2i  5698  fveq2d  5699  2fveq3  5700  fvifdc  5717  dffn5imf  5758  fvelimab  5759  ssimaex  5764  fvco4  5777  fvmptssdm  5790  fvmptf  5798  eqfnfv2f  5810  fvelrn  5839  ralrnmpt  5850  rexrnmpt  5851  ffnfvf  5867  fmptco  5874  cofmpt  5877  fcompt  5878  fcoconst  5879  fsn2g  5883  fnressn  5901  fressnfv  5902  fconstfvm  5933  dfimafnf  5955  foco2  5959  funiunfvdmf  5970  f1veqaeq  5975  dff13f  5976  f1fveq  5978  f1elima  5979  f1ocnvfv  5985  f1ocnvfvb  5986  fcofo  5990  cocan2  5994  fliftfun  6002  isorel  6014  isocnv  6017  isotr  6022  f1oiso2  6033  canth  6036  imbrov2fvoveq  6110  ffnov  6192  eqfnov  6195  fnovim  6197  fnrnov  6235  foov  6236  funimassov  6239  ovelimab  6240  ofvalg  6312  ofrval  6313  offval2  6318  ofrfval2  6319  ofco  6321  caofinvl  6328  op1std  6382  op2ndd  6383  1stval2  6389  2ndval2  6390  unielxp  6408  reldm  6420  oprabco  6453  2ndconst  6458  f1o2ndf1  6464  elsuppfng  6482  elsuppfn  6483  mpoxopn0yelv  6510  mpoxopoveq  6511  smoel  6571  tfrlem1  6579  tfrlem3-2d  6583  tfrlem5  6585  tfrlem9  6590  tfr0dm  6593  tfrlemiubacc  6601  tfrlemi1  6603  tfrexlem  6605  tfr1onlemsucfn  6611  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfr1onlemubacc  6617  tfr1onlemaccex  6619  tfr1onlemres  6620  tfri1dALT  6622  tfrcllemsucfn  6624  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemubacc  6630  tfrcllemaccex  6632  tfrcllemres  6633  tfrcldm  6634  tfrcl  6635  tfri3  6638  rdgtfr  6645  rdgss  6654  rdgisuc1  6655  rdgisucinc  6656  rdgon  6657  frecabex  6669  frecabcl  6670  frecfcllem  6675  frecsuclem  6677  frecsuc  6678  frecrdg  6679  oav  6727  omv  6728  oeiv  6729  fvixp  6985  cbvixp  6997  mptelixpg  7016  elixpsn  7017  dom2lem  7058  xpcomco  7124  xpmapen  7150  fidceq  7171  fieq0  7310  ordiso2  7375  djune  7418  updjudhcoinlf  7420  updjudhcoinrg  7421  updjud  7422  omp1eom  7435  0ct  7447  ctmlemr  7448  ctssdclemn0  7450  ctssdccl  7451  ctssdc  7453  enumctlemm  7454  nninfninc  7463  nnnninfeq  7468  nnnninfeq2  7469  enomnilem  7478  finomni  7480  fodjuomnilemdc  7484  fodju0  7487  fodjuomni  7489  ismkvnex  7495  fodjumkv  7500  nninfwlporlemd  7512  nninfwlpor  7514  exmidaclem  7564  cc1  7631  cc2lem  7632  cc2  7633  cc3  7634  mulpipq2  7738  genipv  7876  genpelxp  7878  addcanprleml  7981  addcanprlemu  7982  recexprlemm  7991  recexprlemdisj  7997  recexprlemloc  7998  recexprlem1ssl  8000  recexprlem1ssu  8001  cauappcvgprlemm  8012  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem1  8026  cauappcvgprlem2  8027  cauappcvgprlemlim  8028  cauappcvgpr  8029  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemm  8035  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprlemcl  8043  caucvgprlemladdfu  8044  caucvgprlemladdrl  8045  caucvgprlem1  8046  caucvgprlem2  8047  caucvgpr  8049  caucvgprprlemell  8052  caucvgprprlemelu  8053  caucvgprprlemcbv  8054  caucvgprprlemval  8055  caucvgprprlemnkeqj  8057  caucvgprprlemnbj  8060  caucvgprprlemml  8061  caucvgprprlemmu  8062  caucvgprprlemopl  8064  caucvgprprlemlol  8065  caucvgprprlemopu  8066  caucvgprprlemloc  8070  caucvgprprlemclphr  8072  caucvgprprlemexbt  8073  caucvgprprlem1  8076  caucvgprprlem2  8077  caucvgsrlemcl  8156  caucvgsrlemfv  8158  caucvgsrlembound  8161  caucvgsrlemgt1  8162  caucvgsrlemoffval  8163  caucvgsrlemoffres  8167  caucvgsrlembnd  8168  caucvgsr  8169  axcaucvglemcau  8265  axcaucvglemres  8266  uz11  9945  cnref1o  10051  fzprval  10489  fztpval  10490  zsupcllemex  10663  infssuzex  10666  suprzubdc  10671  frec2uzuzd  10839  frec2uzltd  10840  frec2uzlt2d  10841  frecuzrdgrrn  10845  frec2uzrdg  10846  frecuzrdgtcl  10849  frecuzrdgg  10853  frecuzrdgfunlem  10856  frecfzennn  10863  seqeq1  10887  iseqovex  10895  seq3val  10897  seqvalcd  10898  seq3-1  10899  seqf  10901  seq3p1  10902  seqovcd  10904  seqp1cd  10907  seq3clss  10908  seq3fveq2  10912  seqfveq2g  10914  seqfveqg  10915  seq3fveq  10916  seq3feq  10917  seq3shft2  10918  seqshft2g  10919  monoord  10922  monoord2  10923  ser3mono  10924  seq3split  10925  seqsplitg  10926  seq3caopr3  10928  seqcaopr3g  10929  seq3caopr2  10930  seqcaopr2g  10931  iseqf1olemkle  10934  iseqf1olemklt  10935  iseqf1olemqval  10937  iseqf1olemqk  10944  iseqf1olemjpcl  10945  iseqf1olemqpcl  10946  iseqf1olemfvp  10947  seq3f1olemqsumkj  10948  seq3f1olemqsum  10950  seq3f1olemstep  10951  seq3f1olemp  10952  seq3f1oleml  10953  seq3f1o  10954  seqf1oglem2a  10955  seqf1og  10958  seq3id2  10963  seq3homo  10964  seq3z  10965  seqhomog  10967  seqfeq4g  10968  ser3ge0  10973  ser3le  10974  exp3vallem  10977  exp3val  10978  facp1  11168  faccl  11173  facdiv  11176  facwordi  11178  faclbnd  11179  facubnd  11183  bcval  11187  bcval5  11201  fz1eqb  11229  omgadd  11242  hashxp  11267  hashmap  11268  hashfibc  11283  hashf1lem1  11285  hashf1lem2  11286  hashf1  11287  zfz1isolem1  11292  zfz1iso  11293  seq3coll  11294  eqwrd  11345  lswwrd  11351  lswex  11356  ccatfvalfi  11360  ccatval1  11365  ccatval2  11366  ccatalpha  11381  s1eq  11387  eqs1  11396  swrdval  11420  ccatopth2  11489  wrd2ind  11495  seq3shft  11603  reval  11614  replim  11624  cj11  11671  caucvgre  11747  cvg1nlemcau  11750  cvg1nlemres  11751  rexuz3  11756  absval  11767  resqrexlemover  11776  resqrexlemdecn  11778  resqrexlemlo  11779  resqrexlemcalc3  11782  resqrexlemnm  11784  resqrexlemcvg  11785  resqrexlemoverl  11787  resqrexlemglsq  11788  resqrexlemga  11789  resqrexlemsqa  11790  resqrexlemex  11791  abs00bd  11832  cau3lem  11880  caubnd2  11883  climconst  12056  climmpt  12066  climshftlemg  12068  climcn1  12074  climle  12100  climub  12110  climserle  12111  climcau  12113  climcvg1nlem  12115  climcvg1n  12116  serf0  12118  fsum3cvg  12145  summodclem3  12147  summodclem2a  12148  summodclem2  12149  summodc  12150  zsumdc  12151  fsum3  12154  fsumf1o  12157  fisumss  12159  fsum3cvg2  12161  fsum3ser  12164  fsumcl2lem  12165  fsumadd  12173  sumsnf  12176  isummulc2  12193  isumge0  12197  isumadd  12198  fsum2dlemstep  12201  fsummulc2  12215  fsumconst  12221  fsumrelem  12238  isumshft  12257  isum1p  12259  isumnn0nn  12260  isumrpcl  12261  isumlessdc  12263  cvgratnnlemnexp  12291  cvgratnnlemmn  12292  cvgratnnlemseq  12293  cvgratnnlemabsle  12294  cvgratnnlemfm  12296  cvgratnnlemrate  12297  cvgratnn  12298  cvgratz  12299  mertenslemi1  12302  mertenslem2  12303  mertensabs  12304  clim2prod  12306  prodfap0  12312  prodfrecap  12313  prodfdivap  12314  fproddccvg  12339  prodmodclem3  12342  prodmodclem2a  12343  prodmodclem2  12344  prodmodc  12345  zproddc  12346  fprodseq  12350  fprodf1o  12355  fprodssdc  12357  fprodmul  12358  prodsnf  12359  fprodfac  12382  fprodconst  12387  fprod2dlemstep  12389  eftvalcn  12424  ef0lem  12427  ege2le3  12438  efcj  12440  efaddlem  12441  eftlub  12457  efgt1p2  12462  reef11  12466  tanvalap  12475  efieq1re  12539  eirraplem  12544  dvdsabseq  12614  dvdsfac  12627  gcd0id  12756  nninfctlemfo  12817  nn0seqcvgd  12819  alginv  12825  algcvg  12826  algcvga  12829  algfx  12830  eucalglt  12835  lcmid  12858  qredeu  12875  prmfac1  12930  sqne2sq  12955  qnumdenbi  12970  dfphi2  12998  eulerthlemrprm  13007  eulerthlema  13008  eulerthlemh  13009  eulerthlemth  13010  phisum  13019  pcmpt  13122  pcfac  13129  1arithlem4  13145  elgz  13150  4sqlem4  13171  4sqlem12  13181  2expltfac  13218  ballotfilem2  13228  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfileme  13236  ballotfilemefi  13237  ballotfilemodife  13240  ballotfilem4  13241  ballotfilemi  13243  ballotfilemic  13250  ballotfilem1c  13251  ballotfilemrval  13261  ballotfilemrc  13274  ballotfilemrinv  13277  ballotfilemth  13281  ballotfi  13282  ennnfonelemk  13291  ennnfonelemp1  13297  ennnfoneleminc  13302  ennnfonelemkh  13303  ennnfonelemhf1o  13304  ennnfonelemex  13305  ennnfonelemhom  13306  ennnfonelemrn  13310  ennnfonelemnn0  13313  ennnfonelemr  13314  ennnfonelemim  13315  ctinfomlemom  13318  ctinfom  13319  ctiunctlemfo  13330  nninfdclemlt  13342  nninfdclemf1  13343  sloteq  13357  ressvalsets  13418  topnvalg  13605  imasex  13626  imasaddvallemg  13636  qusex  13646  xpsfrnel  13665  xpsfeq  13666  ismgm  13677  plusffvalg  13682  grpidvalg  13693  gzsumfzval  13711  gzsumval2  13714  issgrp  13718  ismnddef  13731  ismhm  13768  mhmex  13769  mhmlin  13774  issubm  13779  mhmeql  13799  isgrp  13811  grpn0  13840  grpinvfvalg  13847  grpsubfvalg  13850  grpsubval  13851  grpinv11  13874  grpinvnz  13876  mhmlem  13917  mulgfvalg  13924  mulgsubcl  13939  mulgaddcomlem  13948  mulgneg2  13959  mulgass  13962  issubg  13976  subgex  13979  issubg2m  13992  issubg4m  13996  0subg  14002  isnsg  14005  releqgg  14023  eqgex  14024  eqgval  14026  isghm  14046  ghmlin  14051  ghmrn  14060  ghmeql  14070  f1ghm0to0  14075  iscmn  14096  gsumconstcmn  14166  prdsbasprj  14182  prdsplusgfval  14184  prdsmulrfval  14186  prdsidlem  14193  prdsinvlem  14196  xpsval  14201  pws0g  14213  pwsinvg  14215  pwssub  14216  mgpvalg  14220  isrng  14233  issrg  14269  srgfcl  14277  isring  14304  iscrng  14307  mulgass2  14363  opprvalg  14374  dvdsrvald  14400  isunitd  14413  invrfvald  14429  dvrfvald  14440  dvrvald  14441  isrhm  14465  rhmval  14480  isnzr  14488  islring  14499  issubrng  14507  issubrg  14529  rrgval  14570  rrgsupp  14574  isdomn  14578  aprval  14591  aprap  14598  aprprop  14601  isdrngtap  14606  islmod  14627  scaffvalg  14643  lsssetm  14693  lspfval  14725  sraval  14774  rlmvalg  14791  2idlval  14839  2idlvalg  14840  cnfldmulg  14913  zlmval  14962  znf1o  14986  isassa  15002  aspval  15015  asclfval  15021  psrlinv  15075  mplsubgfilemcl  15090  istps  15133  clsfval  15202  cnpval  15299  lmconst  15317  txcnp  15372  upxp  15373  uptx  15375  txlm  15380  lmcn2  15381  cnmpt11  15384  cnmpt11f  15385  cnmpt1t  15386  cnmpt21  15392  cnmpt21f  15393  cnmpt2t  15394  mopnval  15543  isxms  15552  isms  15554  comet  15600  mopnex  15606  xmetxp  15608  xmetxpbl  15609  txmetcnp  15619  txmetcn  15620  qtopbasss  15622  cncfi  15679  cncfmpt1f  15699  ivthinclemlm  15735  ivthinclemum  15736  ivthinclemlopn  15737  ivthinclemlr  15738  ivthinclemuopn  15739  ivthinclemur  15740  ivthinclemdisj  15741  ivthinclemloc  15742  ivthinc  15744  ivthdec  15745  ivthreinc  15746  cnlimci  15774  limccnpcntop  15776  eldvap  15783  dvcoapbr  15808  dvcj  15810  dvfre  15811  dvmptcjx  15825  dveflem  15827  elply2  15836  elplyd  15842  plymullem1  15849  plyadd  15852  plymul  15853  plycoeid3  15858  plycolemc  15859  plyco  15860  plycjlemc  15861  plycj  15862  dvply1  15866  sin0pilem2  15883  pilem3  15884  coseq0q4123  15935  coseq0negpitopi  15937  cos11  15954  logltb  15975  logfac  15995  rpcxpef  15996  rplogbval  16047  pellexlem1  16091  pellexlem3  16093  mpodvdsmulf1o  16104  fsumdvdsmul  16105  zabsle1  16118  lgslem2  16120  lgslem3  16121  lgsfcl2  16125  lgsfle1  16128  lgsle1  16134  lgsdirprm  16153  lgseisenlem2  16190  lgsquadlem2  16197  2sqlem1  16233  2sqlem2  16234  mul2sq  16235  2sqlem3  16236  2sqlem9  16243  2sqlem10  16244  vtxvalg  16257  iedgvalg  16258  edgvalg  16300  edgopval  16303  edgstruct  16305  isuhgrm  16312  isushgrm  16313  isupgren  16336  isumgren  16346  isuspgren  16398  isusgren  16399  umgr2edg1  16450  usgredg2vlem1  16463  usgredg2vlem2  16464  ushgredgedg  16467  issubgr  16498  vtxdgfval  16529  vtxedgfi  16530  vtxdg0v  16535  vtxdumgrfival  16539  1loopgrvd0fi  16547  1hevtxdg0fi  16548  1hevtxdg1en  16549  wkslem1  16561  wkslem2  16562  wksfval  16563  iswlk  16564  uspgr2wlkeq  16606  uspgr2wlkeqi  16608  2wlklem  16617  trlsfvalg  16624  clwwlkg  16634  isclwwlk  16635  clwwlkccatlem  16641  clwwlkng  16646  clwwlkn2  16662  clwwlkext2edg  16663  umgr2cwwk2dif  16665  umgr2cwwkdifex  16666  clwwlknonmpo  16669  clwwlknonel  16673  clwwlknonex2lem2  16679  eupthsg  16686  iseupth  16688  eupthseg  16693  eupth2lem3lem3fi  16711  eupth2lem3lem6fi  16712  eupth2lem3lem4fi  16714  eupth2lem3fi  16717  eupth2lemsfi  16719  eupth2fi  16720  eulerpathprum  16721  konigsberglem4  16732  depindlem1  16747  depindlem2  16748  depindlem3  16749  012of  17023  2o01f  17024  subctctexmid  17030  nnsf  17048  nninfalllem1  17051  nninffeq  17063  qdencn  17072  trilpolemclim  17085  trilpolemcl  17086  trilpolemisumle  17087  trilpolemeq1  17089  trilpolemlt1  17090  trilpo  17092  iswomni0  17101  redcwlpo  17105  dceqnconst  17110  dcapnconst  17111  nconstwlpolemgt0  17114  nconstwlpolem  17115  nconstwlpo  17116  neapmkv  17118