Theorem fveq2 5561

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 4037	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝑥 ↔ 𝐵𝐹𝑥))
2	1	iotabidv 5242	. 2 ⊢ (𝐴 = 𝐵 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐵𝐹𝑥))
3		df-fv 5267	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5267	. 2 ⊢ (𝐹‘𝐵) = (℩𝑥𝐵𝐹𝑥)
5	2, 3, 4	3eqtr4g 2254	1 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))

Syntax hints:   → wi 4   = wceq 1364   class class class wbr 4034  ℩cio 5218  ‘cfv 5259

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267

This theorem is referenced by:  fveq2i  5564  fveq2d  5565  2fveq3  5566  fvifdc  5583  dffn5imf  5619  fvelimab  5620  ssimaex  5625  fvco4  5636  fvmptssdm  5649  fvmptf  5657  eqfnfv2f  5666  fvelrn  5696  ralrnmpt  5707  rexrnmpt  5708  ffnfvf  5724  fmptco  5731  cofmpt  5734  fcompt  5735  fcoconst  5736  fnressn  5751  fressnfv  5752  fconstfvm  5783  foco2  5803  funiunfvdmf  5814  f1veqaeq  5819  dff13f  5820  f1fveq  5822  f1elima  5823  f1ocnvfv  5829  f1ocnvfvb  5830  fcofo  5834  cocan2  5838  fliftfun  5846  isorel  5858  isocnv  5861  isotr  5866  f1oiso2  5877  canth  5878  imbrov2fvoveq  5950  ffnov  6030  eqfnov  6033  fnovim  6035  fnrnov  6073  foov  6074  funimassov  6077  ovelimab  6078  suppssfv  6135  ofvalg  6149  ofrval  6150  offval2  6155  ofrfval2  6156  ofco  6158  caofinvl  6165  op1std  6215  op2ndd  6216  1stval2  6222  2ndval2  6223  unielxp  6241  reldm  6253  oprabco  6284  2ndconst  6289  f1o2ndf1  6295  mpoxopn0yelv  6306  mpoxopoveq  6307  smoel  6367  tfrlem1  6375  tfrlem3-2d  6379  tfrlem5  6381  tfrlem9  6386  tfr0dm  6389  tfrlemiubacc  6397  tfrlemi1  6399  tfrexlem  6401  tfr1onlemsucfn  6407  tfr1onlemsucaccv  6408  tfr1onlembxssdm  6410  tfr1onlembfn  6411  tfr1onlemubacc  6413  tfr1onlemaccex  6415  tfr1onlemres  6416  tfri1dALT  6418  tfrcllemsucfn  6420  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllembfn  6424  tfrcllemubacc  6426  tfrcllemaccex  6428  tfrcllemres  6429  tfrcldm  6430  tfrcl  6431  tfri3  6434  rdgtfr  6441  rdgss  6450  rdgisuc1  6451  rdgisucinc  6452  rdgon  6453  frecabex  6465  frecabcl  6466  frecfcllem  6471  frecsuclem  6473  frecsuc  6474  frecrdg  6475  oav  6521  omv  6522  oeiv  6523  fvixp  6771  cbvixp  6783  mptelixpg  6802  elixpsn  6803  dom2lem  6840  xpcomco  6894  xpmapen  6920  fidceq  6939  fieq0  7051  ordiso2  7110  djune  7153  updjudhcoinlf  7155  updjudhcoinrg  7156  updjud  7157  omp1eom  7170  0ct  7182  ctmlemr  7183  ctssdclemn0  7185  ctssdccl  7186  ctssdc  7188  enumctlemm  7189  nninfninc  7198  nnnninfeq  7203  nnnninfeq2  7204  enomnilem  7213  finomni  7215  fodjuomnilemdc  7219  fodju0  7222  fodjuomni  7224  ismkvnex  7230  fodjumkv  7235  nninfwlporlemd  7247  nninfwlpor  7249  exmidaclem  7291  cc1  7348  cc2lem  7349  cc2  7350  cc3  7351  mulpipq2  7455  genipv  7593  genpelxp  7595  addcanprleml  7698  addcanprlemu  7699  recexprlemm  7708  recexprlemdisj  7714  recexprlemloc  7715  recexprlem1ssl  7717  recexprlem1ssu  7718  cauappcvgprlemm  7729  cauappcvgprlemdisj  7735  cauappcvgprlemloc  7736  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  cauappcvgprlem1  7743  cauappcvgprlem2  7744  cauappcvgprlemlim  7745  cauappcvgpr  7746  caucvgprlemnkj  7750  caucvgprlemnbj  7751  caucvgprlemm  7752  caucvgprlemdisj  7758  caucvgprlemloc  7759  caucvgprlemcl  7760  caucvgprlemladdfu  7761  caucvgprlemladdrl  7762  caucvgprlem1  7763  caucvgprlem2  7764  caucvgpr  7766  caucvgprprlemell  7769  caucvgprprlemelu  7770  caucvgprprlemcbv  7771  caucvgprprlemval  7772  caucvgprprlemnkeqj  7774  caucvgprprlemnbj  7777  caucvgprprlemml  7778  caucvgprprlemmu  7779  caucvgprprlemopl  7781  caucvgprprlemlol  7782  caucvgprprlemopu  7783  caucvgprprlemloc  7787  caucvgprprlemclphr  7789  caucvgprprlemexbt  7790  caucvgprprlem1  7793  caucvgprprlem2  7794  caucvgsrlemcl  7873  caucvgsrlemfv  7875  caucvgsrlembound  7878  caucvgsrlemgt1  7879  caucvgsrlemoffval  7880  caucvgsrlemoffres  7884  caucvgsrlembnd  7885  caucvgsr  7886  axcaucvglemcau  7982  axcaucvglemres  7983  uz11  9641  cnref1o  9742  fzprval  10174  fztpval  10175  zsupcllemex  10337  infssuzex  10340  suprzubdc  10343  frec2uzuzd  10511  frec2uzltd  10512  frec2uzlt2d  10513  frecuzrdgrrn  10517  frec2uzrdg  10518  frecuzrdgtcl  10521  frecuzrdgg  10525  frecuzrdgfunlem  10528  frecfzennn  10535  seqeq1  10559  iseqovex  10567  seq3val  10569  seqvalcd  10570  seq3-1  10571  seqf  10573  seq3p1  10574  seqovcd  10576  seqp1cd  10579  seq3clss  10580  seq3fveq2  10584  seqfveq2g  10586  seqfveqg  10587  seq3fveq  10588  seq3feq  10589  seq3shft2  10590  seqshft2g  10591  monoord  10594  monoord2  10595  ser3mono  10596  seq3split  10597  seqsplitg  10598  seq3caopr3  10600  seqcaopr3g  10601  seq3caopr2  10602  seqcaopr2g  10603  iseqf1olemkle  10606  iseqf1olemklt  10607  iseqf1olemqval  10609  iseqf1olemqk  10616  iseqf1olemjpcl  10617  iseqf1olemqpcl  10618  iseqf1olemfvp  10619  seq3f1olemqsumkj  10620  seq3f1olemqsum  10622  seq3f1olemstep  10623  seq3f1olemp  10624  seq3f1oleml  10625  seq3f1o  10626  seqf1oglem2a  10627  seqf1og  10630  seq3id2  10635  seq3homo  10636  seq3z  10637  seqhomog  10639  seqfeq4g  10640  ser3ge0  10645  ser3le  10646  exp3vallem  10649  exp3val  10650  facp1  10839  faccl  10844  facdiv  10847  facwordi  10849  faclbnd  10850  facubnd  10854  bcval  10858  bcval5  10872  fz1eqb  10899  omgadd  10911  hashxp  10935  zfz1isolem1  10949  zfz1iso  10950  seq3coll  10951  eqwrd  10992  seq3shft  11020  reval  11031  replim  11041  cj11  11087  caucvgre  11163  cvg1nlemcau  11166  cvg1nlemres  11167  rexuz3  11172  absval  11183  resqrexlemover  11192  resqrexlemdecn  11194  resqrexlemlo  11195  resqrexlemcalc3  11198  resqrexlemnm  11200  resqrexlemcvg  11201  resqrexlemoverl  11203  resqrexlemglsq  11204  resqrexlemga  11205  resqrexlemsqa  11206  resqrexlemex  11207  abs00bd  11248  cau3lem  11296  caubnd2  11299  climconst  11472  climmpt  11482  climshftlemg  11484  climcn1  11490  climle  11516  climub  11526  climserle  11527  climcau  11529  climcvg1nlem  11531  climcvg1n  11532  serf0  11534  fsum3cvg  11560  summodclem3  11562  summodclem2a  11563  summodclem2  11564  summodc  11565  zsumdc  11566  fsum3  11569  fsumf1o  11572  fisumss  11574  fsum3cvg2  11576  fsum3ser  11579  fsumcl2lem  11580  fsumadd  11588  sumsnf  11591  isummulc2  11608  isumge0  11612  isumadd  11613  fsum2dlemstep  11616  fsummulc2  11630  fsumconst  11636  fsumrelem  11653  isumshft  11672  isum1p  11674  isumnn0nn  11675  isumrpcl  11676  isumlessdc  11678  cvgratnnlemnexp  11706  cvgratnnlemmn  11707  cvgratnnlemseq  11708  cvgratnnlemabsle  11709  cvgratnnlemfm  11711  cvgratnnlemrate  11712  cvgratnn  11713  cvgratz  11714  mertenslemi1  11717  mertenslem2  11718  mertensabs  11719  clim2prod  11721  prodfap0  11727  prodfrecap  11728  prodfdivap  11729  fproddccvg  11754  prodmodclem3  11757  prodmodclem2a  11758  prodmodclem2  11759  prodmodc  11760  zproddc  11761  fprodseq  11765  fprodf1o  11770  fprodssdc  11772  fprodmul  11773  prodsnf  11774  fprodfac  11797  fprodconst  11802  fprod2dlemstep  11804  eftvalcn  11839  ef0lem  11842  ege2le3  11853  efcj  11855  efaddlem  11856  eftlub  11872  efgt1p2  11877  reef11  11881  tanvalap  11890  efieq1re  11954  eirraplem  11959  dvdsabseq  12029  dvdsfac  12042  gcd0id  12171  nninfctlemfo  12232  nn0seqcvgd  12234  alginv  12240  algcvg  12241  algcvga  12244  algfx  12245  eucalglt  12250  lcmid  12273  qredeu  12290  prmfac1  12345  sqne2sq  12370  qnumdenbi  12385  dfphi2  12413  eulerthlemrprm  12422  eulerthlema  12423  eulerthlemh  12424  eulerthlemth  12425  phisum  12434  pcmpt  12537  pcfac  12544  1arithlem4  12560  elgz  12565  4sqlem4  12586  4sqlem12  12596  2expltfac  12633  ennnfonelemk  12642  ennnfonelemp1  12648  ennnfoneleminc  12653  ennnfonelemkh  12654  ennnfonelemhf1o  12655  ennnfonelemex  12656  ennnfonelemhom  12657  ennnfonelemrn  12661  ennnfonelemnn0  12664  ennnfonelemr  12665  ennnfonelemim  12666  ctinfomlemom  12669  ctinfom  12670  ctiunctlemfo  12681  nninfdclemlt  12693  nninfdclemf1  12694  sloteq  12708  ressvalsets  12767  topnvalg  12953  prdsbasprj  12984  prdsplusgfval  12986  prdsmulrfval  12988  imasex  13007  imasaddvallemg  13017  qusex  13027  xpsfrnel  13046  xpsfeq  13047  xpsval  13054  ismgm  13059  plusffvalg  13064  grpidvalg  13075  gsumfzval  13093  gsumval2  13099  issgrp  13105  ismnddef  13120  prdsidlem  13149  pws0g  13153  ismhm  13163  mhmex  13164  mhmlin  13169  issubm  13174  mhmeql  13194  isgrp  13208  grpn0  13237  grpinvfvalg  13244  grpsubfvalg  13247  grpsubval  13248  grpinv11  13271  grpinvnz  13273  prdsinvlem  13310  pwsinvg  13314  pwssub  13315  mhmlem  13320  mulgfvalg  13327  mulgsubcl  13342  mulgaddcomlem  13351  mulgneg2  13362  mulgass  13365  issubg  13379  subgex  13382  issubg2m  13395  issubg4m  13399  0subg  13405  isnsg  13408  releqgg  13426  eqgex  13427  eqgval  13429  isghm  13449  ghmlin  13454  ghmrn  13463  ghmeql  13473  f1ghm0to0  13478  iscmn  13499  mgpvalg  13555  isrng  13566  issrg  13597  srgfcl  13605  isring  13632  iscrng  13635  mulgass2  13690  opprvalg  13701  reldvdsrsrg  13724  dvdsrvald  13725  isunitd  13738  invrfvald  13754  dvrfvald  13765  dvrvald  13766  isrhm  13790  rhmval  13805  isnzr  13813  islring  13824  issubrng  13831  issubrg  13853  rrgval  13894  isdomn  13901  aprval  13914  aprap  13918  islmod  13923  scaffvalg  13938  lsssetm  13988  lspfval  14020  sraval  14069  rlmvalg  14086  2idlval  14134  2idlvalg  14135  cnfldmulg  14208  zlmval  14259  znf1o  14283  psrlinv  14312  istps  14352  clsfval  14421  cnpval  14518  lmconst  14536  txcnp  14591  upxp  14592  uptx  14594  txlm  14599  lmcn2  14600  cnmpt11  14603  cnmpt11f  14604  cnmpt1t  14605  cnmpt21  14611  cnmpt21f  14612  cnmpt2t  14613  mopnval  14762  isxms  14771  isms  14773  comet  14819  mopnex  14825  xmetxp  14827  xmetxpbl  14828  txmetcnp  14838  txmetcn  14839  qtopbasss  14841  cncfi  14898  cncfmpt1f  14918  ivthinclemlm  14954  ivthinclemum  14955  ivthinclemlopn  14956  ivthinclemlr  14957  ivthinclemuopn  14958  ivthinclemur  14959  ivthinclemdisj  14960  ivthinclemloc  14961  ivthinc  14963  ivthdec  14964  ivthreinc  14965  cnlimci  14993  limccnpcntop  14995  eldvap  15002  dvcoapbr  15027  dvcj  15029  dvfre  15030  dvmptcjx  15044  dveflem  15046  elply2  15055  elplyd  15061  plymullem1  15068  plyadd  15071  plymul  15072  plycoeid3  15077  plycolemc  15078  plyco  15079  plycjlemc  15080  plycj  15081  dvply1  15085  sin0pilem2  15102  pilem3  15103  coseq0q4123  15154  coseq0negpitopi  15156  cos11  15173  logltb  15194  rpcxpef  15214  rplogbval  15265  mpodvdsmulf1o  15310  fsumdvdsmul  15311  zabsle1  15324  lgslem2  15326  lgslem3  15327  lgsfcl2  15331  lgsfle1  15334  lgsle1  15340  lgsdirprm  15359  lgseisenlem2  15396  lgsquadlem2  15403  2sqlem1  15439  2sqlem2  15440  mul2sq  15441  2sqlem3  15442  2sqlem9  15449  2sqlem10  15450  012of  15724  2o01f  15725  subctctexmid  15731  nnsf  15736  nninfalllem1  15739  nninffeq  15751  qdencn  15758  trilpolemclim  15767  trilpolemcl  15768  trilpolemisumle  15769  trilpolemeq1  15771  trilpolemlt1  15772  trilpo  15774  iswomni0  15782  redcwlpo  15786  dceqnconst  15791  dcapnconst  15792  nconstwlpolemgt0  15795  nconstwlpolem  15796  nconstwlpo  15797  neapmkv  15799