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  fsn2g  5822  fnressn  5840  fressnfv  5841  fconstfvm  5872  foco2  5894  funiunfvdmf  5905  f1veqaeq  5910  dff13f  5911  f1fveq  5913  f1elima  5914  f1ocnvfv  5920  f1ocnvfvb  5921  fcofo  5925  cocan2  5929  fliftfun  5937  isorel  5949  isocnv  5952  isotr  5957  f1oiso2  5968  canth  5969  imbrov2fvoveq  6043  ffnov  6125  eqfnov  6128  fnovim  6130  fnrnov  6168  foov  6169  funimassov  6172  ovelimab  6173  suppssfv  6231  ofvalg  6245  ofrval  6246  offval2  6251  ofrfval2  6252  ofco  6254  caofinvl  6261  op1std  6311  op2ndd  6312  1stval2  6318  2ndval2  6319  unielxp  6337  reldm  6349  oprabco  6382  2ndconst  6387  f1o2ndf1  6393  mpoxopn0yelv  6405  mpoxopoveq  6406  smoel  6466  tfrlem1  6474  tfrlem3-2d  6478  tfrlem5  6480  tfrlem9  6485  tfr0dm  6488  tfrlemiubacc  6496  tfrlemi1  6498  tfrexlem  6500  tfr1onlemsucfn  6506  tfr1onlemsucaccv  6507  tfr1onlembxssdm  6509  tfr1onlembfn  6510  tfr1onlemubacc  6512  tfr1onlemaccex  6514  tfr1onlemres  6515  tfri1dALT  6517  tfrcllemsucfn  6519  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllembfn  6523  tfrcllemubacc  6525  tfrcllemaccex  6527  tfrcllemres  6528  tfrcldm  6529  tfrcl  6530  tfri3  6533  rdgtfr  6540  rdgss  6549  rdgisuc1  6550  rdgisucinc  6551  rdgon  6552  frecabex  6564  frecabcl  6565  frecfcllem  6570  frecsuclem  6572  frecsuc  6573  frecrdg  6574  oav  6622  omv  6623  oeiv  6624  fvixp  6872  cbvixp  6884  mptelixpg  6903  elixpsn  6904  dom2lem  6945  xpcomco  7010  xpmapen  7036  fidceq  7056  fieq0  7175  ordiso2  7234  djune  7277  updjudhcoinlf  7279  updjudhcoinrg  7280  updjud  7281  omp1eom  7294  0ct  7306  ctmlemr  7307  ctssdclemn0  7309  ctssdccl  7310  ctssdc  7312  enumctlemm  7313  nninfninc  7322  nnnninfeq  7327  nnnninfeq2  7328  enomnilem  7337  finomni  7339  fodjuomnilemdc  7343  fodju0  7346  fodjuomni  7348  ismkvnex  7354  fodjumkv  7359  nninfwlporlemd  7371  nninfwlpor  7373  exmidaclem  7423  cc1  7484  cc2lem  7485  cc2  7486  cc3  7487  mulpipq2  7591  genipv  7729  genpelxp  7731  addcanprleml  7834  addcanprlemu  7835  recexprlemm  7844  recexprlemdisj  7850  recexprlemloc  7851  recexprlem1ssl  7853  recexprlem1ssu  7854  cauappcvgprlemm  7865  cauappcvgprlemdisj  7871  cauappcvgprlemloc  7872  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgprlem1  7879  cauappcvgprlem2  7880  cauappcvgprlemlim  7881  cauappcvgpr  7882  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemm  7888  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprlemcl  7896  caucvgprlemladdfu  7897  caucvgprlemladdrl  7898  caucvgprlem1  7899  caucvgprlem2  7900  caucvgpr  7902  caucvgprprlemell  7905  caucvgprprlemelu  7906  caucvgprprlemcbv  7907  caucvgprprlemval  7908  caucvgprprlemnkeqj  7910  caucvgprprlemnbj  7913  caucvgprprlemml  7914  caucvgprprlemmu  7915  caucvgprprlemopl  7917  caucvgprprlemlol  7918  caucvgprprlemopu  7919  caucvgprprlemloc  7923  caucvgprprlemclphr  7925  caucvgprprlemexbt  7926  caucvgprprlem1  7929  caucvgprprlem2  7930  caucvgsrlemcl  8009  caucvgsrlemfv  8011  caucvgsrlembound  8014  caucvgsrlemgt1  8015  caucvgsrlemoffval  8016  caucvgsrlemoffres  8020  caucvgsrlembnd  8021  caucvgsr  8022  axcaucvglemcau  8118  axcaucvglemres  8119  uz11  9779  cnref1o  9885  fzprval  10317  fztpval  10318  zsupcllemex  10491  infssuzex  10494  suprzubdc  10497  frec2uzuzd  10665  frec2uzltd  10666  frec2uzlt2d  10667  frecuzrdgrrn  10671  frec2uzrdg  10672  frecuzrdgtcl  10675  frecuzrdgg  10679  frecuzrdgfunlem  10682  frecfzennn  10689  seqeq1  10713  iseqovex  10721  seq3val  10723  seqvalcd  10724  seq3-1  10725  seqf  10727  seq3p1  10728  seqovcd  10730  seqp1cd  10733  seq3clss  10734  seq3fveq2  10738  seqfveq2g  10740  seqfveqg  10741  seq3fveq  10742  seq3feq  10743  seq3shft2  10744  seqshft2g  10745  monoord  10748  monoord2  10749  ser3mono  10750  seq3split  10751  seqsplitg  10752  seq3caopr3  10754  seqcaopr3g  10755  seq3caopr2  10756  seqcaopr2g  10757  iseqf1olemkle  10760  iseqf1olemklt  10761  iseqf1olemqval  10763  iseqf1olemqk  10770  iseqf1olemjpcl  10771  iseqf1olemqpcl  10772  iseqf1olemfvp  10773  seq3f1olemqsumkj  10774  seq3f1olemqsum  10776  seq3f1olemstep  10777  seq3f1olemp  10778  seq3f1oleml  10779  seq3f1o  10780  seqf1oglem2a  10781  seqf1og  10784  seq3id2  10789  seq3homo  10790  seq3z  10791  seqhomog  10793  seqfeq4g  10794  ser3ge0  10799  ser3le  10800  exp3vallem  10803  exp3val  10804  facp1  10993  faccl  10998  facdiv  11001  facwordi  11003  faclbnd  11004  facubnd  11008  bcval  11012  bcval5  11026  fz1eqb  11053  omgadd  11066  hashxp  11091  zfz1isolem1  11105  zfz1iso  11106  seq3coll  11107  eqwrd  11158  lswwrd  11164  lswex  11169  ccatfvalfi  11173  ccatval1  11178  ccatval2  11179  ccatalpha  11194  s1eq  11200  eqs1  11209  swrdval  11233  ccatopth2  11302  wrd2ind  11308  seq3shft  11403  reval  11414  replim  11424  cj11  11470  caucvgre  11546  cvg1nlemcau  11549  cvg1nlemres  11550  rexuz3  11555  absval  11566  resqrexlemover  11575  resqrexlemdecn  11577  resqrexlemlo  11578  resqrexlemcalc3  11581  resqrexlemnm  11583  resqrexlemcvg  11584  resqrexlemoverl  11586  resqrexlemglsq  11587  resqrexlemga  11588  resqrexlemsqa  11589  resqrexlemex  11590  abs00bd  11631  cau3lem  11679  caubnd2  11682  climconst  11855  climmpt  11865  climshftlemg  11867  climcn1  11873  climle  11899  climub  11909  climserle  11910  climcau  11912  climcvg1nlem  11914  climcvg1n  11915  serf0  11917  fsum3cvg  11944  summodclem3  11946  summodclem2a  11947  summodclem2  11948  summodc  11949  zsumdc  11950  fsum3  11953  fsumf1o  11956  fisumss  11958  fsum3cvg2  11960  fsum3ser  11963  fsumcl2lem  11964  fsumadd  11972  sumsnf  11975  isummulc2  11992  isumge0  11996  isumadd  11997  fsum2dlemstep  12000  fsummulc2  12014  fsumconst  12020  fsumrelem  12037  isumshft  12056  isum1p  12058  isumnn0nn  12059  isumrpcl  12060  isumlessdc  12062  cvgratnnlemnexp  12090  cvgratnnlemmn  12091  cvgratnnlemseq  12092  cvgratnnlemabsle  12093  cvgratnnlemfm  12095  cvgratnnlemrate  12096  cvgratnn  12097  cvgratz  12098  mertenslemi1  12101  mertenslem2  12102  mertensabs  12103  clim2prod  12105  prodfap0  12111  prodfrecap  12112  prodfdivap  12113  fproddccvg  12138  prodmodclem3  12141  prodmodclem2a  12142  prodmodclem2  12143  prodmodc  12144  zproddc  12145  fprodseq  12149  fprodf1o  12154  fprodssdc  12156  fprodmul  12157  prodsnf  12158  fprodfac  12181  fprodconst  12186  fprod2dlemstep  12188  eftvalcn  12223  ef0lem  12226  ege2le3  12237  efcj  12239  efaddlem  12240  eftlub  12256  efgt1p2  12261  reef11  12265  tanvalap  12274  efieq1re  12338  eirraplem  12343  dvdsabseq  12413  dvdsfac  12426  gcd0id  12555  nninfctlemfo  12616  nn0seqcvgd  12618  alginv  12624  algcvg  12625  algcvga  12628  algfx  12629  eucalglt  12634  lcmid  12657  qredeu  12674  prmfac1  12729  sqne2sq  12754  qnumdenbi  12769  dfphi2  12797  eulerthlemrprm  12806  eulerthlema  12807  eulerthlemh  12808  eulerthlemth  12809  phisum  12818  pcmpt  12921  pcfac  12928  1arithlem4  12944  elgz  12949  4sqlem4  12970  4sqlem12  12980  2expltfac  13017  ennnfonelemk  13026  ennnfonelemp1  13032  ennnfoneleminc  13037  ennnfonelemkh  13038  ennnfonelemhf1o  13039  ennnfonelemex  13040  ennnfonelemhom  13041  ennnfonelemrn  13045  ennnfonelemnn0  13048  ennnfonelemr  13049  ennnfonelemim  13050  ctinfomlemom  13053  ctinfom  13054  ctiunctlemfo  13065  nninfdclemlt  13077  nninfdclemf1  13078  sloteq  13092  ressvalsets  13152  topnvalg  13339  prdsbasprj  13370  prdsplusgfval  13372  prdsmulrfval  13374  imasex  13393  imasaddvallemg  13403  qusex  13413  xpsfrnel  13432  xpsfeq  13433  xpsval  13440  ismgm  13445  plusffvalg  13450  grpidvalg  13461  gsumfzval  13479  gsumval2  13485  issgrp  13491  ismnddef  13506  prdsidlem  13535  pws0g  13539  ismhm  13549  mhmex  13550  mhmlin  13555  issubm  13560  mhmeql  13580  isgrp  13594  grpn0  13623  grpinvfvalg  13630  grpsubfvalg  13633  grpsubval  13634  grpinv11  13657  grpinvnz  13659  prdsinvlem  13696  pwsinvg  13700  pwssub  13701  mhmlem  13706  mulgfvalg  13713  mulgsubcl  13728  mulgaddcomlem  13737  mulgneg2  13748  mulgass  13751  issubg  13765  subgex  13768  issubg2m  13781  issubg4m  13785  0subg  13791  isnsg  13794  releqgg  13812  eqgex  13813  eqgval  13815  isghm  13835  ghmlin  13840  ghmrn  13849  ghmeql  13859  f1ghm0to0  13864  iscmn  13885  mgpvalg  13942  isrng  13953  issrg  13984  srgfcl  13992  isring  14019  iscrng  14022  mulgass2  14077  opprvalg  14088  dvdsrvald  14113  isunitd  14126  invrfvald  14142  dvrfvald  14153  dvrvald  14154  isrhm  14178  rhmval  14193  isnzr  14201  islring  14212  issubrng  14219  issubrg  14241  rrgval  14282  isdomn  14289  aprval  14302  aprap  14306  islmod  14311  scaffvalg  14326  lsssetm  14376  lspfval  14408  sraval  14457  rlmvalg  14474  2idlval  14522  2idlvalg  14523  cnfldmulg  14596  zlmval  14647  znf1o  14671  psrlinv  14704  mplsubgfilemcl  14719  istps  14762  clsfval  14831  cnpval  14928  lmconst  14946  txcnp  15001  upxp  15002  uptx  15004  txlm  15009  lmcn2  15010  cnmpt11  15013  cnmpt11f  15014  cnmpt1t  15015  cnmpt21  15021  cnmpt21f  15022  cnmpt2t  15023  mopnval  15172  isxms  15181  isms  15183  comet  15229  mopnex  15235  xmetxp  15237  xmetxpbl  15238  txmetcnp  15248  txmetcn  15249  qtopbasss  15251  cncfi  15308  cncfmpt1f  15328  ivthinclemlm  15364  ivthinclemum  15365  ivthinclemlopn  15366  ivthinclemlr  15367  ivthinclemuopn  15368  ivthinclemur  15369  ivthinclemdisj  15370  ivthinclemloc  15371  ivthinc  15373  ivthdec  15374  ivthreinc  15375  cnlimci  15403  limccnpcntop  15405  eldvap  15412  dvcoapbr  15437  dvcj  15439  dvfre  15440  dvmptcjx  15454  dveflem  15456  elply2  15465  elplyd  15471  plymullem1  15478  plyadd  15481  plymul  15482  plycoeid3  15487  plycolemc  15488  plyco  15489  plycjlemc  15490  plycj  15491  dvply1  15495  sin0pilem2  15512  pilem3  15513  coseq0q4123  15564  coseq0negpitopi  15566  cos11  15583  logltb  15604  rpcxpef  15624  rplogbval  15675  mpodvdsmulf1o  15720  fsumdvdsmul  15721  zabsle1  15734  lgslem2  15736  lgslem3  15737  lgsfcl2  15741  lgsfle1  15744  lgsle1  15750  lgsdirprm  15769  lgseisenlem2  15806  lgsquadlem2  15813  2sqlem1  15849  2sqlem2  15850  mul2sq  15851  2sqlem3  15852  2sqlem9  15859  2sqlem10  15860  vtxvalg  15873  iedgvalg  15874  edgvalg  15916  edgopval  15919  edgstruct  15921  isuhgrm  15928  isushgrm  15929  isupgren  15952  isumgren  15962  isuspgren  16014  isusgren  16015  umgr2edg1  16066  usgredg2vlem1  16079  usgredg2vlem2  16080  ushgredgedg  16083  issubgr  16114  vtxdgfval  16145  vtxedgfi  16146  vtxdg0v  16151  vtxdumgrfival  16155  1loopgrvd0fi  16163  1hevtxdg0fi  16164  1hevtxdg1en  16165  wkslem1  16177  wkslem2  16178  wksfval  16179  iswlk  16180  uspgr2wlkeq  16222  uspgr2wlkeqi  16224  2wlklem  16233  trlsfvalg  16240  clwwlkg  16250  isclwwlk  16251  clwwlkccatlem  16257  clwwlkng  16262  clwwlkn2  16278  clwwlkext2edg  16279  umgr2cwwk2dif  16281  umgr2cwwkdifex  16282  clwwlknonmpo  16285  clwwlknonel  16289  clwwlknonex2lem2  16295  eupthsg  16302  iseupth  16304  eupthseg  16309  eupth2lem3lem3fi  16327  eupth2lem3lem6fi  16328  eupth2lem3lem4fi  16330  eupth2lem3fi  16333  eupth2lemsfi  16335  eupth2fi  16336  eulerpathprum  16337  depindlem1  16351  depindlem2  16352  depindlem3  16353  012of  16618  2o01f  16619  subctctexmid  16627  nnsf  16633  nninfalllem1  16636  nninffeq  16648  qdencn  16657  trilpolemclim  16666  trilpolemcl  16667  trilpolemisumle  16668  trilpolemeq1  16670  trilpolemlt1  16671  trilpo  16673  iswomni0  16682  redcwlpo  16686  dceqnconst  16691  dcapnconst  16692  nconstwlpolemgt0  16695  nconstwlpolem  16696  nconstwlpo  16697  neapmkv  16699