Theorem fveq2 5629

Description: Equality theorem for function value. (Contributed by NM, 29-Dec-1996.)

Assertion

Ref	Expression
fveq2	⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))

Proof of Theorem fveq2

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq1 4086	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝑥 ↔ 𝐵𝐹𝑥))
2	1	iotabidv 5301	. 2 ⊢ (𝐴 = 𝐵 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐵𝐹𝑥))
3		df-fv 5326	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5326	. 2 ⊢ (𝐹‘𝐵) = (℩𝑥𝐵𝐹𝑥)
5	2, 3, 4	3eqtr4g 2287	1 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))

Syntax hints:   → wi 4   = wceq 1395   class class class wbr 4083  ℩cio 5276  ‘cfv 5318

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326

This theorem is referenced by:  fveq2i  5632  fveq2d  5633  2fveq3  5634  fvifdc  5651  dffn5imf  5691  fvelimab  5692  ssimaex  5697  fvco4  5708  fvmptssdm  5721  fvmptf  5729  eqfnfv2f  5738  fvelrn  5768  ralrnmpt  5779  rexrnmpt  5780  ffnfvf  5796  fmptco  5803  cofmpt  5806  fcompt  5807  fcoconst  5808  fnressn  5829  fressnfv  5830  fconstfvm  5861  foco2  5883  funiunfvdmf  5894  f1veqaeq  5899  dff13f  5900  f1fveq  5902  f1elima  5903  f1ocnvfv  5909  f1ocnvfvb  5910  fcofo  5914  cocan2  5918  fliftfun  5926  isorel  5938  isocnv  5941  isotr  5946  f1oiso2  5957  canth  5958  imbrov2fvoveq  6032  ffnov  6114  eqfnov  6117  fnovim  6119  fnrnov  6157  foov  6158  funimassov  6161  ovelimab  6162  suppssfv  6220  ofvalg  6234  ofrval  6235  offval2  6240  ofrfval2  6241  ofco  6243  caofinvl  6250  op1std  6300  op2ndd  6301  1stval2  6307  2ndval2  6308  unielxp  6326  reldm  6338  oprabco  6369  2ndconst  6374  f1o2ndf1  6380  mpoxopn0yelv  6391  mpoxopoveq  6392  smoel  6452  tfrlem1  6460  tfrlem3-2d  6464  tfrlem5  6466  tfrlem9  6471  tfr0dm  6474  tfrlemiubacc  6482  tfrlemi1  6484  tfrexlem  6486  tfr1onlemsucfn  6492  tfr1onlemsucaccv  6493  tfr1onlembxssdm  6495  tfr1onlembfn  6496  tfr1onlemubacc  6498  tfr1onlemaccex  6500  tfr1onlemres  6501  tfri1dALT  6503  tfrcllemsucfn  6505  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllembfn  6509  tfrcllemubacc  6511  tfrcllemaccex  6513  tfrcllemres  6514  tfrcldm  6515  tfrcl  6516  tfri3  6519  rdgtfr  6526  rdgss  6535  rdgisuc1  6536  rdgisucinc  6537  rdgon  6538  frecabex  6550  frecabcl  6551  frecfcllem  6556  frecsuclem  6558  frecsuc  6559  frecrdg  6560  oav  6608  omv  6609  oeiv  6610  fvixp  6858  cbvixp  6870  mptelixpg  6889  elixpsn  6890  dom2lem  6931  xpcomco  6993  xpmapen  7019  fidceq  7039  fieq0  7154  ordiso2  7213  djune  7256  updjudhcoinlf  7258  updjudhcoinrg  7259  updjud  7260  omp1eom  7273  0ct  7285  ctmlemr  7286  ctssdclemn0  7288  ctssdccl  7289  ctssdc  7291  enumctlemm  7292  nninfninc  7301  nnnninfeq  7306  nnnninfeq2  7307  enomnilem  7316  finomni  7318  fodjuomnilemdc  7322  fodju0  7325  fodjuomni  7327  ismkvnex  7333  fodjumkv  7338  nninfwlporlemd  7350  nninfwlpor  7352  exmidaclem  7401  cc1  7462  cc2lem  7463  cc2  7464  cc3  7465  mulpipq2  7569  genipv  7707  genpelxp  7709  addcanprleml  7812  addcanprlemu  7813  recexprlemm  7822  recexprlemdisj  7828  recexprlemloc  7829  recexprlem1ssl  7831  recexprlem1ssu  7832  cauappcvgprlemm  7843  cauappcvgprlemdisj  7849  cauappcvgprlemloc  7850  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  cauappcvgprlem1  7857  cauappcvgprlem2  7858  cauappcvgprlemlim  7859  cauappcvgpr  7860  caucvgprlemnkj  7864  caucvgprlemnbj  7865  caucvgprlemm  7866  caucvgprlemdisj  7872  caucvgprlemloc  7873  caucvgprlemcl  7874  caucvgprlemladdfu  7875  caucvgprlemladdrl  7876  caucvgprlem1  7877  caucvgprlem2  7878  caucvgpr  7880  caucvgprprlemell  7883  caucvgprprlemelu  7884  caucvgprprlemcbv  7885  caucvgprprlemval  7886  caucvgprprlemnkeqj  7888  caucvgprprlemnbj  7891  caucvgprprlemml  7892  caucvgprprlemmu  7893  caucvgprprlemopl  7895  caucvgprprlemlol  7896  caucvgprprlemopu  7897  caucvgprprlemloc  7901  caucvgprprlemclphr  7903  caucvgprprlemexbt  7904  caucvgprprlem1  7907  caucvgprprlem2  7908  caucvgsrlemcl  7987  caucvgsrlemfv  7989  caucvgsrlembound  7992  caucvgsrlemgt1  7993  caucvgsrlemoffval  7994  caucvgsrlemoffres  7998  caucvgsrlembnd  7999  caucvgsr  8000  axcaucvglemcau  8096  axcaucvglemres  8097  uz11  9757  cnref1o  9858  fzprval  10290  fztpval  10291  zsupcllemex  10462  infssuzex  10465  suprzubdc  10468  frec2uzuzd  10636  frec2uzltd  10637  frec2uzlt2d  10638  frecuzrdgrrn  10642  frec2uzrdg  10643  frecuzrdgtcl  10646  frecuzrdgg  10650  frecuzrdgfunlem  10653  frecfzennn  10660  seqeq1  10684  iseqovex  10692  seq3val  10694  seqvalcd  10695  seq3-1  10696  seqf  10698  seq3p1  10699  seqovcd  10701  seqp1cd  10704  seq3clss  10705  seq3fveq2  10709  seqfveq2g  10711  seqfveqg  10712  seq3fveq  10713  seq3feq  10714  seq3shft2  10715  seqshft2g  10716  monoord  10719  monoord2  10720  ser3mono  10721  seq3split  10722  seqsplitg  10723  seq3caopr3  10725  seqcaopr3g  10726  seq3caopr2  10727  seqcaopr2g  10728  iseqf1olemkle  10731  iseqf1olemklt  10732  iseqf1olemqval  10734  iseqf1olemqk  10741  iseqf1olemjpcl  10742  iseqf1olemqpcl  10743  iseqf1olemfvp  10744  seq3f1olemqsumkj  10745  seq3f1olemqsum  10747  seq3f1olemstep  10748  seq3f1olemp  10749  seq3f1oleml  10750  seq3f1o  10751  seqf1oglem2a  10752  seqf1og  10755  seq3id2  10760  seq3homo  10761  seq3z  10762  seqhomog  10764  seqfeq4g  10765  ser3ge0  10770  ser3le  10771  exp3vallem  10774  exp3val  10775  facp1  10964  faccl  10969  facdiv  10972  facwordi  10974  faclbnd  10975  facubnd  10979  bcval  10983  bcval5  10997  fz1eqb  11024  omgadd  11036  hashxp  11061  zfz1isolem1  11075  zfz1iso  11076  seq3coll  11077  eqwrd  11125  lswwrd  11131  lswex  11136  ccatfvalfi  11140  ccatval1  11145  ccatval2  11146  ccatalpha  11161  s1eq  11167  eqs1  11176  swrdval  11195  ccatopth2  11264  wrd2ind  11270  seq3shft  11364  reval  11375  replim  11385  cj11  11431  caucvgre  11507  cvg1nlemcau  11510  cvg1nlemres  11511  rexuz3  11516  absval  11527  resqrexlemover  11536  resqrexlemdecn  11538  resqrexlemlo  11539  resqrexlemcalc3  11542  resqrexlemnm  11544  resqrexlemcvg  11545  resqrexlemoverl  11547  resqrexlemglsq  11548  resqrexlemga  11549  resqrexlemsqa  11550  resqrexlemex  11551  abs00bd  11592  cau3lem  11640  caubnd2  11643  climconst  11816  climmpt  11826  climshftlemg  11828  climcn1  11834  climle  11860  climub  11870  climserle  11871  climcau  11873  climcvg1nlem  11875  climcvg1n  11876  serf0  11878  fsum3cvg  11904  summodclem3  11906  summodclem2a  11907  summodclem2  11908  summodc  11909  zsumdc  11910  fsum3  11913  fsumf1o  11916  fisumss  11918  fsum3cvg2  11920  fsum3ser  11923  fsumcl2lem  11924  fsumadd  11932  sumsnf  11935  isummulc2  11952  isumge0  11956  isumadd  11957  fsum2dlemstep  11960  fsummulc2  11974  fsumconst  11980  fsumrelem  11997  isumshft  12016  isum1p  12018  isumnn0nn  12019  isumrpcl  12020  isumlessdc  12022  cvgratnnlemnexp  12050  cvgratnnlemmn  12051  cvgratnnlemseq  12052  cvgratnnlemabsle  12053  cvgratnnlemfm  12055  cvgratnnlemrate  12056  cvgratnn  12057  cvgratz  12058  mertenslemi1  12061  mertenslem2  12062  mertensabs  12063  clim2prod  12065  prodfap0  12071  prodfrecap  12072  prodfdivap  12073  fproddccvg  12098  prodmodclem3  12101  prodmodclem2a  12102  prodmodclem2  12103  prodmodc  12104  zproddc  12105  fprodseq  12109  fprodf1o  12114  fprodssdc  12116  fprodmul  12117  prodsnf  12118  fprodfac  12141  fprodconst  12146  fprod2dlemstep  12148  eftvalcn  12183  ef0lem  12186  ege2le3  12197  efcj  12199  efaddlem  12200  eftlub  12216  efgt1p2  12221  reef11  12225  tanvalap  12234  efieq1re  12298  eirraplem  12303  dvdsabseq  12373  dvdsfac  12386  gcd0id  12515  nninfctlemfo  12576  nn0seqcvgd  12578  alginv  12584  algcvg  12585  algcvga  12588  algfx  12589  eucalglt  12594  lcmid  12617  qredeu  12634  prmfac1  12689  sqne2sq  12714  qnumdenbi  12729  dfphi2  12757  eulerthlemrprm  12766  eulerthlema  12767  eulerthlemh  12768  eulerthlemth  12769  phisum  12778  pcmpt  12881  pcfac  12888  1arithlem4  12904  elgz  12909  4sqlem4  12930  4sqlem12  12940  2expltfac  12977  ennnfonelemk  12986  ennnfonelemp1  12992  ennnfoneleminc  12997  ennnfonelemkh  12998  ennnfonelemhf1o  12999  ennnfonelemex  13000  ennnfonelemhom  13001  ennnfonelemrn  13005  ennnfonelemnn0  13008  ennnfonelemr  13009  ennnfonelemim  13010  ctinfomlemom  13013  ctinfom  13014  ctiunctlemfo  13025  nninfdclemlt  13037  nninfdclemf1  13038  sloteq  13052  ressvalsets  13112  topnvalg  13299  prdsbasprj  13330  prdsplusgfval  13332  prdsmulrfval  13334  imasex  13353  imasaddvallemg  13363  qusex  13373  xpsfrnel  13392  xpsfeq  13393  xpsval  13400  ismgm  13405  plusffvalg  13410  grpidvalg  13421  gsumfzval  13439  gsumval2  13445  issgrp  13451  ismnddef  13466  prdsidlem  13495  pws0g  13499  ismhm  13509  mhmex  13510  mhmlin  13515  issubm  13520  mhmeql  13540  isgrp  13554  grpn0  13583  grpinvfvalg  13590  grpsubfvalg  13593  grpsubval  13594  grpinv11  13617  grpinvnz  13619  prdsinvlem  13656  pwsinvg  13660  pwssub  13661  mhmlem  13666  mulgfvalg  13673  mulgsubcl  13688  mulgaddcomlem  13697  mulgneg2  13708  mulgass  13711  issubg  13725  subgex  13728  issubg2m  13741  issubg4m  13745  0subg  13751  isnsg  13754  releqgg  13772  eqgex  13773  eqgval  13775  isghm  13795  ghmlin  13800  ghmrn  13809  ghmeql  13819  f1ghm0to0  13824  iscmn  13845  mgpvalg  13901  isrng  13912  issrg  13943  srgfcl  13951  isring  13978  iscrng  13981  mulgass2  14036  opprvalg  14047  dvdsrvald  14072  isunitd  14085  invrfvald  14101  dvrfvald  14112  dvrvald  14113  isrhm  14137  rhmval  14152  isnzr  14160  islring  14171  issubrng  14178  issubrg  14200  rrgval  14241  isdomn  14248  aprval  14261  aprap  14265  islmod  14270  scaffvalg  14285  lsssetm  14335  lspfval  14367  sraval  14416  rlmvalg  14433  2idlval  14481  2idlvalg  14482  cnfldmulg  14555  zlmval  14606  znf1o  14630  psrlinv  14663  mplsubgfilemcl  14678  istps  14721  clsfval  14790  cnpval  14887  lmconst  14905  txcnp  14960  upxp  14961  uptx  14963  txlm  14968  lmcn2  14969  cnmpt11  14972  cnmpt11f  14973  cnmpt1t  14974  cnmpt21  14980  cnmpt21f  14981  cnmpt2t  14982  mopnval  15131  isxms  15140  isms  15142  comet  15188  mopnex  15194  xmetxp  15196  xmetxpbl  15197  txmetcnp  15207  txmetcn  15208  qtopbasss  15210  cncfi  15267  cncfmpt1f  15287  ivthinclemlm  15323  ivthinclemum  15324  ivthinclemlopn  15325  ivthinclemlr  15326  ivthinclemuopn  15327  ivthinclemur  15328  ivthinclemdisj  15329  ivthinclemloc  15330  ivthinc  15332  ivthdec  15333  ivthreinc  15334  cnlimci  15362  limccnpcntop  15364  eldvap  15371  dvcoapbr  15396  dvcj  15398  dvfre  15399  dvmptcjx  15413  dveflem  15415  elply2  15424  elplyd  15430  plymullem1  15437  plyadd  15440  plymul  15441  plycoeid3  15446  plycolemc  15447  plyco  15448  plycjlemc  15449  plycj  15450  dvply1  15454  sin0pilem2  15471  pilem3  15472  coseq0q4123  15523  coseq0negpitopi  15525  cos11  15542  logltb  15563  rpcxpef  15583  rplogbval  15634  mpodvdsmulf1o  15679  fsumdvdsmul  15680  zabsle1  15693  lgslem2  15695  lgslem3  15696  lgsfcl2  15700  lgsfle1  15703  lgsle1  15709  lgsdirprm  15728  lgseisenlem2  15765  lgsquadlem2  15772  2sqlem1  15808  2sqlem2  15809  mul2sq  15810  2sqlem3  15811  2sqlem9  15818  2sqlem10  15819  vtxvalg  15832  iedgvalg  15833  edgvalg  15875  edgopval  15877  edgstruct  15879  isuhgrm  15886  isushgrm  15887  isupgren  15910  isumgren  15920  isuspgren  15970  isusgren  15971  umgr2edg1  16022  usgredg2vlem1  16035  usgredg2vlem2  16036  ushgredgedg  16039  vtxdgfval  16047  vtxedgfi  16048  vtxdg0v  16053  vtxdumgrfival  16057  wkslem1  16061  wkslem2  16062  wksfval  16063  iswlk  16064  uspgr2wlkeq  16106  uspgr2wlkeqi  16108  2wlklem  16115  trlsfvalg  16122  clwwlkg  16131  isclwwlk  16132  clwwlkccatlem  16137  012of  16416  2o01f  16417  subctctexmid  16425  nnsf  16431  nninfalllem1  16434  nninffeq  16446  qdencn  16455  trilpolemclim  16464  trilpolemcl  16465  trilpolemisumle  16466  trilpolemeq1  16468  trilpolemlt1  16469  trilpo  16471  iswomni0  16479  redcwlpo  16483  dceqnconst  16488  dcapnconst  16489  nconstwlpolemgt0  16492  nconstwlpolem  16493  nconstwlpo  16494  neapmkv  16496