Theorem fveq2 5698

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 4134	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝑥 ↔ 𝐵𝐹𝑥))
2	1	iotabidv 5363	. 2 ⊢ (𝐴 = 𝐵 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐵𝐹𝑥))
3		df-fv 5388	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5388	. 2 ⊢ (𝐹‘𝐵) = (℩𝑥𝐵𝐹𝑥)
5	2, 3, 4	3eqtr4g 2296	1 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))

This proof depends on syntax axioms:   → wi 4   = wceq 1402   class class class wbr 4131  ℩cio 5338  ‘cfv 5380

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 4132  df-iota 5340  df-fv 5388

This theorem is used by:  fveq2i  5701  fveq2d  5702  2fveq3  5703  fvifdc  5720  dffn5imf  5761  fvelimab  5762  ssimaex  5767  fvco4  5780  fvmptssdm  5793  fvmptf  5801  eqfnfv2f  5813  fvelrn  5842  ralrnmpt  5853  rexrnmpt  5854  ffnfvf  5870  fmptco  5877  cofmpt  5880  fcompt  5881  fcoconst  5882  fsn2g  5886  fnressn  5904  fressnfv  5905  fconstfvm  5936  dfimafnf  5958  foco2  5962  funiunfvdmf  5973  f1veqaeq  5978  dff13f  5979  f1fveq  5981  f1elima  5982  f1ocnvfv  5988  f1ocnvfvb  5989  fcofo  5993  cocan2  5997  fliftfun  6005  isorel  6017  isocnv  6020  isotr  6025  f1oiso2  6036  canth  6039  imbrov2fvoveq  6113  ffnov  6195  eqfnov  6198  fnovim  6200  fnrnov  6238  foov  6239  funimassov  6242  ovelimab  6243  ofvalg  6316  ofrval  6317  offval2  6322  ofrfval2  6323  ofco  6325  caofinvl  6332  op1std  6386  op2ndd  6387  1stval2  6393  2ndval2  6394  unielxp  6412  reldm  6424  oprabco  6457  2ndconst  6462  f1o2ndf1  6468  elsuppfng  6486  elsuppfn  6487  mpoxopn0yelv  6514  mpoxopoveq  6515  smoel  6575  tfrlem1  6583  tfrlem3-2d  6587  tfrlem5  6589  tfrlem9  6594  tfr0dm  6597  tfrlemiubacc  6605  tfrlemi1  6607  tfrexlem  6609  tfr1onlemsucfn  6615  tfr1onlemsucaccv  6616  tfr1onlembxssdm  6618  tfr1onlembfn  6619  tfr1onlemubacc  6621  tfr1onlemaccex  6623  tfr1onlemres  6624  tfri1dALT  6626  tfrcllemsucfn  6628  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  tfrcllembfn  6632  tfrcllemubacc  6634  tfrcllemaccex  6636  tfrcllemres  6637  tfrcldm  6638  tfrcl  6639  tfri3  6642  rdgtfr  6649  rdgss  6658  rdgisuc1  6659  rdgisucinc  6660  rdgon  6661  frecabex  6673  frecabcl  6674  frecfcllem  6679  frecsuclem  6681  frecsuc  6682  frecrdg  6683  oav  6731  omv  6732  oeiv  6733  fvixp  6989  cbvixp  7001  mptelixpg  7020  elixpsn  7021  dom2lem  7062  xpcomco  7128  xpmapen  7154  fidceq  7175  fieq0  7315  ordiso2  7381  djune  7424  updjudhcoinlf  7426  updjudhcoinrg  7427  updjud  7428  omp1eom  7441  0ct  7453  ctmlemr  7454  ctssdclemn0  7456  ctssdccl  7457  ctssdc  7459  enumctlemm  7460  nninfninc  7469  nnnninfeq  7474  nnnninfeq2  7475  enomnilem  7484  finomni  7486  fodjuomnilemdc  7490  fodju0  7493  fodjuomni  7495  ismkvnex  7501  fodjumkv  7506  nninfwlporlemd  7518  nninfwlpor  7520  exmidaclem  7570  cc1  7637  cc2lem  7638  cc2  7639  cc3  7640  mulpipq2  7744  genipv  7882  genpelxp  7884  addcanprleml  7987  addcanprlemu  7988  recexprlemm  7997  recexprlemdisj  8003  recexprlemloc  8004  recexprlem1ssl  8006  recexprlem1ssu  8007  cauappcvgprlemm  8018  cauappcvgprlemdisj  8024  cauappcvgprlemloc  8025  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  cauappcvgprlem1  8032  cauappcvgprlem2  8033  cauappcvgprlemlim  8034  cauappcvgpr  8035  caucvgprlemnkj  8039  caucvgprlemnbj  8040  caucvgprlemm  8041  caucvgprlemdisj  8047  caucvgprlemloc  8048  caucvgprlemcl  8049  caucvgprlemladdfu  8050  caucvgprlemladdrl  8051  caucvgprlem1  8052  caucvgprlem2  8053  caucvgpr  8055  caucvgprprlemell  8058  caucvgprprlemelu  8059  caucvgprprlemcbv  8060  caucvgprprlemval  8061  caucvgprprlemnkeqj  8063  caucvgprprlemnbj  8066  caucvgprprlemml  8067  caucvgprprlemmu  8068  caucvgprprlemopl  8070  caucvgprprlemlol  8071  caucvgprprlemopu  8072  caucvgprprlemloc  8076  caucvgprprlemclphr  8078  caucvgprprlemexbt  8079  caucvgprprlem1  8082  caucvgprprlem2  8083  caucvgsrlemcl  8162  caucvgsrlemfv  8164  caucvgsrlembound  8167  caucvgsrlemgt1  8168  caucvgsrlemoffval  8169  caucvgsrlemoffres  8173  caucvgsrlembnd  8174  caucvgsr  8175  axcaucvglemcau  8271  axcaucvglemres  8272  uz11  9961  cnref1o  10068  fzprval  10506  fztpval  10507  zsupcllemex  10680  infssuzex  10683  suprzubdc  10688  frec2uzuzd  10860  frec2uzltd  10861  frec2uzlt2d  10862  frecuzrdgrrn  10866  frec2uzrdg  10867  frecuzrdgtcl  10870  frecuzrdgg  10874  frecuzrdgfunlem  10877  frecfzennn  10884  seqeq1  10908  iseqovex  10916  seq3val  10918  seqvalcd  10919  seq3-1  10920  seqf  10922  seq3p1  10923  seqovcd  10925  seqp1cd  10928  seq3clss  10929  seq3fveq2  10933  seqfveq2g  10935  seqfveqg  10936  seq3fveq  10937  seq3feq  10938  seq3shft2  10939  seqshft2g  10940  monoord  10943  monoord2  10944  ser3mono  10945  seq3split  10946  seqsplitg  10947  seq3caopr3  10949  seqcaopr3g  10950  seq3caopr2  10951  seqcaopr2g  10952  iseqf1olemkle  10955  iseqf1olemklt  10956  iseqf1olemqval  10958  iseqf1olemqk  10965  iseqf1olemjpcl  10966  iseqf1olemqpcl  10967  iseqf1olemfvp  10968  seq3f1olemqsumkj  10969  seq3f1olemqsum  10971  seq3f1olemstep  10972  seq3f1olemp  10973  seq3f1oleml  10974  seq3f1o  10975  seqf1oglem2a  10976  seqf1og  10979  seq3id2  10984  seq3homo  10985  seq3z  10986  seqhomog  10988  seqfeq4g  10989  ser3ge0  10994  ser3le  10995  exp3vallem  10998  exp3val  10999  facp1  11190  faccl  11195  facdiv  11198  facwordi  11200  faclbnd  11201  facubnd  11205  bcval  11209  bcval5  11223  fz1eqb  11251  omgadd  11264  hashxp  11289  hashmap  11290  hashfibc  11305  hashf1lem1  11307  hashf1lem2  11308  hashf1  11309  zfz1isolem1  11314  zfz1iso  11315  seq3coll  11316  eqwrd  11367  lswwrd  11373  lswex  11378  ccatfvalfi  11382  ccatval1  11387  ccatval2  11388  ccatalpha  11403  s1eq  11409  eqs1  11418  swrdval  11442  ccatopth2  11511  wrd2ind  11517  seq3shft  11625  reval  11636  replim  11646  cj11  11693  caucvgre  11769  cvg1nlemcau  11772  cvg1nlemres  11773  rexuz3  11778  absval  11789  resqrexlemover  11798  resqrexlemdecn  11800  resqrexlemlo  11801  resqrexlemcalc3  11804  resqrexlemnm  11806  resqrexlemcvg  11807  resqrexlemoverl  11809  resqrexlemglsq  11810  resqrexlemga  11811  resqrexlemsqa  11812  resqrexlemex  11813  abs00bd  11854  cau3lem  11903  caubnd2  11906  fiidxsupcl  12018  climconst  12081  climmpt  12091  climshftlemg  12093  climcn1  12099  climle  12125  climub  12135  climserle  12136  climcau  12138  climcvg1nlem  12140  climcvg1n  12141  serf0  12143  fsum3cvg  12170  summodclem3  12172  summodclem2a  12173  summodclem2  12174  summodc  12175  zsumdc  12176  fsum3  12179  fsumf1o  12182  fisumss  12184  fsum3cvg2  12186  fsum3ser  12189  fsumcl2lem  12190  fsumadd  12198  sumsnf  12201  isummulc2  12218  isumge0  12222  isumadd  12223  fsum2dlemstep  12226  fsummulc2  12240  fsumconst  12246  fsumrelem  12263  isumshft  12282  isum1p  12284  isumnn0nn  12285  isumrpcl  12286  isumlessdc  12288  cvgratnnlemnexp  12316  cvgratnnlemmn  12317  cvgratnnlemseq  12318  cvgratnnlemabsle  12319  cvgratnnlemfm  12321  cvgratnnlemrate  12322  cvgratnn  12323  cvgratz  12324  mertenslemi1  12327  mertenslem2  12328  mertensabs  12329  clim2prod  12331  prodfap0  12337  prodfrecap  12338  prodfdivap  12339  fproddccvg  12364  prodmodclem3  12367  prodmodclem2a  12368  prodmodclem2  12369  prodmodc  12370  zproddc  12371  fprodseq  12375  fprodf1o  12380  fprodssdc  12382  fprodmul  12383  prodsnf  12384  fprodfac  12407  fprodconst  12412  fprod2dlemstep  12414  eftvalcn  12449  ef0lem  12452  ege2le3  12463  efcj  12465  efaddlem  12466  eftlub  12482  efgt1p2  12487  reef11  12491  tanvalap  12500  efieq1re  12564  eirraplem  12569  dvdsabseq  12639  dvdsfac  12652  gcd0id  12781  nninfctlemfo  12842  nn0seqcvgd  12844  alginv  12850  algcvg  12851  algcvga  12854  algfx  12855  eucalglt  12860  lcmid  12883  qredeu  12900  prmfac1  12956  sqne2sq  12982  qnumdenbi  12997  dfphi2  13027  eulerthlemrprm  13036  eulerthlema  13037  eulerthlemh  13038  eulerthlemth  13039  phisum  13048  pcmpt  13151  pcfac  13158  1arithlem4  13174  elgz  13179  4sqlem4  13200  4sqlem12  13210  2expltfac  13248  ballotfilem2  13286  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfileme  13294  ballotfilemefi  13295  ballotfilemodife  13298  ballotfilem4  13299  ballotfilemi  13301  ballotfilemic  13308  ballotfilem1c  13309  ballotfilemrval  13319  ballotfilemrc  13332  ballotfilemrinv  13335  ballotfilemth  13339  ballotfi  13340  ennnfonelemk  13349  ennnfonelemp1  13355  ennnfoneleminc  13360  ennnfonelemkh  13361  ennnfonelemhf1o  13362  ennnfonelemex  13363  ennnfonelemhom  13364  ennnfonelemrn  13368  ennnfonelemnn0  13371  ennnfonelemr  13372  ennnfonelemim  13373  ctinfomlemom  13376  ctinfom  13377  ctiunctlemfo  13388  nninfdclemlt  13400  nninfdclemf1  13401  sloteq  13415  ressvalsets  13476  topnvalg  13664  imasex  13685  imasaddvallemg  13695  qusex  13705  xpsfrnel  13724  xpsfeq  13725  ismgm  13736  plusffvalg  13741  grpidvalg  13752  gzsumfzval  13770  gzsumval2  13773  issgrp  13777  ismnddef  13790  ismhm  13827  mhmex  13828  mhmlin  13833  issubm  13838  mhmeql  13858  isgrp  13870  grpn0  13899  grpinvfvalg  13906  grpsubfvalg  13909  grpsubval  13910  grpinv11  13933  grpinvnz  13935  mhmlem  13976  mulgfvalg  13983  mulgsubcl  13998  mulgaddcomlem  14007  mulgneg2  14018  mulgass  14021  issubg  14035  subgex  14038  issubg2m  14051  issubg4m  14055  0subg  14061  isnsg  14064  releqgg  14082  eqgex  14083  eqgval  14085  isghm  14105  ghmlin  14110  ghmrn  14119  ghmeql  14129  f1ghm0to0  14134  cntzex  14150  cntrval  14151  cntzfval  14152  iscmn  14186  gsumresfi  14263  gsumconstcmn  14266  gsumcom2fi  14275  prdsbasprj  14289  prdsplusgfval  14291  prdsmulrfval  14293  prdsidlem  14300  prdsinvlem  14303  xpsval  14308  pws0g  14320  pwsinvg  14322  pwssub  14323  mgpvalg  14327  isrng  14340  issrg  14376  srgfcl  14384  isring  14411  iscrng  14414  mulgass2  14470  opprvalg  14483  dvdsrvald  14509  isunitd  14522  invrfvald  14538  dvrfvald  14549  dvrvald  14550  isrhm  14574  rhmval  14589  isnzr  14597  islring  14608  issubrng  14616  issubrg  14638  rrgval  14679  rrgsupp  14683  isdomn  14687  aprval  14700  aprap  14707  aprprop  14710  isdrngtap  14715  islmod  14736  scaffvalg  14752  lsssetm  14802  lspfval  14834  sraval  14883  rlmvalg  14900  2idlval  14948  2idlvalg  14949  cnfldmulg  15022  zlmval  15071  znf1o  15095  isassa  15111  aspval  15124  asclfval  15130  psrbaglefifi  15172  psrlinv  15194  psrlidmfi  15199  psrridmfi  15200  psrass1fi  15201  mplsubgfilemcl  15215  istps  15258  clsfval  15327  cnpval  15424  lmconst  15442  txcnp  15497  upxp  15498  uptx  15500  txlm  15505  lmcn2  15506  cnmpt11  15509  cnmpt11f  15510  cnmpt1t  15511  cnmpt21  15517  cnmpt21f  15518  cnmpt2t  15519  mopnval  15668  isxms  15677  isms  15679  comet  15725  mopnex  15731  xmetxp  15733  xmetxpbl  15734  txmetcnp  15744  txmetcn  15745  qtopbasss  15747  cncfi  15804  cncfmpt1f  15824  ivthinclemlm  15860  ivthinclemum  15861  ivthinclemlopn  15862  ivthinclemlr  15863  ivthinclemuopn  15864  ivthinclemur  15865  ivthinclemdisj  15866  ivthinclemloc  15867  ivthinc  15869  ivthdec  15870  ivthreinc  15871  cnlimci  15899  limccnpcntop  15901  eldvap  15908  dvcoapbr  15933  dvcj  15935  dvfre  15936  dvmptcjx  15950  dveflem  15952  elply2  15961  elplyd  15967  plymullem1  15974  plyadd  15977  plymul  15978  plycoeid3  15983  plycolemc  15984  plyco  15985  plycjlemc  15986  plycj  15987  dvply1  15991  sin0pilem2  16009  pilem3  16010  coseq0q4123  16061  coseq0negpitopi  16063  sineq0re  16076  cos11  16081  logltb  16104  logfac  16126  rpcxpef  16127  rplogbval  16181  pellexlem1  16229  pellexlem3  16231  efnnfsumcl  16239  chtprm  16261  efchtqdvds  16265  ppiqltx  16281  prmorcht  16282  mpodvdsmulf1o  16284  fsumdvdsmul  16285  chtqub  16296  bposlem5  16315  bposlem7  16317  bposlem8  16318  bposlem9  16319  zabsle1  16323  lgslem2  16325  lgslem3  16326  lgsfcl2  16330  lgsfle1  16333  lgsle1  16339  lgsdirprm  16358  lgseisenlem2  16395  lgsquadlem2  16402  2sqlem1  16438  2sqlem2  16439  mul2sq  16440  2sqlem3  16441  2sqlem9  16448  2sqlem10  16449  vtxvalg  16462  iedgvalg  16463  edgvalg  16505  edgopval  16508  edgstruct  16510  isuhgrm  16517  isushgrm  16518  isupgren  16541  isumgren  16551  isuspgren  16603  isusgren  16604  umgr2edg1  16655  usgredg2vlem1  16668  usgredg2vlem2  16669  ushgredgedg  16672  issubgr  16703  vtxdgfval  16734  vtxedgfi  16735  vtxdg0v  16740  vtxdumgrfival  16744  1loopgrvd0fi  16752  1hevtxdg0fi  16753  1hevtxdg1en  16754  wkslem1  16766  wkslem2  16767  wksfval  16768  iswlk  16769  uspgr2wlkeq  16811  uspgr2wlkeqi  16813  2wlklem  16822  trlsfvalg  16829  clwwlkg  16839  isclwwlk  16840  clwwlkccatlem  16846  clwwlkng  16851  clwwlkn2  16867  clwwlkext2edg  16868  umgr2cwwk2dif  16870  umgr2cwwkdifex  16871  clwwlknonmpo  16874  clwwlknonel  16878  clwwlknonex2lem2  16884  eupthsg  16891  iseupth  16893  eupthseg  16898  eupth2lem3lem3fi  16916  eupth2lem3lem6fi  16917  eupth2lem3lem4fi  16919  eupth2lem3fi  16922  eupth2lemsfi  16924  eupth2fi  16925  eulerpathprum  16926  konigsberglem4  16937  depindlem1  16952  depindlem2  16953  depindlem3  16954  012of  17228  2o01f  17229  subctctexmid  17235  nnsf  17254  nninfalllem1  17257  nninffeq  17269  qdencn  17278  trilpolemclim  17292  trilpolemcl  17293  trilpolemisumle  17294  trilpolemeq1  17296  trilpolemlt1  17297  trilpo  17299  iswomni0  17308  redcwlpo  17312  dceqnconst  17317  dcapnconst  17318  nconstwlpolemgt0  17321  nconstwlpolem  17322  nconstwlpo  17323  neapmkv  17325