Theorem fveq2 5670

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 4112	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝑥 ↔ 𝐵𝐹𝑥))
2	1	iotabidv 5335	. 2 ⊢ (𝐴 = 𝐵 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐵𝐹𝑥))
3		df-fv 5360	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5360	. 2 ⊢ (𝐹‘𝐵) = (℩𝑥𝐵𝐹𝑥)
5	2, 3, 4	3eqtr4g 2290	1 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))

Syntax hints:   → wi 4   = wceq 1398   class class class wbr 4109  ℩cio 5310  ‘cfv 5352

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-v 2815  df-un 3215  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-iota 5312  df-fv 5360

This theorem is referenced by:  fveq2i  5673  fveq2d  5674  2fveq3  5675  fvifdc  5692  dffn5imf  5732  fvelimab  5733  ssimaex  5738  fvco4  5749  fvmptssdm  5762  fvmptf  5770  eqfnfv2f  5779  fvelrn  5808  ralrnmpt  5819  rexrnmpt  5820  ffnfvf  5836  fmptco  5843  cofmpt  5846  fcompt  5847  fcoconst  5848  fsn2g  5852  fnressn  5870  fressnfv  5871  fconstfvm  5902  foco2  5926  funiunfvdmf  5937  f1veqaeq  5942  dff13f  5943  f1fveq  5945  f1elima  5946  f1ocnvfv  5952  f1ocnvfvb  5953  fcofo  5957  cocan2  5961  fliftfun  5969  isorel  5981  isocnv  5984  isotr  5989  f1oiso2  6000  canth  6001  imbrov2fvoveq  6075  ffnov  6157  eqfnov  6160  fnovim  6162  fnrnov  6200  foov  6201  funimassov  6204  ovelimab  6205  ofvalg  6276  ofrval  6277  offval2  6282  ofrfval2  6283  ofco  6285  caofinvl  6292  op1std  6342  op2ndd  6343  1stval2  6349  2ndval2  6350  unielxp  6368  reldm  6380  oprabco  6413  2ndconst  6418  f1o2ndf1  6424  elsuppfng  6442  elsuppfn  6443  mpoxopn0yelv  6470  mpoxopoveq  6471  smoel  6531  tfrlem1  6539  tfrlem3-2d  6543  tfrlem5  6545  tfrlem9  6550  tfr0dm  6553  tfrlemiubacc  6561  tfrlemi1  6563  tfrexlem  6565  tfr1onlemsucfn  6571  tfr1onlemsucaccv  6572  tfr1onlembxssdm  6574  tfr1onlembfn  6575  tfr1onlemubacc  6577  tfr1onlemaccex  6579  tfr1onlemres  6580  tfri1dALT  6582  tfrcllemsucfn  6584  tfrcllemsucaccv  6585  tfrcllembxssdm  6587  tfrcllembfn  6588  tfrcllemubacc  6590  tfrcllemaccex  6592  tfrcllemres  6593  tfrcldm  6594  tfrcl  6595  tfri3  6598  rdgtfr  6605  rdgss  6614  rdgisuc1  6615  rdgisucinc  6616  rdgon  6617  frecabex  6629  frecabcl  6630  frecfcllem  6635  frecsuclem  6637  frecsuc  6638  frecrdg  6639  oav  6687  omv  6688  oeiv  6689  fvixp  6938  cbvixp  6950  mptelixpg  6969  elixpsn  6970  dom2lem  7011  xpcomco  7077  xpmapen  7103  fidceq  7124  fieq0  7263  ordiso2  7326  djune  7369  updjudhcoinlf  7371  updjudhcoinrg  7372  updjud  7373  omp1eom  7386  0ct  7398  ctmlemr  7399  ctssdclemn0  7401  ctssdccl  7402  ctssdc  7404  enumctlemm  7405  nninfninc  7414  nnnninfeq  7419  nnnninfeq2  7420  enomnilem  7429  finomni  7431  fodjuomnilemdc  7435  fodju0  7438  fodjuomni  7440  ismkvnex  7446  fodjumkv  7451  nninfwlporlemd  7463  nninfwlpor  7465  exmidaclem  7515  cc1  7579  cc2lem  7580  cc2  7581  cc3  7582  mulpipq2  7686  genipv  7824  genpelxp  7826  addcanprleml  7929  addcanprlemu  7930  recexprlemm  7939  recexprlemdisj  7945  recexprlemloc  7946  recexprlem1ssl  7948  recexprlem1ssu  7949  cauappcvgprlemm  7960  cauappcvgprlemdisj  7966  cauappcvgprlemloc  7967  cauappcvgprlemladdru  7971  cauappcvgprlemladdrl  7972  cauappcvgprlem1  7974  cauappcvgprlem2  7975  cauappcvgprlemlim  7976  cauappcvgpr  7977  caucvgprlemnkj  7981  caucvgprlemnbj  7982  caucvgprlemm  7983  caucvgprlemdisj  7989  caucvgprlemloc  7990  caucvgprlemcl  7991  caucvgprlemladdfu  7992  caucvgprlemladdrl  7993  caucvgprlem1  7994  caucvgprlem2  7995  caucvgpr  7997  caucvgprprlemell  8000  caucvgprprlemelu  8001  caucvgprprlemcbv  8002  caucvgprprlemval  8003  caucvgprprlemnkeqj  8005  caucvgprprlemnbj  8008  caucvgprprlemml  8009  caucvgprprlemmu  8010  caucvgprprlemopl  8012  caucvgprprlemlol  8013  caucvgprprlemopu  8014  caucvgprprlemloc  8018  caucvgprprlemclphr  8020  caucvgprprlemexbt  8021  caucvgprprlem1  8024  caucvgprprlem2  8025  caucvgsrlemcl  8104  caucvgsrlemfv  8106  caucvgsrlembound  8109  caucvgsrlemgt1  8110  caucvgsrlemoffval  8111  caucvgsrlemoffres  8115  caucvgsrlembnd  8116  caucvgsr  8117  axcaucvglemcau  8213  axcaucvglemres  8214  uz11  9877  cnref1o  9983  fzprval  10416  fztpval  10417  zsupcllemex  10590  infssuzex  10593  suprzubdc  10596  frec2uzuzd  10764  frec2uzltd  10765  frec2uzlt2d  10766  frecuzrdgrrn  10770  frec2uzrdg  10771  frecuzrdgtcl  10774  frecuzrdgg  10778  frecuzrdgfunlem  10781  frecfzennn  10788  seqeq1  10812  iseqovex  10820  seq3val  10822  seqvalcd  10823  seq3-1  10824  seqf  10826  seq3p1  10827  seqovcd  10829  seqp1cd  10832  seq3clss  10833  seq3fveq2  10837  seqfveq2g  10839  seqfveqg  10840  seq3fveq  10841  seq3feq  10842  seq3shft2  10843  seqshft2g  10844  monoord  10847  monoord2  10848  ser3mono  10849  seq3split  10850  seqsplitg  10851  seq3caopr3  10853  seqcaopr3g  10854  seq3caopr2  10855  seqcaopr2g  10856  iseqf1olemkle  10859  iseqf1olemklt  10860  iseqf1olemqval  10862  iseqf1olemqk  10869  iseqf1olemjpcl  10870  iseqf1olemqpcl  10871  iseqf1olemfvp  10872  seq3f1olemqsumkj  10873  seq3f1olemqsum  10875  seq3f1olemstep  10876  seq3f1olemp  10877  seq3f1oleml  10878  seq3f1o  10879  seqf1oglem2a  10880  seqf1og  10883  seq3id2  10888  seq3homo  10889  seq3z  10890  seqhomog  10892  seqfeq4g  10893  ser3ge0  10898  ser3le  10899  exp3vallem  10902  exp3val  10903  facp1  11092  faccl  11097  facdiv  11100  facwordi  11102  faclbnd  11103  facubnd  11107  bcval  11111  bcval5  11125  fz1eqb  11153  omgadd  11166  hashxp  11191  hashmap  11192  hashfibc  11207  zfz1isolem1  11212  zfz1iso  11213  seq3coll  11214  eqwrd  11265  lswwrd  11271  lswex  11276  ccatfvalfi  11280  ccatval1  11285  ccatval2  11286  ccatalpha  11301  s1eq  11307  eqs1  11316  swrdval  11340  ccatopth2  11409  wrd2ind  11415  seq3shft  11523  reval  11534  replim  11544  cj11  11590  caucvgre  11666  cvg1nlemcau  11669  cvg1nlemres  11670  rexuz3  11675  absval  11686  resqrexlemover  11695  resqrexlemdecn  11697  resqrexlemlo  11698  resqrexlemcalc3  11701  resqrexlemnm  11703  resqrexlemcvg  11704  resqrexlemoverl  11706  resqrexlemglsq  11707  resqrexlemga  11708  resqrexlemsqa  11709  resqrexlemex  11710  abs00bd  11751  cau3lem  11799  caubnd2  11802  climconst  11975  climmpt  11985  climshftlemg  11987  climcn1  11993  climle  12019  climub  12029  climserle  12030  climcau  12032  climcvg1nlem  12034  climcvg1n  12035  serf0  12037  fsum3cvg  12064  summodclem3  12066  summodclem2a  12067  summodclem2  12068  summodc  12069  zsumdc  12070  fsum3  12073  fsumf1o  12076  fisumss  12078  fsum3cvg2  12080  fsum3ser  12083  fsumcl2lem  12084  fsumadd  12092  sumsnf  12095  isummulc2  12112  isumge0  12116  isumadd  12117  fsum2dlemstep  12120  fsummulc2  12134  fsumconst  12140  fsumrelem  12157  isumshft  12176  isum1p  12178  isumnn0nn  12179  isumrpcl  12180  isumlessdc  12182  cvgratnnlemnexp  12210  cvgratnnlemmn  12211  cvgratnnlemseq  12212  cvgratnnlemabsle  12213  cvgratnnlemfm  12215  cvgratnnlemrate  12216  cvgratnn  12217  cvgratz  12218  mertenslemi1  12221  mertenslem2  12222  mertensabs  12223  clim2prod  12225  prodfap0  12231  prodfrecap  12232  prodfdivap  12233  fproddccvg  12258  prodmodclem3  12261  prodmodclem2a  12262  prodmodclem2  12263  prodmodc  12264  zproddc  12265  fprodseq  12269  fprodf1o  12274  fprodssdc  12276  fprodmul  12277  prodsnf  12278  fprodfac  12301  fprodconst  12306  fprod2dlemstep  12308  eftvalcn  12343  ef0lem  12346  ege2le3  12357  efcj  12359  efaddlem  12360  eftlub  12376  efgt1p2  12381  reef11  12385  tanvalap  12394  efieq1re  12458  eirraplem  12463  dvdsabseq  12533  dvdsfac  12546  gcd0id  12675  nninfctlemfo  12736  nn0seqcvgd  12738  alginv  12744  algcvg  12745  algcvga  12748  algfx  12749  eucalglt  12754  lcmid  12777  qredeu  12794  prmfac1  12849  sqne2sq  12874  qnumdenbi  12889  dfphi2  12917  eulerthlemrprm  12926  eulerthlema  12927  eulerthlemh  12928  eulerthlemth  12929  phisum  12938  pcmpt  13041  pcfac  13048  1arithlem4  13064  elgz  13069  4sqlem4  13090  4sqlem12  13100  2expltfac  13137  ballotfilem2  13142  ennnfonelemk  13151  ennnfonelemp1  13157  ennnfoneleminc  13162  ennnfonelemkh  13163  ennnfonelemhf1o  13164  ennnfonelemex  13165  ennnfonelemhom  13166  ennnfonelemrn  13170  ennnfonelemnn0  13173  ennnfonelemr  13174  ennnfonelemim  13175  ctinfomlemom  13178  ctinfom  13179  ctiunctlemfo  13190  nninfdclemlt  13202  nninfdclemf1  13203  sloteq  13217  ressvalsets  13277  topnvalg  13464  prdsbasprj  13495  prdsplusgfval  13497  prdsmulrfval  13499  imasex  13518  imasaddvallemg  13528  qusex  13538  xpsfrnel  13557  xpsfeq  13558  xpsval  13565  ismgm  13570  plusffvalg  13575  grpidvalg  13586  gsumfzval  13604  gsumval2  13610  issgrp  13616  ismnddef  13631  prdsidlem  13660  pws0g  13664  ismhm  13674  mhmex  13675  mhmlin  13680  issubm  13685  mhmeql  13705  isgrp  13719  grpn0  13748  grpinvfvalg  13755  grpsubfvalg  13758  grpsubval  13759  grpinv11  13782  grpinvnz  13784  prdsinvlem  13821  pwsinvg  13825  pwssub  13826  mhmlem  13831  mulgfvalg  13838  mulgsubcl  13853  mulgaddcomlem  13862  mulgneg2  13873  mulgass  13876  issubg  13890  subgex  13893  issubg2m  13906  issubg4m  13910  0subg  13916  isnsg  13919  releqgg  13937  eqgex  13938  eqgval  13940  isghm  13960  ghmlin  13965  ghmrn  13974  ghmeql  13984  f1ghm0to0  13989  iscmn  14010  mgpvalg  14067  isrng  14078  issrg  14109  srgfcl  14117  isring  14144  iscrng  14147  mulgass2  14202  opprvalg  14213  dvdsrvald  14238  isunitd  14251  invrfvald  14267  dvrfvald  14278  dvrvald  14279  isrhm  14303  rhmval  14318  isnzr  14326  islring  14337  issubrng  14344  issubrg  14366  rrgval  14407  rrgsupp  14411  isdomn  14415  aprval  14428  aprap  14432  islmod  14439  scaffvalg  14454  lsssetm  14504  lspfval  14536  sraval  14585  rlmvalg  14602  2idlval  14650  2idlvalg  14651  cnfldmulg  14724  zlmval  14775  znf1o  14799  psrlinv  14839  mplsubgfilemcl  14854  istps  14897  clsfval  14966  cnpval  15063  lmconst  15081  txcnp  15136  upxp  15137  uptx  15139  txlm  15144  lmcn2  15145  cnmpt11  15148  cnmpt11f  15149  cnmpt1t  15150  cnmpt21  15156  cnmpt21f  15157  cnmpt2t  15158  mopnval  15307  isxms  15316  isms  15318  comet  15364  mopnex  15370  xmetxp  15372  xmetxpbl  15373  txmetcnp  15383  txmetcn  15384  qtopbasss  15386  cncfi  15443  cncfmpt1f  15463  ivthinclemlm  15499  ivthinclemum  15500  ivthinclemlopn  15501  ivthinclemlr  15502  ivthinclemuopn  15503  ivthinclemur  15504  ivthinclemdisj  15505  ivthinclemloc  15506  ivthinc  15508  ivthdec  15509  ivthreinc  15510  cnlimci  15538  limccnpcntop  15540  eldvap  15547  dvcoapbr  15572  dvcj  15574  dvfre  15575  dvmptcjx  15589  dveflem  15591  elply2  15600  elplyd  15606  plymullem1  15613  plyadd  15616  plymul  15617  plycoeid3  15622  plycolemc  15623  plyco  15624  plycjlemc  15625  plycj  15626  dvply1  15630  sin0pilem2  15647  pilem3  15648  coseq0q4123  15699  coseq0negpitopi  15701  cos11  15718  logltb  15739  rpcxpef  15759  rplogbval  15810  pellexlem1  15845  pellexlem3  15847  mpodvdsmulf1o  15858  fsumdvdsmul  15859  zabsle1  15872  lgslem2  15874  lgslem3  15875  lgsfcl2  15879  lgsfle1  15882  lgsle1  15888  lgsdirprm  15907  lgseisenlem2  15944  lgsquadlem2  15951  2sqlem1  15987  2sqlem2  15988  mul2sq  15989  2sqlem3  15990  2sqlem9  15997  2sqlem10  15998  vtxvalg  16011  iedgvalg  16012  edgvalg  16054  edgopval  16057  edgstruct  16059  isuhgrm  16066  isushgrm  16067  isupgren  16090  isumgren  16100  isuspgren  16152  isusgren  16153  umgr2edg1  16204  usgredg2vlem1  16217  usgredg2vlem2  16218  ushgredgedg  16221  issubgr  16252  vtxdgfval  16283  vtxedgfi  16284  vtxdg0v  16289  vtxdumgrfival  16293  1loopgrvd0fi  16301  1hevtxdg0fi  16302  1hevtxdg1en  16303  wkslem1  16315  wkslem2  16316  wksfval  16317  iswlk  16318  uspgr2wlkeq  16360  uspgr2wlkeqi  16362  2wlklem  16371  trlsfvalg  16378  clwwlkg  16388  isclwwlk  16389  clwwlkccatlem  16395  clwwlkng  16400  clwwlkn2  16416  clwwlkext2edg  16417  umgr2cwwk2dif  16419  umgr2cwwkdifex  16420  clwwlknonmpo  16423  clwwlknonel  16427  clwwlknonex2lem2  16433  eupthsg  16440  iseupth  16442  eupthseg  16447  eupth2lem3lem3fi  16465  eupth2lem3lem6fi  16466  eupth2lem3lem4fi  16468  eupth2lem3fi  16471  eupth2lemsfi  16473  eupth2fi  16474  eulerpathprum  16475  konigsberglem4  16486  depindlem1  16501  depindlem2  16502  depindlem3  16503  012of  16767  2o01f  16768  subctctexmid  16774  nnsf  16783  nninfalllem1  16786  nninffeq  16798  qdencn  16807  trilpolemclim  16820  trilpolemcl  16821  trilpolemisumle  16822  trilpolemeq1  16824  trilpolemlt1  16825  trilpo  16827  iswomni0  16836  redcwlpo  16840  dceqnconst  16846  dcapnconst  16847  nconstwlpolemgt0  16850  nconstwlpolem  16851  nconstwlpo  16852  neapmkv  16854