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  9954  cnref1o  10061  fzprval  10499  fztpval  10500  zsupcllemex  10673  infssuzex  10676  suprzubdc  10681  frec2uzuzd  10852  frec2uzltd  10853  frec2uzlt2d  10854  frecuzrdgrrn  10858  frec2uzrdg  10859  frecuzrdgtcl  10862  frecuzrdgg  10866  frecuzrdgfunlem  10869  frecfzennn  10876  seqeq1  10900  iseqovex  10908  seq3val  10910  seqvalcd  10911  seq3-1  10912  seqf  10914  seq3p1  10915  seqovcd  10917  seqp1cd  10920  seq3clss  10921  seq3fveq2  10925  seqfveq2g  10927  seqfveqg  10928  seq3fveq  10929  seq3feq  10930  seq3shft2  10931  seqshft2g  10932  monoord  10935  monoord2  10936  ser3mono  10937  seq3split  10938  seqsplitg  10939  seq3caopr3  10941  seqcaopr3g  10942  seq3caopr2  10943  seqcaopr2g  10944  iseqf1olemkle  10947  iseqf1olemklt  10948  iseqf1olemqval  10950  iseqf1olemqk  10957  iseqf1olemjpcl  10958  iseqf1olemqpcl  10959  iseqf1olemfvp  10960  seq3f1olemqsumkj  10961  seq3f1olemqsum  10963  seq3f1olemstep  10964  seq3f1olemp  10965  seq3f1oleml  10966  seq3f1o  10967  seqf1oglem2a  10968  seqf1og  10971  seq3id2  10976  seq3homo  10977  seq3z  10978  seqhomog  10980  seqfeq4g  10981  ser3ge0  10986  ser3le  10987  exp3vallem  10990  exp3val  10991  facp1  11182  faccl  11187  facdiv  11190  facwordi  11192  faclbnd  11193  facubnd  11197  bcval  11201  bcval5  11215  fz1eqb  11243  omgadd  11256  hashxp  11281  hashmap  11282  hashfibc  11297  hashf1lem1  11299  hashf1lem2  11300  hashf1  11301  zfz1isolem1  11306  zfz1iso  11307  seq3coll  11308  eqwrd  11359  lswwrd  11365  lswex  11370  ccatfvalfi  11374  ccatval1  11379  ccatval2  11380  ccatalpha  11395  s1eq  11401  eqs1  11410  swrdval  11434  ccatopth2  11503  wrd2ind  11509  seq3shft  11617  reval  11628  replim  11638  cj11  11685  caucvgre  11761  cvg1nlemcau  11764  cvg1nlemres  11765  rexuz3  11770  absval  11781  resqrexlemover  11790  resqrexlemdecn  11792  resqrexlemlo  11793  resqrexlemcalc3  11796  resqrexlemnm  11798  resqrexlemcvg  11799  resqrexlemoverl  11801  resqrexlemglsq  11802  resqrexlemga  11803  resqrexlemsqa  11804  resqrexlemex  11805  abs00bd  11846  cau3lem  11895  caubnd2  11898  climconst  12072  climmpt  12082  climshftlemg  12084  climcn1  12090  climle  12116  climub  12126  climserle  12127  climcau  12129  climcvg1nlem  12131  climcvg1n  12132  serf0  12134  fsum3cvg  12161  summodclem3  12163  summodclem2a  12164  summodclem2  12165  summodc  12166  zsumdc  12167  fsum3  12170  fsumf1o  12173  fisumss  12175  fsum3cvg2  12177  fsum3ser  12180  fsumcl2lem  12181  fsumadd  12189  sumsnf  12192  isummulc2  12209  isumge0  12213  isumadd  12214  fsum2dlemstep  12217  fsummulc2  12231  fsumconst  12237  fsumrelem  12254  isumshft  12273  isum1p  12275  isumnn0nn  12276  isumrpcl  12277  isumlessdc  12279  cvgratnnlemnexp  12307  cvgratnnlemmn  12308  cvgratnnlemseq  12309  cvgratnnlemabsle  12310  cvgratnnlemfm  12312  cvgratnnlemrate  12313  cvgratnn  12314  cvgratz  12315  mertenslemi1  12318  mertenslem2  12319  mertensabs  12320  clim2prod  12322  prodfap0  12328  prodfrecap  12329  prodfdivap  12330  fproddccvg  12355  prodmodclem3  12358  prodmodclem2a  12359  prodmodclem2  12360  prodmodc  12361  zproddc  12362  fprodseq  12366  fprodf1o  12371  fprodssdc  12373  fprodmul  12374  prodsnf  12375  fprodfac  12398  fprodconst  12403  fprod2dlemstep  12405  eftvalcn  12440  ef0lem  12443  ege2le3  12454  efcj  12456  efaddlem  12457  eftlub  12473  efgt1p2  12478  reef11  12482  tanvalap  12491  efieq1re  12555  eirraplem  12560  dvdsabseq  12630  dvdsfac  12643  gcd0id  12772  nninfctlemfo  12833  nn0seqcvgd  12835  alginv  12841  algcvg  12842  algcvga  12845  algfx  12846  eucalglt  12851  lcmid  12874  qredeu  12891  prmfac1  12947  sqne2sq  12973  qnumdenbi  12988  dfphi2  13018  eulerthlemrprm  13027  eulerthlema  13028  eulerthlemh  13029  eulerthlemth  13030  phisum  13039  pcmpt  13142  pcfac  13149  1arithlem4  13165  elgz  13170  4sqlem4  13191  4sqlem12  13201  2expltfac  13239  ballotfilem2  13277  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfileme  13285  ballotfilemefi  13286  ballotfilemodife  13289  ballotfilem4  13290  ballotfilemi  13292  ballotfilemic  13299  ballotfilem1c  13300  ballotfilemrval  13310  ballotfilemrc  13323  ballotfilemrinv  13326  ballotfilemth  13330  ballotfi  13331  ennnfonelemk  13340  ennnfonelemp1  13346  ennnfoneleminc  13351  ennnfonelemkh  13352  ennnfonelemhf1o  13353  ennnfonelemex  13354  ennnfonelemhom  13355  ennnfonelemrn  13359  ennnfonelemnn0  13362  ennnfonelemr  13363  ennnfonelemim  13364  ctinfomlemom  13367  ctinfom  13368  ctiunctlemfo  13379  nninfdclemlt  13391  nninfdclemf1  13392  sloteq  13406  ressvalsets  13467  topnvalg  13654  imasex  13675  imasaddvallemg  13685  qusex  13695  xpsfrnel  13714  xpsfeq  13715  ismgm  13726  plusffvalg  13731  grpidvalg  13742  gzsumfzval  13760  gzsumval2  13763  issgrp  13767  ismnddef  13780  ismhm  13817  mhmex  13818  mhmlin  13823  issubm  13828  mhmeql  13848  isgrp  13860  grpn0  13889  grpinvfvalg  13896  grpsubfvalg  13899  grpsubval  13900  grpinv11  13923  grpinvnz  13925  mhmlem  13966  mulgfvalg  13973  mulgsubcl  13988  mulgaddcomlem  13997  mulgneg2  14008  mulgass  14011  issubg  14025  subgex  14028  issubg2m  14041  issubg4m  14045  0subg  14051  isnsg  14054  releqgg  14072  eqgex  14073  eqgval  14075  isghm  14095  ghmlin  14100  ghmrn  14109  ghmeql  14119  f1ghm0to0  14124  iscmn  14145  gsumconstcmn  14215  prdsbasprj  14231  prdsplusgfval  14233  prdsmulrfval  14235  prdsidlem  14242  prdsinvlem  14245  xpsval  14250  pws0g  14262  pwsinvg  14264  pwssub  14265  mgpvalg  14269  isrng  14282  issrg  14318  srgfcl  14326  isring  14353  iscrng  14356  mulgass2  14412  opprvalg  14423  dvdsrvald  14449  isunitd  14462  invrfvald  14478  dvrfvald  14489  dvrvald  14490  isrhm  14514  rhmval  14529  isnzr  14537  islring  14548  issubrng  14556  issubrg  14578  rrgval  14619  rrgsupp  14623  isdomn  14627  aprval  14640  aprap  14647  aprprop  14650  isdrngtap  14655  islmod  14676  scaffvalg  14692  lsssetm  14742  lspfval  14774  sraval  14823  rlmvalg  14840  2idlval  14888  2idlvalg  14889  cnfldmulg  14962  zlmval  15011  znf1o  15035  isassa  15051  aspval  15064  asclfval  15070  psrlinv  15124  mplsubgfilemcl  15139  istps  15182  clsfval  15251  cnpval  15348  lmconst  15366  txcnp  15421  upxp  15422  uptx  15424  txlm  15429  lmcn2  15430  cnmpt11  15433  cnmpt11f  15434  cnmpt1t  15435  cnmpt21  15441  cnmpt21f  15442  cnmpt2t  15443  mopnval  15592  isxms  15601  isms  15603  comet  15649  mopnex  15655  xmetxp  15657  xmetxpbl  15658  txmetcnp  15668  txmetcn  15669  qtopbasss  15671  cncfi  15728  cncfmpt1f  15748  ivthinclemlm  15784  ivthinclemum  15785  ivthinclemlopn  15786  ivthinclemlr  15787  ivthinclemuopn  15788  ivthinclemur  15789  ivthinclemdisj  15790  ivthinclemloc  15791  ivthinc  15793  ivthdec  15794  ivthreinc  15795  cnlimci  15823  limccnpcntop  15825  eldvap  15832  dvcoapbr  15857  dvcj  15859  dvfre  15860  dvmptcjx  15874  dveflem  15876  elply2  15885  elplyd  15891  plymullem1  15898  plyadd  15901  plymul  15902  plycoeid3  15907  plycolemc  15908  plyco  15909  plycjlemc  15910  plycj  15911  dvply1  15915  sin0pilem2  15933  pilem3  15934  coseq0q4123  15985  coseq0negpitopi  15987  cos11  16004  logltb  16026  logfac  16048  rpcxpef  16049  rplogbval  16100  pellexlem1  16148  pellexlem3  16150  ppiqltx  16183  mpodvdsmulf1o  16185  fsumdvdsmul  16186  bposlem5  16213  zabsle1  16216  lgslem2  16218  lgslem3  16219  lgsfcl2  16223  lgsfle1  16226  lgsle1  16232  lgsdirprm  16251  lgseisenlem2  16288  lgsquadlem2  16295  2sqlem1  16331  2sqlem2  16332  mul2sq  16333  2sqlem3  16334  2sqlem9  16341  2sqlem10  16342  vtxvalg  16355  iedgvalg  16356  edgvalg  16398  edgopval  16401  edgstruct  16403  isuhgrm  16410  isushgrm  16411  isupgren  16434  isumgren  16444  isuspgren  16496  isusgren  16497  umgr2edg1  16548  usgredg2vlem1  16561  usgredg2vlem2  16562  ushgredgedg  16565  issubgr  16596  vtxdgfval  16627  vtxedgfi  16628  vtxdg0v  16633  vtxdumgrfival  16637  1loopgrvd0fi  16645  1hevtxdg0fi  16646  1hevtxdg1en  16647  wkslem1  16659  wkslem2  16660  wksfval  16661  iswlk  16662  uspgr2wlkeq  16704  uspgr2wlkeqi  16706  2wlklem  16715  trlsfvalg  16722  clwwlkg  16732  isclwwlk  16733  clwwlkccatlem  16739  clwwlkng  16744  clwwlkn2  16760  clwwlkext2edg  16761  umgr2cwwk2dif  16763  umgr2cwwkdifex  16764  clwwlknonmpo  16767  clwwlknonel  16771  clwwlknonex2lem2  16777  eupthsg  16784  iseupth  16786  eupthseg  16791  eupth2lem3lem3fi  16809  eupth2lem3lem6fi  16810  eupth2lem3lem4fi  16812  eupth2lem3fi  16815  eupth2lemsfi  16817  eupth2fi  16818  eulerpathprum  16819  konigsberglem4  16830  depindlem1  16845  depindlem2  16846  depindlem3  16847  012of  17121  2o01f  17122  subctctexmid  17128  nnsf  17146  nninfalllem1  17149  nninffeq  17161  qdencn  17170  trilpolemclim  17183  trilpolemcl  17184  trilpolemisumle  17185  trilpolemeq1  17187  trilpolemlt1  17188  trilpo  17190  iswomni0  17199  redcwlpo  17203  dceqnconst  17208  dcapnconst  17209  nconstwlpolemgt0  17212  nconstwlpolem  17213  nconstwlpo  17214  neapmkv  17216