Theorem fveq2 5626

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 4085	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝑥 ↔ 𝐵𝐹𝑥))
2	1	iotabidv 5300	. 2 ⊢ (𝐴 = 𝐵 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐵𝐹𝑥))
3		df-fv 5325	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5325	. 2 ⊢ (𝐹‘𝐵) = (℩𝑥𝐵𝐹𝑥)
5	2, 3, 4	3eqtr4g 2287	1 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))

Syntax hints:   → wi 4   = wceq 1395   class class class wbr 4082  ℩cio 5275  ‘cfv 5317

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 3888  df-br 4083  df-iota 5277  df-fv 5325

This theorem is referenced by:  fveq2i  5629  fveq2d  5630  2fveq3  5631  fvifdc  5648  dffn5imf  5688  fvelimab  5689  ssimaex  5694  fvco4  5705  fvmptssdm  5718  fvmptf  5726  eqfnfv2f  5735  fvelrn  5765  ralrnmpt  5776  rexrnmpt  5777  ffnfvf  5793  fmptco  5800  cofmpt  5803  fcompt  5804  fcoconst  5805  fnressn  5824  fressnfv  5825  fconstfvm  5856  foco2  5876  funiunfvdmf  5887  f1veqaeq  5892  dff13f  5893  f1fveq  5895  f1elima  5896  f1ocnvfv  5902  f1ocnvfvb  5903  fcofo  5907  cocan2  5911  fliftfun  5919  isorel  5931  isocnv  5934  isotr  5939  f1oiso2  5950  canth  5951  imbrov2fvoveq  6025  ffnov  6107  eqfnov  6110  fnovim  6112  fnrnov  6150  foov  6151  funimassov  6154  ovelimab  6155  suppssfv  6212  ofvalg  6226  ofrval  6227  offval2  6232  ofrfval2  6233  ofco  6235  caofinvl  6242  op1std  6292  op2ndd  6293  1stval2  6299  2ndval2  6300  unielxp  6318  reldm  6330  oprabco  6361  2ndconst  6366  f1o2ndf1  6372  mpoxopn0yelv  6383  mpoxopoveq  6384  smoel  6444  tfrlem1  6452  tfrlem3-2d  6456  tfrlem5  6458  tfrlem9  6463  tfr0dm  6466  tfrlemiubacc  6474  tfrlemi1  6476  tfrexlem  6478  tfr1onlemsucfn  6484  tfr1onlemsucaccv  6485  tfr1onlembxssdm  6487  tfr1onlembfn  6488  tfr1onlemubacc  6490  tfr1onlemaccex  6492  tfr1onlemres  6493  tfri1dALT  6495  tfrcllemsucfn  6497  tfrcllemsucaccv  6498  tfrcllembxssdm  6500  tfrcllembfn  6501  tfrcllemubacc  6503  tfrcllemaccex  6505  tfrcllemres  6506  tfrcldm  6507  tfrcl  6508  tfri3  6511  rdgtfr  6518  rdgss  6527  rdgisuc1  6528  rdgisucinc  6529  rdgon  6530  frecabex  6542  frecabcl  6543  frecfcllem  6548  frecsuclem  6550  frecsuc  6551  frecrdg  6552  oav  6598  omv  6599  oeiv  6600  fvixp  6848  cbvixp  6860  mptelixpg  6879  elixpsn  6880  dom2lem  6921  xpcomco  6981  xpmapen  7007  fidceq  7027  fieq0  7139  ordiso2  7198  djune  7241  updjudhcoinlf  7243  updjudhcoinrg  7244  updjud  7245  omp1eom  7258  0ct  7270  ctmlemr  7271  ctssdclemn0  7273  ctssdccl  7274  ctssdc  7276  enumctlemm  7277  nninfninc  7286  nnnninfeq  7291  nnnninfeq2  7292  enomnilem  7301  finomni  7303  fodjuomnilemdc  7307  fodju0  7310  fodjuomni  7312  ismkvnex  7318  fodjumkv  7323  nninfwlporlemd  7335  nninfwlpor  7337  exmidaclem  7386  cc1  7447  cc2lem  7448  cc2  7449  cc3  7450  mulpipq2  7554  genipv  7692  genpelxp  7694  addcanprleml  7797  addcanprlemu  7798  recexprlemm  7807  recexprlemdisj  7813  recexprlemloc  7814  recexprlem1ssl  7816  recexprlem1ssu  7817  cauappcvgprlemm  7828  cauappcvgprlemdisj  7834  cauappcvgprlemloc  7835  cauappcvgprlemladdru  7839  cauappcvgprlemladdrl  7840  cauappcvgprlem1  7842  cauappcvgprlem2  7843  cauappcvgprlemlim  7844  cauappcvgpr  7845  caucvgprlemnkj  7849  caucvgprlemnbj  7850  caucvgprlemm  7851  caucvgprlemdisj  7857  caucvgprlemloc  7858  caucvgprlemcl  7859  caucvgprlemladdfu  7860  caucvgprlemladdrl  7861  caucvgprlem1  7862  caucvgprlem2  7863  caucvgpr  7865  caucvgprprlemell  7868  caucvgprprlemelu  7869  caucvgprprlemcbv  7870  caucvgprprlemval  7871  caucvgprprlemnkeqj  7873  caucvgprprlemnbj  7876  caucvgprprlemml  7877  caucvgprprlemmu  7878  caucvgprprlemopl  7880  caucvgprprlemlol  7881  caucvgprprlemopu  7882  caucvgprprlemloc  7886  caucvgprprlemclphr  7888  caucvgprprlemexbt  7889  caucvgprprlem1  7892  caucvgprprlem2  7893  caucvgsrlemcl  7972  caucvgsrlemfv  7974  caucvgsrlembound  7977  caucvgsrlemgt1  7978  caucvgsrlemoffval  7979  caucvgsrlemoffres  7983  caucvgsrlembnd  7984  caucvgsr  7985  axcaucvglemcau  8081  axcaucvglemres  8082  uz11  9741  cnref1o  9842  fzprval  10274  fztpval  10275  zsupcllemex  10445  infssuzex  10448  suprzubdc  10451  frec2uzuzd  10619  frec2uzltd  10620  frec2uzlt2d  10621  frecuzrdgrrn  10625  frec2uzrdg  10626  frecuzrdgtcl  10629  frecuzrdgg  10633  frecuzrdgfunlem  10636  frecfzennn  10643  seqeq1  10667  iseqovex  10675  seq3val  10677  seqvalcd  10678  seq3-1  10679  seqf  10681  seq3p1  10682  seqovcd  10684  seqp1cd  10687  seq3clss  10688  seq3fveq2  10692  seqfveq2g  10694  seqfveqg  10695  seq3fveq  10696  seq3feq  10697  seq3shft2  10698  seqshft2g  10699  monoord  10702  monoord2  10703  ser3mono  10704  seq3split  10705  seqsplitg  10706  seq3caopr3  10708  seqcaopr3g  10709  seq3caopr2  10710  seqcaopr2g  10711  iseqf1olemkle  10714  iseqf1olemklt  10715  iseqf1olemqval  10717  iseqf1olemqk  10724  iseqf1olemjpcl  10725  iseqf1olemqpcl  10726  iseqf1olemfvp  10727  seq3f1olemqsumkj  10728  seq3f1olemqsum  10730  seq3f1olemstep  10731  seq3f1olemp  10732  seq3f1oleml  10733  seq3f1o  10734  seqf1oglem2a  10735  seqf1og  10738  seq3id2  10743  seq3homo  10744  seq3z  10745  seqhomog  10747  seqfeq4g  10748  ser3ge0  10753  ser3le  10754  exp3vallem  10757  exp3val  10758  facp1  10947  faccl  10952  facdiv  10955  facwordi  10957  faclbnd  10958  facubnd  10962  bcval  10966  bcval5  10980  fz1eqb  11007  omgadd  11019  hashxp  11043  zfz1isolem1  11057  zfz1iso  11058  seq3coll  11059  eqwrd  11107  lswwrd  11113  lswex  11118  ccatfvalfi  11122  ccatval1  11127  ccatval2  11128  s1eq  11147  eqs1  11156  swrdval  11175  ccatopth2  11244  wrd2ind  11250  seq3shft  11344  reval  11355  replim  11365  cj11  11411  caucvgre  11487  cvg1nlemcau  11490  cvg1nlemres  11491  rexuz3  11496  absval  11507  resqrexlemover  11516  resqrexlemdecn  11518  resqrexlemlo  11519  resqrexlemcalc3  11522  resqrexlemnm  11524  resqrexlemcvg  11525  resqrexlemoverl  11527  resqrexlemglsq  11528  resqrexlemga  11529  resqrexlemsqa  11530  resqrexlemex  11531  abs00bd  11572  cau3lem  11620  caubnd2  11623  climconst  11796  climmpt  11806  climshftlemg  11808  climcn1  11814  climle  11840  climub  11850  climserle  11851  climcau  11853  climcvg1nlem  11855  climcvg1n  11856  serf0  11858  fsum3cvg  11884  summodclem3  11886  summodclem2a  11887  summodclem2  11888  summodc  11889  zsumdc  11890  fsum3  11893  fsumf1o  11896  fisumss  11898  fsum3cvg2  11900  fsum3ser  11903  fsumcl2lem  11904  fsumadd  11912  sumsnf  11915  isummulc2  11932  isumge0  11936  isumadd  11937  fsum2dlemstep  11940  fsummulc2  11954  fsumconst  11960  fsumrelem  11977  isumshft  11996  isum1p  11998  isumnn0nn  11999  isumrpcl  12000  isumlessdc  12002  cvgratnnlemnexp  12030  cvgratnnlemmn  12031  cvgratnnlemseq  12032  cvgratnnlemabsle  12033  cvgratnnlemfm  12035  cvgratnnlemrate  12036  cvgratnn  12037  cvgratz  12038  mertenslemi1  12041  mertenslem2  12042  mertensabs  12043  clim2prod  12045  prodfap0  12051  prodfrecap  12052  prodfdivap  12053  fproddccvg  12078  prodmodclem3  12081  prodmodclem2a  12082  prodmodclem2  12083  prodmodc  12084  zproddc  12085  fprodseq  12089  fprodf1o  12094  fprodssdc  12096  fprodmul  12097  prodsnf  12098  fprodfac  12121  fprodconst  12126  fprod2dlemstep  12128  eftvalcn  12163  ef0lem  12166  ege2le3  12177  efcj  12179  efaddlem  12180  eftlub  12196  efgt1p2  12201  reef11  12205  tanvalap  12214  efieq1re  12278  eirraplem  12283  dvdsabseq  12353  dvdsfac  12366  gcd0id  12495  nninfctlemfo  12556  nn0seqcvgd  12558  alginv  12564  algcvg  12565  algcvga  12568  algfx  12569  eucalglt  12574  lcmid  12597  qredeu  12614  prmfac1  12669  sqne2sq  12694  qnumdenbi  12709  dfphi2  12737  eulerthlemrprm  12746  eulerthlema  12747  eulerthlemh  12748  eulerthlemth  12749  phisum  12758  pcmpt  12861  pcfac  12868  1arithlem4  12884  elgz  12889  4sqlem4  12910  4sqlem12  12920  2expltfac  12957  ennnfonelemk  12966  ennnfonelemp1  12972  ennnfoneleminc  12977  ennnfonelemkh  12978  ennnfonelemhf1o  12979  ennnfonelemex  12980  ennnfonelemhom  12981  ennnfonelemrn  12985  ennnfonelemnn0  12988  ennnfonelemr  12989  ennnfonelemim  12990  ctinfomlemom  12993  ctinfom  12994  ctiunctlemfo  13005  nninfdclemlt  13017  nninfdclemf1  13018  sloteq  13032  ressvalsets  13092  topnvalg  13279  prdsbasprj  13310  prdsplusgfval  13312  prdsmulrfval  13314  imasex  13333  imasaddvallemg  13343  qusex  13353  xpsfrnel  13372  xpsfeq  13373  xpsval  13380  ismgm  13385  plusffvalg  13390  grpidvalg  13401  gsumfzval  13419  gsumval2  13425  issgrp  13431  ismnddef  13446  prdsidlem  13475  pws0g  13479  ismhm  13489  mhmex  13490  mhmlin  13495  issubm  13500  mhmeql  13520  isgrp  13534  grpn0  13563  grpinvfvalg  13570  grpsubfvalg  13573  grpsubval  13574  grpinv11  13597  grpinvnz  13599  prdsinvlem  13636  pwsinvg  13640  pwssub  13641  mhmlem  13646  mulgfvalg  13653  mulgsubcl  13668  mulgaddcomlem  13677  mulgneg2  13688  mulgass  13691  issubg  13705  subgex  13708  issubg2m  13721  issubg4m  13725  0subg  13731  isnsg  13734  releqgg  13752  eqgex  13753  eqgval  13755  isghm  13775  ghmlin  13780  ghmrn  13789  ghmeql  13799  f1ghm0to0  13804  iscmn  13825  mgpvalg  13881  isrng  13892  issrg  13923  srgfcl  13931  isring  13958  iscrng  13961  mulgass2  14016  opprvalg  14027  reldvdsrsrg  14050  dvdsrvald  14051  isunitd  14064  invrfvald  14080  dvrfvald  14091  dvrvald  14092  isrhm  14116  rhmval  14131  isnzr  14139  islring  14150  issubrng  14157  issubrg  14179  rrgval  14220  isdomn  14227  aprval  14240  aprap  14244  islmod  14249  scaffvalg  14264  lsssetm  14314  lspfval  14346  sraval  14395  rlmvalg  14412  2idlval  14460  2idlvalg  14461  cnfldmulg  14534  zlmval  14585  znf1o  14609  psrlinv  14642  mplsubgfilemcl  14657  istps  14700  clsfval  14769  cnpval  14866  lmconst  14884  txcnp  14939  upxp  14940  uptx  14942  txlm  14947  lmcn2  14948  cnmpt11  14951  cnmpt11f  14952  cnmpt1t  14953  cnmpt21  14959  cnmpt21f  14960  cnmpt2t  14961  mopnval  15110  isxms  15119  isms  15121  comet  15167  mopnex  15173  xmetxp  15175  xmetxpbl  15176  txmetcnp  15186  txmetcn  15187  qtopbasss  15189  cncfi  15246  cncfmpt1f  15266  ivthinclemlm  15302  ivthinclemum  15303  ivthinclemlopn  15304  ivthinclemlr  15305  ivthinclemuopn  15306  ivthinclemur  15307  ivthinclemdisj  15308  ivthinclemloc  15309  ivthinc  15311  ivthdec  15312  ivthreinc  15313  cnlimci  15341  limccnpcntop  15343  eldvap  15350  dvcoapbr  15375  dvcj  15377  dvfre  15378  dvmptcjx  15392  dveflem  15394  elply2  15403  elplyd  15409  plymullem1  15416  plyadd  15419  plymul  15420  plycoeid3  15425  plycolemc  15426  plyco  15427  plycjlemc  15428  plycj  15429  dvply1  15433  sin0pilem2  15450  pilem3  15451  coseq0q4123  15502  coseq0negpitopi  15504  cos11  15521  logltb  15542  rpcxpef  15562  rplogbval  15613  mpodvdsmulf1o  15658  fsumdvdsmul  15659  zabsle1  15672  lgslem2  15674  lgslem3  15675  lgsfcl2  15679  lgsfle1  15682  lgsle1  15688  lgsdirprm  15707  lgseisenlem2  15744  lgsquadlem2  15751  2sqlem1  15787  2sqlem2  15788  mul2sq  15789  2sqlem3  15790  2sqlem9  15797  2sqlem10  15798  vtxvalg  15811  iedgvalg  15812  edgvalg  15854  edgopval  15856  edgstruct  15858  isuhgrm  15865  isushgrm  15866  isupgren  15889  isumgren  15899  isuspgren  15949  isusgren  15950  umgr2edg1  16001  usgredg2vlem1  16014  usgredg2vlem2  16015  ushgredgedg  16018  wkslem1  16026  wkslem2  16027  wksfval  16028  iswlk  16029  012of  16316  2o01f  16317  subctctexmid  16325  nnsf  16330  nninfalllem1  16333  nninffeq  16345  qdencn  16354  trilpolemclim  16363  trilpolemcl  16364  trilpolemisumle  16365  trilpolemeq1  16367  trilpolemlt1  16368  trilpo  16370  iswomni0  16378  redcwlpo  16382  dceqnconst  16387  dcapnconst  16388  nconstwlpolemgt0  16391  nconstwlpolem  16392  nconstwlpo  16393  neapmkv  16395