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  6515  mpoxopoveq  6516  smoel  6576  tfrlem1  6584  tfrlem3-2d  6588  tfrlem5  6590  tfrlem9  6595  tfr0dm  6598  tfrlemiubacc  6606  tfrlemi1  6608  tfrexlem  6610  tfr1onlemsucfn  6616  tfr1onlemsucaccv  6617  tfr1onlembxssdm  6619  tfr1onlembfn  6620  tfr1onlemubacc  6622  tfr1onlemaccex  6624  tfr1onlemres  6625  tfri1dALT  6627  tfrcllemsucfn  6629  tfrcllemsucaccv  6630  tfrcllembxssdm  6632  tfrcllembfn  6633  tfrcllemubacc  6635  tfrcllemaccex  6637  tfrcllemres  6638  tfrcldm  6639  tfrcl  6640  tfri3  6643  rdgtfr  6650  rdgss  6659  rdgisuc1  6660  rdgisucinc  6661  rdgon  6662  frecabex  6674  frecabcl  6675  frecfcllem  6680  frecsuclem  6682  frecsuc  6683  frecrdg  6684  oav  6732  omv  6733  oeiv  6734  fvixp  6991  cbvixp  7003  mptelixpg  7022  elixpsn  7023  dom2lem  7064  xpcomco  7130  xpmapen  7156  fidceq  7177  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  9960  cnref1o  10067  fzprval  10505  fztpval  10506  zsupcllemex  10679  infssuzex  10682  suprzubdc  10687  frec2uzuzd  10859  frec2uzltd  10860  frec2uzlt2d  10861  frecuzrdgrrn  10865  frec2uzrdg  10866  frecuzrdgtcl  10869  frecuzrdgg  10873  frecuzrdgfunlem  10876  frecfzennn  10883  seqeq1  10907  iseqovex  10915  seq3val  10917  seqvalcd  10918  seq3-1  10919  seqf  10921  seq3p1  10922  seqovcd  10924  seqp1cd  10927  seq3clss  10928  seq3fveq2  10932  seqfveq2g  10934  seqfveqg  10935  seq3fveq  10936  seq3feq  10937  seq3shft2  10938  seqshft2g  10939  monoord  10942  monoord2  10943  ser3mono  10944  seq3split  10945  seqsplitg  10946  seq3caopr3  10948  seqcaopr3g  10949  seq3caopr2  10950  seqcaopr2g  10951  iseqf1olemkle  10954  iseqf1olemklt  10955  iseqf1olemqval  10957  iseqf1olemqk  10964  iseqf1olemjpcl  10965  iseqf1olemqpcl  10966  iseqf1olemfvp  10967  seq3f1olemqsumkj  10968  seq3f1olemqsum  10970  seq3f1olemstep  10971  seq3f1olemp  10972  seq3f1oleml  10973  seq3f1o  10974  seqf1oglem2a  10975  seqf1og  10978  seq3id2  10983  seq3homo  10984  seq3z  10985  seqhomog  10987  seqfeq4g  10988  ser3ge0  10993  ser3le  10994  exp3vallem  10997  exp3val  10998  facp1  11189  faccl  11194  facdiv  11197  facwordi  11199  faclbnd  11200  facubnd  11204  bcval  11208  bcval5  11222  fz1eqb  11250  omgadd  11263  hashxp  11288  hashmap  11289  hashfibc  11304  hashf1lem1  11306  hashf1lem2  11307  hashf1  11308  zfz1isolem1  11313  zfz1iso  11314  seq3coll  11315  eqwrd  11366  lswwrd  11372  lswex  11377  ccatfvalfi  11381  ccatval1  11386  ccatval2  11387  ccatalpha  11402  s1eq  11408  eqs1  11417  swrdval  11441  ccatopth2  11510  wrd2ind  11516  seq3shft  11624  reval  11635  replim  11645  cj11  11692  caucvgre  11768  cvg1nlemcau  11771  cvg1nlemres  11772  rexuz3  11777  absval  11788  resqrexlemover  11797  resqrexlemdecn  11799  resqrexlemlo  11800  resqrexlemcalc3  11803  resqrexlemnm  11805  resqrexlemcvg  11806  resqrexlemoverl  11808  resqrexlemglsq  11809  resqrexlemga  11810  resqrexlemsqa  11811  resqrexlemex  11812  abs00bd  11853  cau3lem  11902  caubnd2  11905  fiidxsupcl  12017  climconst  12080  climmpt  12090  climshftlemg  12092  climcn1  12098  climle  12124  climub  12134  climserle  12135  climcau  12137  climcvg1nlem  12139  climcvg1n  12140  serf0  12142  fsum3cvg  12169  summodclem3  12171  summodclem2a  12172  summodclem2  12173  summodc  12174  zsumdc  12175  fsum3  12178  fsumf1o  12181  fisumss  12183  fsum3cvg2  12185  fsum3ser  12188  fsumcl2lem  12189  fsumadd  12197  sumsnf  12200  isummulc2  12217  isumge0  12221  isumadd  12222  fsum2dlemstep  12225  fsummulc2  12239  fsumconst  12245  fsumrelem  12262  isumshft  12281  isum1p  12283  isumnn0nn  12284  isumrpcl  12285  isumlessdc  12287  cvgratnnlemnexp  12315  cvgratnnlemmn  12316  cvgratnnlemseq  12317  cvgratnnlemabsle  12318  cvgratnnlemfm  12320  cvgratnnlemrate  12321  cvgratnn  12322  cvgratz  12323  mertenslemi1  12326  mertenslem2  12327  mertensabs  12328  clim2prod  12330  prodfap0  12336  prodfrecap  12337  prodfdivap  12338  fproddccvg  12363  prodmodclem3  12366  prodmodclem2a  12367  prodmodclem2  12368  prodmodc  12369  zproddc  12370  fprodseq  12374  fprodf1o  12379  fprodssdc  12381  fprodmul  12382  prodsnf  12383  fprodfac  12406  fprodconst  12411  fprod2dlemstep  12413  eftvalcn  12448  ef0lem  12451  ege2le3  12462  efcj  12464  efaddlem  12465  eftlub  12481  efgt1p2  12486  reef11  12490  tanvalap  12499  efieq1re  12563  eirraplem  12568  dvdsabseq  12638  dvdsfac  12651  gcd0id  12780  nninfctlemfo  12841  nn0seqcvgd  12843  alginv  12849  algcvg  12850  algcvga  12853  algfx  12854  eucalglt  12859  lcmid  12882  qredeu  12899  prmfac1  12955  sqne2sq  12981  qnumdenbi  12996  dfphi2  13026  eulerthlemrprm  13035  eulerthlema  13036  eulerthlemh  13037  eulerthlemth  13038  phisum  13047  pcmpt  13150  pcfac  13157  1arithlem4  13173  elgz  13178  4sqlem4  13199  4sqlem12  13209  2expltfac  13247  ballotfilem2  13285  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfileme  13293  ballotfilemefi  13294  ballotfilemodife  13297  ballotfilem4  13298  ballotfilemi  13300  ballotfilemic  13307  ballotfilem1c  13308  ballotfilemrval  13318  ballotfilemrc  13331  ballotfilemrinv  13334  ballotfilemth  13338  ballotfi  13339  ennnfonelemk  13348  ennnfonelemp1  13354  ennnfoneleminc  13359  ennnfonelemkh  13360  ennnfonelemhf1o  13361  ennnfonelemex  13362  ennnfonelemhom  13363  ennnfonelemrn  13367  ennnfonelemnn0  13370  ennnfonelemr  13371  ennnfonelemim  13372  ctinfomlemom  13375  ctinfom  13376  ctiunctlemfo  13387  nninfdclemlt  13399  nninfdclemf1  13400  sloteq  13414  ressvalsets  13475  topnvalg  13663  imasex  13684  imasaddvallemg  13694  qusex  13704  xpsfrnel  13723  xpsfeq  13724  ismgm  13735  plusffvalg  13740  grpidvalg  13751  gzsumfzval  13769  gzsumval2  13772  issgrp  13776  ismnddef  13789  ismhm  13826  mhmex  13827  mhmlin  13832  issubm  13837  mhmeql  13857  isgrp  13869  grpn0  13898  grpinvfvalg  13905  grpsubfvalg  13908  grpsubval  13909  grpinv11  13932  grpinvnz  13934  mhmlem  13975  mulgfvalg  13982  mulgsubcl  13997  mulgaddcomlem  14006  mulgneg2  14017  mulgass  14020  issubg  14034  subgex  14037  issubg2m  14050  issubg4m  14054  0subg  14060  isnsg  14063  releqgg  14081  eqgex  14082  eqgval  14084  isghm  14104  ghmlin  14109  ghmrn  14118  ghmeql  14128  f1ghm0to0  14133  cntzex  14149  cntrval  14150  cntzfval  14151  iscmn  14185  gsumresfi  14262  gsumconstcmn  14265  gsumcom2fi  14274  prdsbasprj  14288  prdsplusgfval  14290  prdsmulrfval  14292  prdsidlem  14299  prdsinvlem  14302  xpsval  14307  pws0g  14319  pwsinvg  14321  pwssub  14322  mgpvalg  14326  isrng  14339  issrg  14375  srgfcl  14383  isring  14410  iscrng  14413  mulgass2  14469  opprvalg  14482  dvdsrvald  14508  isunitd  14521  invrfvald  14537  dvrfvald  14548  dvrvald  14549  isrhm  14573  rhmval  14588  isnzr  14596  islring  14607  issubrng  14615  issubrg  14637  rrgval  14678  rrgsupp  14682  isdomn  14686  aprval  14699  aprap  14706  aprprop  14709  isdrngtap  14714  islmod  14735  scaffvalg  14751  lsssetm  14801  lspfval  14833  sraval  14882  rlmvalg  14899  2idlval  14947  2idlvalg  14948  cnfldmulg  15021  zlmval  15070  znf1o  15094  isassa  15110  aspval  15123  asclfval  15129  psrbaglefifi  15175  psrbagmaxlem1x  15181  psrbagmaxlem1y  15182  psrbagmax  15183  psrlinv  15203  psrlidmfi  15208  psrridmfi  15209  psrass1fi  15210  istps  15275  clsfval  15344  cnpval  15441  lmconst  15459  txcnp  15514  upxp  15515  uptx  15517  txlm  15522  lmcn2  15523  cnmpt11  15526  cnmpt11f  15527  cnmpt1t  15528  cnmpt21  15534  cnmpt21f  15535  cnmpt2t  15536  mopnval  15685  isxms  15694  isms  15696  comet  15742  mopnex  15748  xmetxp  15750  xmetxpbl  15751  txmetcnp  15761  txmetcn  15762  qtopbasss  15764  cncfi  15821  cncfmpt1f  15841  ivthinclemlm  15877  ivthinclemum  15878  ivthinclemlopn  15879  ivthinclemlr  15880  ivthinclemuopn  15881  ivthinclemur  15882  ivthinclemdisj  15883  ivthinclemloc  15884  ivthinc  15886  ivthdec  15887  ivthreinc  15888  cnlimci  15916  limccnpcntop  15918  eldvap  15925  dvcoapbr  15950  dvcj  15952  dvfre  15953  dvmptcjx  15967  dveflem  15969  elply2  15978  elplyd  15984  plymullem1  15991  plyadd  15994  plymul  15995  plycoeid3  16000  plycolemc  16001  plyco  16002  plycjlemc  16003  plycj  16004  dvply1  16008  sin0pilem2  16026  pilem3  16027  coseq0q4123  16078  coseq0negpitopi  16080  sineq0re  16093  cos11  16098  logltb  16121  logfac  16143  rpcxpef  16144  rplogbval  16198  pellexlem1  16246  pellexlem3  16248  efnnfsumcl  16256  chtprm  16278  efchtqdvds  16282  ppiqltx  16298  prmorcht  16299  mpodvdsmulf1o  16301  fsumdvdsmul  16302  chtqub  16313  bposlem5  16332  bposlem7  16334  bposlem8  16335  bposlem9  16336  zabsle1  16340  lgslem2  16342  lgslem3  16343  lgsfcl2  16347  lgsfle1  16350  lgsle1  16356  lgsdirprm  16375  lgseisenlem2  16412  lgsquadlem2  16419  2sqlem1  16455  2sqlem2  16456  mul2sq  16457  2sqlem3  16458  2sqlem9  16465  2sqlem10  16466  vtxvalg  16479  iedgvalg  16480  edgvalg  16522  edgopval  16525  edgstruct  16527  isuhgrm  16534  isushgrm  16535  isupgren  16558  isumgren  16568  isuspgren  16620  isusgren  16621  umgr2edg1  16672  usgredg2vlem1  16685  usgredg2vlem2  16686  ushgredgedg  16689  issubgr  16720  vtxdgfval  16751  vtxedgfi  16752  vtxdg0v  16757  vtxdumgrfival  16761  1loopgrvd0fi  16769  1hevtxdg0fi  16770  1hevtxdg1en  16771  wkslem1  16783  wkslem2  16784  wksfval  16785  iswlk  16786  uspgr2wlkeq  16828  uspgr2wlkeqi  16830  2wlklem  16839  trlsfvalg  16846  clwwlkg  16856  isclwwlk  16857  clwwlkccatlem  16863  clwwlkng  16868  clwwlkn2  16884  clwwlkext2edg  16885  umgr2cwwk2dif  16887  umgr2cwwkdifex  16888  clwwlknonmpo  16891  clwwlknonel  16895  clwwlknonex2lem2  16901  eupthsg  16908  iseupth  16910  eupthseg  16915  eupth2lem3lem3fi  16933  eupth2lem3lem6fi  16934  eupth2lem3lem4fi  16936  eupth2lem3fi  16939  eupth2lemsfi  16941  eupth2fi  16942  eulerpathprum  16943  konigsberglem4  16954  depindlem1  16969  depindlem2  16970  depindlem3  16971  012of  17245  2o01f  17246  subctctexmid  17252  nnsf  17271  nninfalllem1  17274  nninffeq  17286  qdencn  17295  trilpolemclim  17309  trilpolemcl  17310  trilpolemisumle  17311  trilpolemeq1  17313  trilpolemlt1  17314  trilpo  17316  iswomni0  17325  redcwlpo  17329  dceqnconst  17334  dcapnconst  17335  nconstwlpolemgt0  17338  nconstwlpolem  17339  nconstwlpo  17340  neapmkv  17342