Theorem fveq2 5599

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 4062	. . 3 |- ( A = B -> ( A F x <-> B F x ) )
2	1	iotabidv 5273	. 2 |- ( A = B -> ( iota x A F x ) = ( iota x B F x ) )
3		df-fv 5298	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5298	. 2 |- ( F ` B ) = ( iota x B F x )
5	2, 3, 4	3eqtr4g 2265	1 |- ( A = B -> ( F ` A ) = ( F ` B ) )

Syntax hints:   -> wi 4   = wceq 1373   class class class wbr 4059   iotacio 5249   ` cfv 5290

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rex 2492  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-iota 5251  df-fv 5298

This theorem is referenced by:  fveq2i  5602  fveq2d  5603  2fveq3  5604  fvifdc  5621  dffn5imf  5657  fvelimab  5658  ssimaex  5663  fvco4  5674  fvmptssdm  5687  fvmptf  5695  eqfnfv2f  5704  fvelrn  5734  ralrnmpt  5745  rexrnmpt  5746  ffnfvf  5762  fmptco  5769  cofmpt  5772  fcompt  5773  fcoconst  5774  fnressn  5793  fressnfv  5794  fconstfvm  5825  foco2  5845  funiunfvdmf  5856  f1veqaeq  5861  dff13f  5862  f1fveq  5864  f1elima  5865  f1ocnvfv  5871  f1ocnvfvb  5872  fcofo  5876  cocan2  5880  fliftfun  5888  isorel  5900  isocnv  5903  isotr  5908  f1oiso2  5919  canth  5920  imbrov2fvoveq  5992  ffnov  6072  eqfnov  6075  fnovim  6077  fnrnov  6115  foov  6116  funimassov  6119  ovelimab  6120  suppssfv  6177  ofvalg  6191  ofrval  6192  offval2  6197  ofrfval2  6198  ofco  6200  caofinvl  6207  op1std  6257  op2ndd  6258  1stval2  6264  2ndval2  6265  unielxp  6283  reldm  6295  oprabco  6326  2ndconst  6331  f1o2ndf1  6337  mpoxopn0yelv  6348  mpoxopoveq  6349  smoel  6409  tfrlem1  6417  tfrlem3-2d  6421  tfrlem5  6423  tfrlem9  6428  tfr0dm  6431  tfrlemiubacc  6439  tfrlemi1  6441  tfrexlem  6443  tfr1onlemsucfn  6449  tfr1onlemsucaccv  6450  tfr1onlembxssdm  6452  tfr1onlembfn  6453  tfr1onlemubacc  6455  tfr1onlemaccex  6457  tfr1onlemres  6458  tfri1dALT  6460  tfrcllemsucfn  6462  tfrcllemsucaccv  6463  tfrcllembxssdm  6465  tfrcllembfn  6466  tfrcllemubacc  6468  tfrcllemaccex  6470  tfrcllemres  6471  tfrcldm  6472  tfrcl  6473  tfri3  6476  rdgtfr  6483  rdgss  6492  rdgisuc1  6493  rdgisucinc  6494  rdgon  6495  frecabex  6507  frecabcl  6508  frecfcllem  6513  frecsuclem  6515  frecsuc  6516  frecrdg  6517  oav  6563  omv  6564  oeiv  6565  fvixp  6813  cbvixp  6825  mptelixpg  6844  elixpsn  6845  dom2lem  6886  xpcomco  6946  xpmapen  6972  fidceq  6992  fieq0  7104  ordiso2  7163  djune  7206  updjudhcoinlf  7208  updjudhcoinrg  7209  updjud  7210  omp1eom  7223  0ct  7235  ctmlemr  7236  ctssdclemn0  7238  ctssdccl  7239  ctssdc  7241  enumctlemm  7242  nninfninc  7251  nnnninfeq  7256  nnnninfeq2  7257  enomnilem  7266  finomni  7268  fodjuomnilemdc  7272  fodju0  7275  fodjuomni  7277  ismkvnex  7283  fodjumkv  7288  nninfwlporlemd  7300  nninfwlpor  7302  exmidaclem  7351  cc1  7412  cc2lem  7413  cc2  7414  cc3  7415  mulpipq2  7519  genipv  7657  genpelxp  7659  addcanprleml  7762  addcanprlemu  7763  recexprlemm  7772  recexprlemdisj  7778  recexprlemloc  7779  recexprlem1ssl  7781  recexprlem1ssu  7782  cauappcvgprlemm  7793  cauappcvgprlemdisj  7799  cauappcvgprlemloc  7800  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  cauappcvgprlem1  7807  cauappcvgprlem2  7808  cauappcvgprlemlim  7809  cauappcvgpr  7810  caucvgprlemnkj  7814  caucvgprlemnbj  7815  caucvgprlemm  7816  caucvgprlemdisj  7822  caucvgprlemloc  7823  caucvgprlemcl  7824  caucvgprlemladdfu  7825  caucvgprlemladdrl  7826  caucvgprlem1  7827  caucvgprlem2  7828  caucvgpr  7830  caucvgprprlemell  7833  caucvgprprlemelu  7834  caucvgprprlemcbv  7835  caucvgprprlemval  7836  caucvgprprlemnkeqj  7838  caucvgprprlemnbj  7841  caucvgprprlemml  7842  caucvgprprlemmu  7843  caucvgprprlemopl  7845  caucvgprprlemlol  7846  caucvgprprlemopu  7847  caucvgprprlemloc  7851  caucvgprprlemclphr  7853  caucvgprprlemexbt  7854  caucvgprprlem1  7857  caucvgprprlem2  7858  caucvgsrlemcl  7937  caucvgsrlemfv  7939  caucvgsrlembound  7942  caucvgsrlemgt1  7943  caucvgsrlemoffval  7944  caucvgsrlemoffres  7948  caucvgsrlembnd  7949  caucvgsr  7950  axcaucvglemcau  8046  axcaucvglemres  8047  uz11  9706  cnref1o  9807  fzprval  10239  fztpval  10240  zsupcllemex  10410  infssuzex  10413  suprzubdc  10416  frec2uzuzd  10584  frec2uzltd  10585  frec2uzlt2d  10586  frecuzrdgrrn  10590  frec2uzrdg  10591  frecuzrdgtcl  10594  frecuzrdgg  10598  frecuzrdgfunlem  10601  frecfzennn  10608  seqeq1  10632  iseqovex  10640  seq3val  10642  seqvalcd  10643  seq3-1  10644  seqf  10646  seq3p1  10647  seqovcd  10649  seqp1cd  10652  seq3clss  10653  seq3fveq2  10657  seqfveq2g  10659  seqfveqg  10660  seq3fveq  10661  seq3feq  10662  seq3shft2  10663  seqshft2g  10664  monoord  10667  monoord2  10668  ser3mono  10669  seq3split  10670  seqsplitg  10671  seq3caopr3  10673  seqcaopr3g  10674  seq3caopr2  10675  seqcaopr2g  10676  iseqf1olemkle  10679  iseqf1olemklt  10680  iseqf1olemqval  10682  iseqf1olemqk  10689  iseqf1olemjpcl  10690  iseqf1olemqpcl  10691  iseqf1olemfvp  10692  seq3f1olemqsumkj  10693  seq3f1olemqsum  10695  seq3f1olemstep  10696  seq3f1olemp  10697  seq3f1oleml  10698  seq3f1o  10699  seqf1oglem2a  10700  seqf1og  10703  seq3id2  10708  seq3homo  10709  seq3z  10710  seqhomog  10712  seqfeq4g  10713  ser3ge0  10718  ser3le  10719  exp3vallem  10722  exp3val  10723  facp1  10912  faccl  10917  facdiv  10920  facwordi  10922  faclbnd  10923  facubnd  10927  bcval  10931  bcval5  10945  fz1eqb  10972  omgadd  10984  hashxp  11008  zfz1isolem1  11022  zfz1iso  11023  seq3coll  11024  eqwrd  11071  lswwrd  11077  lswex  11082  ccatfvalfi  11086  ccatval1  11091  ccatval2  11092  s1eq  11111  eqs1  11120  swrdval  11139  ccatopth2  11208  wrd2ind  11214  seq3shft  11264  reval  11275  replim  11285  cj11  11331  caucvgre  11407  cvg1nlemcau  11410  cvg1nlemres  11411  rexuz3  11416  absval  11427  resqrexlemover  11436  resqrexlemdecn  11438  resqrexlemlo  11439  resqrexlemcalc3  11442  resqrexlemnm  11444  resqrexlemcvg  11445  resqrexlemoverl  11447  resqrexlemglsq  11448  resqrexlemga  11449  resqrexlemsqa  11450  resqrexlemex  11451  abs00bd  11492  cau3lem  11540  caubnd2  11543  climconst  11716  climmpt  11726  climshftlemg  11728  climcn1  11734  climle  11760  climub  11770  climserle  11771  climcau  11773  climcvg1nlem  11775  climcvg1n  11776  serf0  11778  fsum3cvg  11804  summodclem3  11806  summodclem2a  11807  summodclem2  11808  summodc  11809  zsumdc  11810  fsum3  11813  fsumf1o  11816  fisumss  11818  fsum3cvg2  11820  fsum3ser  11823  fsumcl2lem  11824  fsumadd  11832  sumsnf  11835  isummulc2  11852  isumge0  11856  isumadd  11857  fsum2dlemstep  11860  fsummulc2  11874  fsumconst  11880  fsumrelem  11897  isumshft  11916  isum1p  11918  isumnn0nn  11919  isumrpcl  11920  isumlessdc  11922  cvgratnnlemnexp  11950  cvgratnnlemmn  11951  cvgratnnlemseq  11952  cvgratnnlemabsle  11953  cvgratnnlemfm  11955  cvgratnnlemrate  11956  cvgratnn  11957  cvgratz  11958  mertenslemi1  11961  mertenslem2  11962  mertensabs  11963  clim2prod  11965  prodfap0  11971  prodfrecap  11972  prodfdivap  11973  fproddccvg  11998  prodmodclem3  12001  prodmodclem2a  12002  prodmodclem2  12003  prodmodc  12004  zproddc  12005  fprodseq  12009  fprodf1o  12014  fprodssdc  12016  fprodmul  12017  prodsnf  12018  fprodfac  12041  fprodconst  12046  fprod2dlemstep  12048  eftvalcn  12083  ef0lem  12086  ege2le3  12097  efcj  12099  efaddlem  12100  eftlub  12116  efgt1p2  12121  reef11  12125  tanvalap  12134  efieq1re  12198  eirraplem  12203  dvdsabseq  12273  dvdsfac  12286  gcd0id  12415  nninfctlemfo  12476  nn0seqcvgd  12478  alginv  12484  algcvg  12485  algcvga  12488  algfx  12489  eucalglt  12494  lcmid  12517  qredeu  12534  prmfac1  12589  sqne2sq  12614  qnumdenbi  12629  dfphi2  12657  eulerthlemrprm  12666  eulerthlema  12667  eulerthlemh  12668  eulerthlemth  12669  phisum  12678  pcmpt  12781  pcfac  12788  1arithlem4  12804  elgz  12809  4sqlem4  12830  4sqlem12  12840  2expltfac  12877  ennnfonelemk  12886  ennnfonelemp1  12892  ennnfoneleminc  12897  ennnfonelemkh  12898  ennnfonelemhf1o  12899  ennnfonelemex  12900  ennnfonelemhom  12901  ennnfonelemrn  12905  ennnfonelemnn0  12908  ennnfonelemr  12909  ennnfonelemim  12910  ctinfomlemom  12913  ctinfom  12914  ctiunctlemfo  12925  nninfdclemlt  12937  nninfdclemf1  12938  sloteq  12952  ressvalsets  13011  topnvalg  13198  prdsbasprj  13229  prdsplusgfval  13231  prdsmulrfval  13233  imasex  13252  imasaddvallemg  13262  qusex  13272  xpsfrnel  13291  xpsfeq  13292  xpsval  13299  ismgm  13304  plusffvalg  13309  grpidvalg  13320  gsumfzval  13338  gsumval2  13344  issgrp  13350  ismnddef  13365  prdsidlem  13394  pws0g  13398  ismhm  13408  mhmex  13409  mhmlin  13414  issubm  13419  mhmeql  13439  isgrp  13453  grpn0  13482  grpinvfvalg  13489  grpsubfvalg  13492  grpsubval  13493  grpinv11  13516  grpinvnz  13518  prdsinvlem  13555  pwsinvg  13559  pwssub  13560  mhmlem  13565  mulgfvalg  13572  mulgsubcl  13587  mulgaddcomlem  13596  mulgneg2  13607  mulgass  13610  issubg  13624  subgex  13627  issubg2m  13640  issubg4m  13644  0subg  13650  isnsg  13653  releqgg  13671  eqgex  13672  eqgval  13674  isghm  13694  ghmlin  13699  ghmrn  13708  ghmeql  13718  f1ghm0to0  13723  iscmn  13744  mgpvalg  13800  isrng  13811  issrg  13842  srgfcl  13850  isring  13877  iscrng  13880  mulgass2  13935  opprvalg  13946  reldvdsrsrg  13969  dvdsrvald  13970  isunitd  13983  invrfvald  13999  dvrfvald  14010  dvrvald  14011  isrhm  14035  rhmval  14050  isnzr  14058  islring  14069  issubrng  14076  issubrg  14098  rrgval  14139  isdomn  14146  aprval  14159  aprap  14163  islmod  14168  scaffvalg  14183  lsssetm  14233  lspfval  14265  sraval  14314  rlmvalg  14331  2idlval  14379  2idlvalg  14380  cnfldmulg  14453  zlmval  14504  znf1o  14528  psrlinv  14561  mplsubgfilemcl  14576  istps  14619  clsfval  14688  cnpval  14785  lmconst  14803  txcnp  14858  upxp  14859  uptx  14861  txlm  14866  lmcn2  14867  cnmpt11  14870  cnmpt11f  14871  cnmpt1t  14872  cnmpt21  14878  cnmpt21f  14879  cnmpt2t  14880  mopnval  15029  isxms  15038  isms  15040  comet  15086  mopnex  15092  xmetxp  15094  xmetxpbl  15095  txmetcnp  15105  txmetcn  15106  qtopbasss  15108  cncfi  15165  cncfmpt1f  15185  ivthinclemlm  15221  ivthinclemum  15222  ivthinclemlopn  15223  ivthinclemlr  15224  ivthinclemuopn  15225  ivthinclemur  15226  ivthinclemdisj  15227  ivthinclemloc  15228  ivthinc  15230  ivthdec  15231  ivthreinc  15232  cnlimci  15260  limccnpcntop  15262  eldvap  15269  dvcoapbr  15294  dvcj  15296  dvfre  15297  dvmptcjx  15311  dveflem  15313  elply2  15322  elplyd  15328  plymullem1  15335  plyadd  15338  plymul  15339  plycoeid3  15344  plycolemc  15345  plyco  15346  plycjlemc  15347  plycj  15348  dvply1  15352  sin0pilem2  15369  pilem3  15370  coseq0q4123  15421  coseq0negpitopi  15423  cos11  15440  logltb  15461  rpcxpef  15481  rplogbval  15532  mpodvdsmulf1o  15577  fsumdvdsmul  15578  zabsle1  15591  lgslem2  15593  lgslem3  15594  lgsfcl2  15598  lgsfle1  15601  lgsle1  15607  lgsdirprm  15626  lgseisenlem2  15663  lgsquadlem2  15670  2sqlem1  15706  2sqlem2  15707  mul2sq  15708  2sqlem3  15709  2sqlem9  15716  2sqlem10  15717  vtxvalg  15730  iedgvalg  15731  edgvalg  15771  edgopval  15773  edgstruct  15775  isuhgrm  15782  isushgrm  15783  isupgren  15806  isumgren  15816  012of  16130  2o01f  16131  subctctexmid  16139  nnsf  16144  nninfalllem1  16147  nninffeq  16159  qdencn  16168  trilpolemclim  16177  trilpolemcl  16178  trilpolemisumle  16179  trilpolemeq1  16181  trilpolemlt1  16182  trilpo  16184  iswomni0  16192  redcwlpo  16196  dceqnconst  16201  dcapnconst  16202  nconstwlpolemgt0  16205  nconstwlpolem  16206  nconstwlpo  16207  neapmkv  16209