Theorem fveq2 5648

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

Syntax hints:   → wi 4   = wceq 1398   class class class wbr 4093  ℩cio 5291  ‘cfv 5333

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341

This theorem is referenced by:  fveq2i  5651  fveq2d  5652  2fveq3  5653  fvifdc  5670  dffn5imf  5710  fvelimab  5711  ssimaex  5716  fvco4  5727  fvmptssdm  5740  fvmptf  5748  eqfnfv2f  5757  fvelrn  5786  ralrnmpt  5797  rexrnmpt  5798  ffnfvf  5814  fmptco  5821  cofmpt  5824  fcompt  5825  fcoconst  5826  fsn2g  5830  fnressn  5848  fressnfv  5849  fconstfvm  5880  foco2  5904  funiunfvdmf  5915  f1veqaeq  5920  dff13f  5921  f1fveq  5923  f1elima  5924  f1ocnvfv  5930  f1ocnvfvb  5931  fcofo  5935  cocan2  5939  fliftfun  5947  isorel  5959  isocnv  5962  isotr  5967  f1oiso2  5978  canth  5979  imbrov2fvoveq  6053  ffnov  6135  eqfnov  6138  fnovim  6140  fnrnov  6178  foov  6179  funimassov  6182  ovelimab  6183  ofvalg  6254  ofrval  6255  offval2  6260  ofrfval2  6261  ofco  6263  caofinvl  6270  op1std  6320  op2ndd  6321  1stval2  6327  2ndval2  6328  unielxp  6346  reldm  6358  oprabco  6391  2ndconst  6396  f1o2ndf1  6402  elsuppfng  6420  elsuppfn  6421  mpoxopn0yelv  6448  mpoxopoveq  6449  smoel  6509  tfrlem1  6517  tfrlem3-2d  6521  tfrlem5  6523  tfrlem9  6528  tfr0dm  6531  tfrlemiubacc  6539  tfrlemi1  6541  tfrexlem  6543  tfr1onlemsucfn  6549  tfr1onlemsucaccv  6550  tfr1onlembxssdm  6552  tfr1onlembfn  6553  tfr1onlemubacc  6555  tfr1onlemaccex  6557  tfr1onlemres  6558  tfri1dALT  6560  tfrcllemsucfn  6562  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllembfn  6566  tfrcllemubacc  6568  tfrcllemaccex  6570  tfrcllemres  6571  tfrcldm  6572  tfrcl  6573  tfri3  6576  rdgtfr  6583  rdgss  6592  rdgisuc1  6593  rdgisucinc  6594  rdgon  6595  frecabex  6607  frecabcl  6608  frecfcllem  6613  frecsuclem  6615  frecsuc  6616  frecrdg  6617  oav  6665  omv  6666  oeiv  6667  fvixp  6915  cbvixp  6927  mptelixpg  6946  elixpsn  6947  dom2lem  6988  xpcomco  7053  xpmapen  7079  fidceq  7099  fieq0  7218  ordiso2  7277  djune  7320  updjudhcoinlf  7322  updjudhcoinrg  7323  updjud  7324  omp1eom  7337  0ct  7349  ctmlemr  7350  ctssdclemn0  7352  ctssdccl  7353  ctssdc  7355  enumctlemm  7356  nninfninc  7365  nnnninfeq  7370  nnnninfeq2  7371  enomnilem  7380  finomni  7382  fodjuomnilemdc  7386  fodju0  7389  fodjuomni  7391  ismkvnex  7397  fodjumkv  7402  nninfwlporlemd  7414  nninfwlpor  7416  exmidaclem  7466  cc1  7527  cc2lem  7528  cc2  7529  cc3  7530  mulpipq2  7634  genipv  7772  genpelxp  7774  addcanprleml  7877  addcanprlemu  7878  recexprlemm  7887  recexprlemdisj  7893  recexprlemloc  7894  recexprlem1ssl  7896  recexprlem1ssu  7897  cauappcvgprlemm  7908  cauappcvgprlemdisj  7914  cauappcvgprlemloc  7915  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  cauappcvgprlem1  7922  cauappcvgprlem2  7923  cauappcvgprlemlim  7924  cauappcvgpr  7925  caucvgprlemnkj  7929  caucvgprlemnbj  7930  caucvgprlemm  7931  caucvgprlemdisj  7937  caucvgprlemloc  7938  caucvgprlemcl  7939  caucvgprlemladdfu  7940  caucvgprlemladdrl  7941  caucvgprlem1  7942  caucvgprlem2  7943  caucvgpr  7945  caucvgprprlemell  7948  caucvgprprlemelu  7949  caucvgprprlemcbv  7950  caucvgprprlemval  7951  caucvgprprlemnkeqj  7953  caucvgprprlemnbj  7956  caucvgprprlemml  7957  caucvgprprlemmu  7958  caucvgprprlemopl  7960  caucvgprprlemlol  7961  caucvgprprlemopu  7962  caucvgprprlemloc  7966  caucvgprprlemclphr  7968  caucvgprprlemexbt  7969  caucvgprprlem1  7972  caucvgprprlem2  7973  caucvgsrlemcl  8052  caucvgsrlemfv  8054  caucvgsrlembound  8057  caucvgsrlemgt1  8058  caucvgsrlemoffval  8059  caucvgsrlemoffres  8063  caucvgsrlembnd  8064  caucvgsr  8065  axcaucvglemcau  8161  axcaucvglemres  8162  uz11  9823  cnref1o  9929  fzprval  10362  fztpval  10363  zsupcllemex  10536  infssuzex  10539  suprzubdc  10542  frec2uzuzd  10710  frec2uzltd  10711  frec2uzlt2d  10712  frecuzrdgrrn  10716  frec2uzrdg  10717  frecuzrdgtcl  10720  frecuzrdgg  10724  frecuzrdgfunlem  10727  frecfzennn  10734  seqeq1  10758  iseqovex  10766  seq3val  10768  seqvalcd  10769  seq3-1  10770  seqf  10772  seq3p1  10773  seqovcd  10775  seqp1cd  10778  seq3clss  10779  seq3fveq2  10783  seqfveq2g  10785  seqfveqg  10786  seq3fveq  10787  seq3feq  10788  seq3shft2  10789  seqshft2g  10790  monoord  10793  monoord2  10794  ser3mono  10795  seq3split  10796  seqsplitg  10797  seq3caopr3  10799  seqcaopr3g  10800  seq3caopr2  10801  seqcaopr2g  10802  iseqf1olemkle  10805  iseqf1olemklt  10806  iseqf1olemqval  10808  iseqf1olemqk  10815  iseqf1olemjpcl  10816  iseqf1olemqpcl  10817  iseqf1olemfvp  10818  seq3f1olemqsumkj  10819  seq3f1olemqsum  10821  seq3f1olemstep  10822  seq3f1olemp  10823  seq3f1oleml  10824  seq3f1o  10825  seqf1oglem2a  10826  seqf1og  10829  seq3id2  10834  seq3homo  10835  seq3z  10836  seqhomog  10838  seqfeq4g  10839  ser3ge0  10844  ser3le  10845  exp3vallem  10848  exp3val  10849  facp1  11038  faccl  11043  facdiv  11046  facwordi  11048  faclbnd  11049  facubnd  11053  bcval  11057  bcval5  11071  fz1eqb  11098  omgadd  11111  hashxp  11136  zfz1isolem1  11150  zfz1iso  11151  seq3coll  11152  eqwrd  11203  lswwrd  11209  lswex  11214  ccatfvalfi  11218  ccatval1  11223  ccatval2  11224  ccatalpha  11239  s1eq  11245  eqs1  11254  swrdval  11278  ccatopth2  11347  wrd2ind  11353  seq3shft  11461  reval  11472  replim  11482  cj11  11528  caucvgre  11604  cvg1nlemcau  11607  cvg1nlemres  11608  rexuz3  11613  absval  11624  resqrexlemover  11633  resqrexlemdecn  11635  resqrexlemlo  11636  resqrexlemcalc3  11639  resqrexlemnm  11641  resqrexlemcvg  11642  resqrexlemoverl  11644  resqrexlemglsq  11645  resqrexlemga  11646  resqrexlemsqa  11647  resqrexlemex  11648  abs00bd  11689  cau3lem  11737  caubnd2  11740  climconst  11913  climmpt  11923  climshftlemg  11925  climcn1  11931  climle  11957  climub  11967  climserle  11968  climcau  11970  climcvg1nlem  11972  climcvg1n  11973  serf0  11975  fsum3cvg  12002  summodclem3  12004  summodclem2a  12005  summodclem2  12006  summodc  12007  zsumdc  12008  fsum3  12011  fsumf1o  12014  fisumss  12016  fsum3cvg2  12018  fsum3ser  12021  fsumcl2lem  12022  fsumadd  12030  sumsnf  12033  isummulc2  12050  isumge0  12054  isumadd  12055  fsum2dlemstep  12058  fsummulc2  12072  fsumconst  12078  fsumrelem  12095  isumshft  12114  isum1p  12116  isumnn0nn  12117  isumrpcl  12118  isumlessdc  12120  cvgratnnlemnexp  12148  cvgratnnlemmn  12149  cvgratnnlemseq  12150  cvgratnnlemabsle  12151  cvgratnnlemfm  12153  cvgratnnlemrate  12154  cvgratnn  12155  cvgratz  12156  mertenslemi1  12159  mertenslem2  12160  mertensabs  12161  clim2prod  12163  prodfap0  12169  prodfrecap  12170  prodfdivap  12171  fproddccvg  12196  prodmodclem3  12199  prodmodclem2a  12200  prodmodclem2  12201  prodmodc  12202  zproddc  12203  fprodseq  12207  fprodf1o  12212  fprodssdc  12214  fprodmul  12215  prodsnf  12216  fprodfac  12239  fprodconst  12244  fprod2dlemstep  12246  eftvalcn  12281  ef0lem  12284  ege2le3  12295  efcj  12297  efaddlem  12298  eftlub  12314  efgt1p2  12319  reef11  12323  tanvalap  12332  efieq1re  12396  eirraplem  12401  dvdsabseq  12471  dvdsfac  12484  gcd0id  12613  nninfctlemfo  12674  nn0seqcvgd  12676  alginv  12682  algcvg  12683  algcvga  12686  algfx  12687  eucalglt  12692  lcmid  12715  qredeu  12732  prmfac1  12787  sqne2sq  12812  qnumdenbi  12827  dfphi2  12855  eulerthlemrprm  12864  eulerthlema  12865  eulerthlemh  12866  eulerthlemth  12867  phisum  12876  pcmpt  12979  pcfac  12986  1arithlem4  13002  elgz  13007  4sqlem4  13028  4sqlem12  13038  2expltfac  13075  ennnfonelemk  13084  ennnfonelemp1  13090  ennnfoneleminc  13095  ennnfonelemkh  13096  ennnfonelemhf1o  13097  ennnfonelemex  13098  ennnfonelemhom  13099  ennnfonelemrn  13103  ennnfonelemnn0  13106  ennnfonelemr  13107  ennnfonelemim  13108  ctinfomlemom  13111  ctinfom  13112  ctiunctlemfo  13123  nninfdclemlt  13135  nninfdclemf1  13136  sloteq  13150  ressvalsets  13210  topnvalg  13397  prdsbasprj  13428  prdsplusgfval  13430  prdsmulrfval  13432  imasex  13451  imasaddvallemg  13461  qusex  13471  xpsfrnel  13490  xpsfeq  13491  xpsval  13498  ismgm  13503  plusffvalg  13508  grpidvalg  13519  gsumfzval  13537  gsumval2  13543  issgrp  13549  ismnddef  13564  prdsidlem  13593  pws0g  13597  ismhm  13607  mhmex  13608  mhmlin  13613  issubm  13618  mhmeql  13638  isgrp  13652  grpn0  13681  grpinvfvalg  13688  grpsubfvalg  13691  grpsubval  13692  grpinv11  13715  grpinvnz  13717  prdsinvlem  13754  pwsinvg  13758  pwssub  13759  mhmlem  13764  mulgfvalg  13771  mulgsubcl  13786  mulgaddcomlem  13795  mulgneg2  13806  mulgass  13809  issubg  13823  subgex  13826  issubg2m  13839  issubg4m  13843  0subg  13849  isnsg  13852  releqgg  13870  eqgex  13871  eqgval  13873  isghm  13893  ghmlin  13898  ghmrn  13907  ghmeql  13917  f1ghm0to0  13922  iscmn  13943  mgpvalg  14000  isrng  14011  issrg  14042  srgfcl  14050  isring  14077  iscrng  14080  mulgass2  14135  opprvalg  14146  dvdsrvald  14171  isunitd  14184  invrfvald  14200  dvrfvald  14211  dvrvald  14212  isrhm  14236  rhmval  14251  isnzr  14259  islring  14270  issubrng  14277  issubrg  14299  rrgval  14340  rrgsupp  14344  isdomn  14348  aprval  14361  aprap  14365  islmod  14370  scaffvalg  14385  lsssetm  14435  lspfval  14467  sraval  14516  rlmvalg  14533  2idlval  14581  2idlvalg  14582  cnfldmulg  14655  zlmval  14706  znf1o  14730  psrlinv  14768  mplsubgfilemcl  14783  istps  14826  clsfval  14895  cnpval  14992  lmconst  15010  txcnp  15065  upxp  15066  uptx  15068  txlm  15073  lmcn2  15074  cnmpt11  15077  cnmpt11f  15078  cnmpt1t  15079  cnmpt21  15085  cnmpt21f  15086  cnmpt2t  15087  mopnval  15236  isxms  15245  isms  15247  comet  15293  mopnex  15299  xmetxp  15301  xmetxpbl  15302  txmetcnp  15312  txmetcn  15313  qtopbasss  15315  cncfi  15372  cncfmpt1f  15392  ivthinclemlm  15428  ivthinclemum  15429  ivthinclemlopn  15430  ivthinclemlr  15431  ivthinclemuopn  15432  ivthinclemur  15433  ivthinclemdisj  15434  ivthinclemloc  15435  ivthinc  15437  ivthdec  15438  ivthreinc  15439  cnlimci  15467  limccnpcntop  15469  eldvap  15476  dvcoapbr  15501  dvcj  15503  dvfre  15504  dvmptcjx  15518  dveflem  15520  elply2  15529  elplyd  15535  plymullem1  15542  plyadd  15545  plymul  15546  plycoeid3  15551  plycolemc  15552  plyco  15553  plycjlemc  15554  plycj  15555  dvply1  15559  sin0pilem2  15576  pilem3  15577  coseq0q4123  15628  coseq0negpitopi  15630  cos11  15647  logltb  15668  rpcxpef  15688  rplogbval  15739  pellexlem1  15774  pellexlem3  15776  mpodvdsmulf1o  15787  fsumdvdsmul  15788  zabsle1  15801  lgslem2  15803  lgslem3  15804  lgsfcl2  15808  lgsfle1  15811  lgsle1  15817  lgsdirprm  15836  lgseisenlem2  15873  lgsquadlem2  15880  2sqlem1  15916  2sqlem2  15917  mul2sq  15918  2sqlem3  15919  2sqlem9  15926  2sqlem10  15927  vtxvalg  15940  iedgvalg  15941  edgvalg  15983  edgopval  15986  edgstruct  15988  isuhgrm  15995  isushgrm  15996  isupgren  16019  isumgren  16029  isuspgren  16081  isusgren  16082  umgr2edg1  16133  usgredg2vlem1  16146  usgredg2vlem2  16147  ushgredgedg  16150  issubgr  16181  vtxdgfval  16212  vtxedgfi  16213  vtxdg0v  16218  vtxdumgrfival  16222  1loopgrvd0fi  16230  1hevtxdg0fi  16231  1hevtxdg1en  16232  wkslem1  16244  wkslem2  16245  wksfval  16246  iswlk  16247  uspgr2wlkeq  16289  uspgr2wlkeqi  16291  2wlklem  16300  trlsfvalg  16307  clwwlkg  16317  isclwwlk  16318  clwwlkccatlem  16324  clwwlkng  16329  clwwlkn2  16345  clwwlkext2edg  16346  umgr2cwwk2dif  16348  umgr2cwwkdifex  16349  clwwlknonmpo  16352  clwwlknonel  16356  clwwlknonex2lem2  16362  eupthsg  16369  iseupth  16371  eupthseg  16376  eupth2lem3lem3fi  16394  eupth2lem3lem6fi  16395  eupth2lem3lem4fi  16397  eupth2lem3fi  16400  eupth2lemsfi  16402  eupth2fi  16403  eulerpathprum  16404  konigsberglem4  16415  depindlem1  16430  depindlem2  16431  depindlem3  16432  012of  16696  2o01f  16697  subctctexmid  16705  nnsf  16714  nninfalllem1  16717  nninffeq  16729  qdencn  16738  trilpolemclim  16751  trilpolemcl  16752  trilpolemisumle  16753  trilpolemeq1  16755  trilpolemlt1  16756  trilpo  16758  iswomni0  16767  redcwlpo  16771  dceqnconst  16776  dcapnconst  16777  nconstwlpolemgt0  16780  nconstwlpolem  16781  nconstwlpo  16782  neapmkv  16784