Theorem fveq2 5639

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 4091	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝑥 ↔ 𝐵𝐹𝑥))
2	1	iotabidv 5309	. 2 ⊢ (𝐴 = 𝐵 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐵𝐹𝑥))
3		df-fv 5334	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5334	. 2 ⊢ (𝐹‘𝐵) = (℩𝑥𝐵𝐹𝑥)
5	2, 3, 4	3eqtr4g 2289	1 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))

Syntax hints:   → wi 4   = wceq 1397   class class class wbr 4088  ℩cio 5284  ‘cfv 5326

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334

This theorem is referenced by:  fveq2i  5642  fveq2d  5643  2fveq3  5644  fvifdc  5661  dffn5imf  5701  fvelimab  5702  ssimaex  5707  fvco4  5718  fvmptssdm  5731  fvmptf  5739  eqfnfv2f  5748  fvelrn  5778  ralrnmpt  5789  rexrnmpt  5790  ffnfvf  5806  fmptco  5813  cofmpt  5816  fcompt  5817  fcoconst  5818  fnressn  5839  fressnfv  5840  fconstfvm  5871  foco2  5893  funiunfvdmf  5904  f1veqaeq  5909  dff13f  5910  f1fveq  5912  f1elima  5913  f1ocnvfv  5919  f1ocnvfvb  5920  fcofo  5924  cocan2  5928  fliftfun  5936  isorel  5948  isocnv  5951  isotr  5956  f1oiso2  5967  canth  5968  imbrov2fvoveq  6042  ffnov  6124  eqfnov  6127  fnovim  6129  fnrnov  6167  foov  6168  funimassov  6171  ovelimab  6172  suppssfv  6230  ofvalg  6244  ofrval  6245  offval2  6250  ofrfval2  6251  ofco  6253  caofinvl  6260  op1std  6310  op2ndd  6311  1stval2  6317  2ndval2  6318  unielxp  6336  reldm  6348  oprabco  6381  2ndconst  6386  f1o2ndf1  6392  mpoxopn0yelv  6404  mpoxopoveq  6405  smoel  6465  tfrlem1  6473  tfrlem3-2d  6477  tfrlem5  6479  tfrlem9  6484  tfr0dm  6487  tfrlemiubacc  6495  tfrlemi1  6497  tfrexlem  6499  tfr1onlemsucfn  6505  tfr1onlemsucaccv  6506  tfr1onlembxssdm  6508  tfr1onlembfn  6509  tfr1onlemubacc  6511  tfr1onlemaccex  6513  tfr1onlemres  6514  tfri1dALT  6516  tfrcllemsucfn  6518  tfrcllemsucaccv  6519  tfrcllembxssdm  6521  tfrcllembfn  6522  tfrcllemubacc  6524  tfrcllemaccex  6526  tfrcllemres  6527  tfrcldm  6528  tfrcl  6529  tfri3  6532  rdgtfr  6539  rdgss  6548  rdgisuc1  6549  rdgisucinc  6550  rdgon  6551  frecabex  6563  frecabcl  6564  frecfcllem  6569  frecsuclem  6571  frecsuc  6572  frecrdg  6573  oav  6621  omv  6622  oeiv  6623  fvixp  6871  cbvixp  6883  mptelixpg  6902  elixpsn  6903  dom2lem  6944  xpcomco  7009  xpmapen  7035  fidceq  7055  fieq0  7174  ordiso2  7233  djune  7276  updjudhcoinlf  7278  updjudhcoinrg  7279  updjud  7280  omp1eom  7293  0ct  7305  ctmlemr  7306  ctssdclemn0  7308  ctssdccl  7309  ctssdc  7311  enumctlemm  7312  nninfninc  7321  nnnninfeq  7326  nnnninfeq2  7327  enomnilem  7336  finomni  7338  fodjuomnilemdc  7342  fodju0  7345  fodjuomni  7347  ismkvnex  7353  fodjumkv  7358  nninfwlporlemd  7370  nninfwlpor  7372  exmidaclem  7422  cc1  7483  cc2lem  7484  cc2  7485  cc3  7486  mulpipq2  7590  genipv  7728  genpelxp  7730  addcanprleml  7833  addcanprlemu  7834  recexprlemm  7843  recexprlemdisj  7849  recexprlemloc  7850  recexprlem1ssl  7852  recexprlem1ssu  7853  cauappcvgprlemm  7864  cauappcvgprlemdisj  7870  cauappcvgprlemloc  7871  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  cauappcvgprlem1  7878  cauappcvgprlem2  7879  cauappcvgprlemlim  7880  cauappcvgpr  7881  caucvgprlemnkj  7885  caucvgprlemnbj  7886  caucvgprlemm  7887  caucvgprlemdisj  7893  caucvgprlemloc  7894  caucvgprlemcl  7895  caucvgprlemladdfu  7896  caucvgprlemladdrl  7897  caucvgprlem1  7898  caucvgprlem2  7899  caucvgpr  7901  caucvgprprlemell  7904  caucvgprprlemelu  7905  caucvgprprlemcbv  7906  caucvgprprlemval  7907  caucvgprprlemnkeqj  7909  caucvgprprlemnbj  7912  caucvgprprlemml  7913  caucvgprprlemmu  7914  caucvgprprlemopl  7916  caucvgprprlemlol  7917  caucvgprprlemopu  7918  caucvgprprlemloc  7922  caucvgprprlemclphr  7924  caucvgprprlemexbt  7925  caucvgprprlem1  7928  caucvgprprlem2  7929  caucvgsrlemcl  8008  caucvgsrlemfv  8010  caucvgsrlembound  8013  caucvgsrlemgt1  8014  caucvgsrlemoffval  8015  caucvgsrlemoffres  8019  caucvgsrlembnd  8020  caucvgsr  8021  axcaucvglemcau  8117  axcaucvglemres  8118  uz11  9778  cnref1o  9884  fzprval  10316  fztpval  10317  zsupcllemex  10489  infssuzex  10492  suprzubdc  10495  frec2uzuzd  10663  frec2uzltd  10664  frec2uzlt2d  10665  frecuzrdgrrn  10669  frec2uzrdg  10670  frecuzrdgtcl  10673  frecuzrdgg  10677  frecuzrdgfunlem  10680  frecfzennn  10687  seqeq1  10711  iseqovex  10719  seq3val  10721  seqvalcd  10722  seq3-1  10723  seqf  10725  seq3p1  10726  seqovcd  10728  seqp1cd  10731  seq3clss  10732  seq3fveq2  10736  seqfveq2g  10738  seqfveqg  10739  seq3fveq  10740  seq3feq  10741  seq3shft2  10742  seqshft2g  10743  monoord  10746  monoord2  10747  ser3mono  10748  seq3split  10749  seqsplitg  10750  seq3caopr3  10752  seqcaopr3g  10753  seq3caopr2  10754  seqcaopr2g  10755  iseqf1olemkle  10758  iseqf1olemklt  10759  iseqf1olemqval  10761  iseqf1olemqk  10768  iseqf1olemjpcl  10769  iseqf1olemqpcl  10770  iseqf1olemfvp  10771  seq3f1olemqsumkj  10772  seq3f1olemqsum  10774  seq3f1olemstep  10775  seq3f1olemp  10776  seq3f1oleml  10777  seq3f1o  10778  seqf1oglem2a  10779  seqf1og  10782  seq3id2  10787  seq3homo  10788  seq3z  10789  seqhomog  10791  seqfeq4g  10792  ser3ge0  10797  ser3le  10798  exp3vallem  10801  exp3val  10802  facp1  10991  faccl  10996  facdiv  10999  facwordi  11001  faclbnd  11002  facubnd  11006  bcval  11010  bcval5  11024  fz1eqb  11051  omgadd  11064  hashxp  11089  zfz1isolem1  11103  zfz1iso  11104  seq3coll  11105  eqwrd  11153  lswwrd  11159  lswex  11164  ccatfvalfi  11168  ccatval1  11173  ccatval2  11174  ccatalpha  11189  s1eq  11195  eqs1  11204  swrdval  11228  ccatopth2  11297  wrd2ind  11303  seq3shft  11398  reval  11409  replim  11419  cj11  11465  caucvgre  11541  cvg1nlemcau  11544  cvg1nlemres  11545  rexuz3  11550  absval  11561  resqrexlemover  11570  resqrexlemdecn  11572  resqrexlemlo  11573  resqrexlemcalc3  11576  resqrexlemnm  11578  resqrexlemcvg  11579  resqrexlemoverl  11581  resqrexlemglsq  11582  resqrexlemga  11583  resqrexlemsqa  11584  resqrexlemex  11585  abs00bd  11626  cau3lem  11674  caubnd2  11677  climconst  11850  climmpt  11860  climshftlemg  11862  climcn1  11868  climle  11894  climub  11904  climserle  11905  climcau  11907  climcvg1nlem  11909  climcvg1n  11910  serf0  11912  fsum3cvg  11938  summodclem3  11940  summodclem2a  11941  summodclem2  11942  summodc  11943  zsumdc  11944  fsum3  11947  fsumf1o  11950  fisumss  11952  fsum3cvg2  11954  fsum3ser  11957  fsumcl2lem  11958  fsumadd  11966  sumsnf  11969  isummulc2  11986  isumge0  11990  isumadd  11991  fsum2dlemstep  11994  fsummulc2  12008  fsumconst  12014  fsumrelem  12031  isumshft  12050  isum1p  12052  isumnn0nn  12053  isumrpcl  12054  isumlessdc  12056  cvgratnnlemnexp  12084  cvgratnnlemmn  12085  cvgratnnlemseq  12086  cvgratnnlemabsle  12087  cvgratnnlemfm  12089  cvgratnnlemrate  12090  cvgratnn  12091  cvgratz  12092  mertenslemi1  12095  mertenslem2  12096  mertensabs  12097  clim2prod  12099  prodfap0  12105  prodfrecap  12106  prodfdivap  12107  fproddccvg  12132  prodmodclem3  12135  prodmodclem2a  12136  prodmodclem2  12137  prodmodc  12138  zproddc  12139  fprodseq  12143  fprodf1o  12148  fprodssdc  12150  fprodmul  12151  prodsnf  12152  fprodfac  12175  fprodconst  12180  fprod2dlemstep  12182  eftvalcn  12217  ef0lem  12220  ege2le3  12231  efcj  12233  efaddlem  12234  eftlub  12250  efgt1p2  12255  reef11  12259  tanvalap  12268  efieq1re  12332  eirraplem  12337  dvdsabseq  12407  dvdsfac  12420  gcd0id  12549  nninfctlemfo  12610  nn0seqcvgd  12612  alginv  12618  algcvg  12619  algcvga  12622  algfx  12623  eucalglt  12628  lcmid  12651  qredeu  12668  prmfac1  12723  sqne2sq  12748  qnumdenbi  12763  dfphi2  12791  eulerthlemrprm  12800  eulerthlema  12801  eulerthlemh  12802  eulerthlemth  12803  phisum  12812  pcmpt  12915  pcfac  12922  1arithlem4  12938  elgz  12943  4sqlem4  12964  4sqlem12  12974  2expltfac  13011  ennnfonelemk  13020  ennnfonelemp1  13026  ennnfoneleminc  13031  ennnfonelemkh  13032  ennnfonelemhf1o  13033  ennnfonelemex  13034  ennnfonelemhom  13035  ennnfonelemrn  13039  ennnfonelemnn0  13042  ennnfonelemr  13043  ennnfonelemim  13044  ctinfomlemom  13047  ctinfom  13048  ctiunctlemfo  13059  nninfdclemlt  13071  nninfdclemf1  13072  sloteq  13086  ressvalsets  13146  topnvalg  13333  prdsbasprj  13364  prdsplusgfval  13366  prdsmulrfval  13368  imasex  13387  imasaddvallemg  13397  qusex  13407  xpsfrnel  13426  xpsfeq  13427  xpsval  13434  ismgm  13439  plusffvalg  13444  grpidvalg  13455  gsumfzval  13473  gsumval2  13479  issgrp  13485  ismnddef  13500  prdsidlem  13529  pws0g  13533  ismhm  13543  mhmex  13544  mhmlin  13549  issubm  13554  mhmeql  13574  isgrp  13588  grpn0  13617  grpinvfvalg  13624  grpsubfvalg  13627  grpsubval  13628  grpinv11  13651  grpinvnz  13653  prdsinvlem  13690  pwsinvg  13694  pwssub  13695  mhmlem  13700  mulgfvalg  13707  mulgsubcl  13722  mulgaddcomlem  13731  mulgneg2  13742  mulgass  13745  issubg  13759  subgex  13762  issubg2m  13775  issubg4m  13779  0subg  13785  isnsg  13788  releqgg  13806  eqgex  13807  eqgval  13809  isghm  13829  ghmlin  13834  ghmrn  13843  ghmeql  13853  f1ghm0to0  13858  iscmn  13879  mgpvalg  13935  isrng  13946  issrg  13977  srgfcl  13985  isring  14012  iscrng  14015  mulgass2  14070  opprvalg  14081  dvdsrvald  14106  isunitd  14119  invrfvald  14135  dvrfvald  14146  dvrvald  14147  isrhm  14171  rhmval  14186  isnzr  14194  islring  14205  issubrng  14212  issubrg  14234  rrgval  14275  isdomn  14282  aprval  14295  aprap  14299  islmod  14304  scaffvalg  14319  lsssetm  14369  lspfval  14401  sraval  14450  rlmvalg  14467  2idlval  14515  2idlvalg  14516  cnfldmulg  14589  zlmval  14640  znf1o  14664  psrlinv  14697  mplsubgfilemcl  14712  istps  14755  clsfval  14824  cnpval  14921  lmconst  14939  txcnp  14994  upxp  14995  uptx  14997  txlm  15002  lmcn2  15003  cnmpt11  15006  cnmpt11f  15007  cnmpt1t  15008  cnmpt21  15014  cnmpt21f  15015  cnmpt2t  15016  mopnval  15165  isxms  15174  isms  15176  comet  15222  mopnex  15228  xmetxp  15230  xmetxpbl  15231  txmetcnp  15241  txmetcn  15242  qtopbasss  15244  cncfi  15301  cncfmpt1f  15321  ivthinclemlm  15357  ivthinclemum  15358  ivthinclemlopn  15359  ivthinclemlr  15360  ivthinclemuopn  15361  ivthinclemur  15362  ivthinclemdisj  15363  ivthinclemloc  15364  ivthinc  15366  ivthdec  15367  ivthreinc  15368  cnlimci  15396  limccnpcntop  15398  eldvap  15405  dvcoapbr  15430  dvcj  15432  dvfre  15433  dvmptcjx  15447  dveflem  15449  elply2  15458  elplyd  15464  plymullem1  15471  plyadd  15474  plymul  15475  plycoeid3  15480  plycolemc  15481  plyco  15482  plycjlemc  15483  plycj  15484  dvply1  15488  sin0pilem2  15505  pilem3  15506  coseq0q4123  15557  coseq0negpitopi  15559  cos11  15576  logltb  15597  rpcxpef  15617  rplogbval  15668  mpodvdsmulf1o  15713  fsumdvdsmul  15714  zabsle1  15727  lgslem2  15729  lgslem3  15730  lgsfcl2  15734  lgsfle1  15737  lgsle1  15743  lgsdirprm  15762  lgseisenlem2  15799  lgsquadlem2  15806  2sqlem1  15842  2sqlem2  15843  mul2sq  15844  2sqlem3  15845  2sqlem9  15852  2sqlem10  15853  vtxvalg  15866  iedgvalg  15867  edgvalg  15909  edgopval  15912  edgstruct  15914  isuhgrm  15921  isushgrm  15922  isupgren  15945  isumgren  15955  isuspgren  16007  isusgren  16008  umgr2edg1  16059  usgredg2vlem1  16072  usgredg2vlem2  16073  ushgredgedg  16076  issubgr  16107  vtxdgfval  16138  vtxedgfi  16139  vtxdg0v  16144  vtxdumgrfival  16148  1loopgrvd0fi  16156  1hevtxdg0fi  16157  1hevtxdg1en  16158  wkslem1  16170  wkslem2  16171  wksfval  16172  iswlk  16173  uspgr2wlkeq  16215  uspgr2wlkeqi  16217  2wlklem  16226  trlsfvalg  16233  clwwlkg  16243  isclwwlk  16244  clwwlkccatlem  16250  clwwlkng  16255  clwwlkn2  16271  clwwlkext2edg  16272  umgr2cwwk2dif  16274  umgr2cwwkdifex  16275  clwwlknonmpo  16278  clwwlknonel  16282  clwwlknonex2lem2  16288  eupthsg  16295  iseupth  16297  eupthseg  16302  012of  16592  2o01f  16593  subctctexmid  16601  nnsf  16607  nninfalllem1  16610  nninffeq  16622  qdencn  16631  trilpolemclim  16640  trilpolemcl  16641  trilpolemisumle  16642  trilpolemeq1  16644  trilpolemlt1  16645  trilpo  16647  iswomni0  16655  redcwlpo  16659  dceqnconst  16664  dcapnconst  16665  nconstwlpolemgt0  16668  nconstwlpolem  16669  nconstwlpo  16670  neapmkv  16672