Theorem fveq2 5575

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 4046	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝑥 ↔ 𝐵𝐹𝑥))
2	1	iotabidv 5253	. 2 ⊢ (𝐴 = 𝐵 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐵𝐹𝑥))
3		df-fv 5278	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5278	. 2 ⊢ (𝐹‘𝐵) = (℩𝑥𝐵𝐹𝑥)
5	2, 3, 4	3eqtr4g 2262	1 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))

Syntax hints:   → wi 4   = wceq 1372   class class class wbr 4043  ℩cio 5229  ‘cfv 5270

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-rex 2489  df-v 2773  df-un 3169  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-br 4044  df-iota 5231  df-fv 5278

This theorem is referenced by:  fveq2i  5578  fveq2d  5579  2fveq3  5580  fvifdc  5597  dffn5imf  5633  fvelimab  5634  ssimaex  5639  fvco4  5650  fvmptssdm  5663  fvmptf  5671  eqfnfv2f  5680  fvelrn  5710  ralrnmpt  5721  rexrnmpt  5722  ffnfvf  5738  fmptco  5745  cofmpt  5748  fcompt  5749  fcoconst  5750  fnressn  5769  fressnfv  5770  fconstfvm  5801  foco2  5821  funiunfvdmf  5832  f1veqaeq  5837  dff13f  5838  f1fveq  5840  f1elima  5841  f1ocnvfv  5847  f1ocnvfvb  5848  fcofo  5852  cocan2  5856  fliftfun  5864  isorel  5876  isocnv  5879  isotr  5884  f1oiso2  5895  canth  5896  imbrov2fvoveq  5968  ffnov  6048  eqfnov  6051  fnovim  6053  fnrnov  6091  foov  6092  funimassov  6095  ovelimab  6096  suppssfv  6153  ofvalg  6167  ofrval  6168  offval2  6173  ofrfval2  6174  ofco  6176  caofinvl  6183  op1std  6233  op2ndd  6234  1stval2  6240  2ndval2  6241  unielxp  6259  reldm  6271  oprabco  6302  2ndconst  6307  f1o2ndf1  6313  mpoxopn0yelv  6324  mpoxopoveq  6325  smoel  6385  tfrlem1  6393  tfrlem3-2d  6397  tfrlem5  6399  tfrlem9  6404  tfr0dm  6407  tfrlemiubacc  6415  tfrlemi1  6417  tfrexlem  6419  tfr1onlemsucfn  6425  tfr1onlemsucaccv  6426  tfr1onlembxssdm  6428  tfr1onlembfn  6429  tfr1onlemubacc  6431  tfr1onlemaccex  6433  tfr1onlemres  6434  tfri1dALT  6436  tfrcllemsucfn  6438  tfrcllemsucaccv  6439  tfrcllembxssdm  6441  tfrcllembfn  6442  tfrcllemubacc  6444  tfrcllemaccex  6446  tfrcllemres  6447  tfrcldm  6448  tfrcl  6449  tfri3  6452  rdgtfr  6459  rdgss  6468  rdgisuc1  6469  rdgisucinc  6470  rdgon  6471  frecabex  6483  frecabcl  6484  frecfcllem  6489  frecsuclem  6491  frecsuc  6492  frecrdg  6493  oav  6539  omv  6540  oeiv  6541  fvixp  6789  cbvixp  6801  mptelixpg  6820  elixpsn  6821  dom2lem  6862  xpcomco  6920  xpmapen  6946  fidceq  6965  fieq0  7077  ordiso2  7136  djune  7179  updjudhcoinlf  7181  updjudhcoinrg  7182  updjud  7183  omp1eom  7196  0ct  7208  ctmlemr  7209  ctssdclemn0  7211  ctssdccl  7212  ctssdc  7214  enumctlemm  7215  nninfninc  7224  nnnninfeq  7229  nnnninfeq2  7230  enomnilem  7239  finomni  7241  fodjuomnilemdc  7245  fodju0  7248  fodjuomni  7250  ismkvnex  7256  fodjumkv  7261  nninfwlporlemd  7273  nninfwlpor  7275  exmidaclem  7319  cc1  7376  cc2lem  7377  cc2  7378  cc3  7379  mulpipq2  7483  genipv  7621  genpelxp  7623  addcanprleml  7726  addcanprlemu  7727  recexprlemm  7736  recexprlemdisj  7742  recexprlemloc  7743  recexprlem1ssl  7745  recexprlem1ssu  7746  cauappcvgprlemm  7757  cauappcvgprlemdisj  7763  cauappcvgprlemloc  7764  cauappcvgprlemladdru  7768  cauappcvgprlemladdrl  7769  cauappcvgprlem1  7771  cauappcvgprlem2  7772  cauappcvgprlemlim  7773  cauappcvgpr  7774  caucvgprlemnkj  7778  caucvgprlemnbj  7779  caucvgprlemm  7780  caucvgprlemdisj  7786  caucvgprlemloc  7787  caucvgprlemcl  7788  caucvgprlemladdfu  7789  caucvgprlemladdrl  7790  caucvgprlem1  7791  caucvgprlem2  7792  caucvgpr  7794  caucvgprprlemell  7797  caucvgprprlemelu  7798  caucvgprprlemcbv  7799  caucvgprprlemval  7800  caucvgprprlemnkeqj  7802  caucvgprprlemnbj  7805  caucvgprprlemml  7806  caucvgprprlemmu  7807  caucvgprprlemopl  7809  caucvgprprlemlol  7810  caucvgprprlemopu  7811  caucvgprprlemloc  7815  caucvgprprlemclphr  7817  caucvgprprlemexbt  7818  caucvgprprlem1  7821  caucvgprprlem2  7822  caucvgsrlemcl  7901  caucvgsrlemfv  7903  caucvgsrlembound  7906  caucvgsrlemgt1  7907  caucvgsrlemoffval  7908  caucvgsrlemoffres  7912  caucvgsrlembnd  7913  caucvgsr  7914  axcaucvglemcau  8010  axcaucvglemres  8011  uz11  9670  cnref1o  9771  fzprval  10203  fztpval  10204  zsupcllemex  10371  infssuzex  10374  suprzubdc  10377  frec2uzuzd  10545  frec2uzltd  10546  frec2uzlt2d  10547  frecuzrdgrrn  10551  frec2uzrdg  10552  frecuzrdgtcl  10555  frecuzrdgg  10559  frecuzrdgfunlem  10562  frecfzennn  10569  seqeq1  10593  iseqovex  10601  seq3val  10603  seqvalcd  10604  seq3-1  10605  seqf  10607  seq3p1  10608  seqovcd  10610  seqp1cd  10613  seq3clss  10614  seq3fveq2  10618  seqfveq2g  10620  seqfveqg  10621  seq3fveq  10622  seq3feq  10623  seq3shft2  10624  seqshft2g  10625  monoord  10628  monoord2  10629  ser3mono  10630  seq3split  10631  seqsplitg  10632  seq3caopr3  10634  seqcaopr3g  10635  seq3caopr2  10636  seqcaopr2g  10637  iseqf1olemkle  10640  iseqf1olemklt  10641  iseqf1olemqval  10643  iseqf1olemqk  10650  iseqf1olemjpcl  10651  iseqf1olemqpcl  10652  iseqf1olemfvp  10653  seq3f1olemqsumkj  10654  seq3f1olemqsum  10656  seq3f1olemstep  10657  seq3f1olemp  10658  seq3f1oleml  10659  seq3f1o  10660  seqf1oglem2a  10661  seqf1og  10664  seq3id2  10669  seq3homo  10670  seq3z  10671  seqhomog  10673  seqfeq4g  10674  ser3ge0  10679  ser3le  10680  exp3vallem  10683  exp3val  10684  facp1  10873  faccl  10878  facdiv  10881  facwordi  10883  faclbnd  10884  facubnd  10888  bcval  10892  bcval5  10906  fz1eqb  10933  omgadd  10945  hashxp  10969  zfz1isolem1  10983  zfz1iso  10984  seq3coll  10985  eqwrd  11032  lswwrd  11038  ccatfvalfi  11046  ccatval1  11051  ccatval2  11052  s1eq  11071  eqs1  11080  seq3shft  11120  reval  11131  replim  11141  cj11  11187  caucvgre  11263  cvg1nlemcau  11266  cvg1nlemres  11267  rexuz3  11272  absval  11283  resqrexlemover  11292  resqrexlemdecn  11294  resqrexlemlo  11295  resqrexlemcalc3  11298  resqrexlemnm  11300  resqrexlemcvg  11301  resqrexlemoverl  11303  resqrexlemglsq  11304  resqrexlemga  11305  resqrexlemsqa  11306  resqrexlemex  11307  abs00bd  11348  cau3lem  11396  caubnd2  11399  climconst  11572  climmpt  11582  climshftlemg  11584  climcn1  11590  climle  11616  climub  11626  climserle  11627  climcau  11629  climcvg1nlem  11631  climcvg1n  11632  serf0  11634  fsum3cvg  11660  summodclem3  11662  summodclem2a  11663  summodclem2  11664  summodc  11665  zsumdc  11666  fsum3  11669  fsumf1o  11672  fisumss  11674  fsum3cvg2  11676  fsum3ser  11679  fsumcl2lem  11680  fsumadd  11688  sumsnf  11691  isummulc2  11708  isumge0  11712  isumadd  11713  fsum2dlemstep  11716  fsummulc2  11730  fsumconst  11736  fsumrelem  11753  isumshft  11772  isum1p  11774  isumnn0nn  11775  isumrpcl  11776  isumlessdc  11778  cvgratnnlemnexp  11806  cvgratnnlemmn  11807  cvgratnnlemseq  11808  cvgratnnlemabsle  11809  cvgratnnlemfm  11811  cvgratnnlemrate  11812  cvgratnn  11813  cvgratz  11814  mertenslemi1  11817  mertenslem2  11818  mertensabs  11819  clim2prod  11821  prodfap0  11827  prodfrecap  11828  prodfdivap  11829  fproddccvg  11854  prodmodclem3  11857  prodmodclem2a  11858  prodmodclem2  11859  prodmodc  11860  zproddc  11861  fprodseq  11865  fprodf1o  11870  fprodssdc  11872  fprodmul  11873  prodsnf  11874  fprodfac  11897  fprodconst  11902  fprod2dlemstep  11904  eftvalcn  11939  ef0lem  11942  ege2le3  11953  efcj  11955  efaddlem  11956  eftlub  11972  efgt1p2  11977  reef11  11981  tanvalap  11990  efieq1re  12054  eirraplem  12059  dvdsabseq  12129  dvdsfac  12142  gcd0id  12271  nninfctlemfo  12332  nn0seqcvgd  12334  alginv  12340  algcvg  12341  algcvga  12344  algfx  12345  eucalglt  12350  lcmid  12373  qredeu  12390  prmfac1  12445  sqne2sq  12470  qnumdenbi  12485  dfphi2  12513  eulerthlemrprm  12522  eulerthlema  12523  eulerthlemh  12524  eulerthlemth  12525  phisum  12534  pcmpt  12637  pcfac  12644  1arithlem4  12660  elgz  12665  4sqlem4  12686  4sqlem12  12696  2expltfac  12733  ennnfonelemk  12742  ennnfonelemp1  12748  ennnfoneleminc  12753  ennnfonelemkh  12754  ennnfonelemhf1o  12755  ennnfonelemex  12756  ennnfonelemhom  12757  ennnfonelemrn  12761  ennnfonelemnn0  12764  ennnfonelemr  12765  ennnfonelemim  12766  ctinfomlemom  12769  ctinfom  12770  ctiunctlemfo  12781  nninfdclemlt  12793  nninfdclemf1  12794  sloteq  12808  ressvalsets  12867  topnvalg  13054  prdsbasprj  13085  prdsplusgfval  13087  prdsmulrfval  13089  imasex  13108  imasaddvallemg  13118  qusex  13128  xpsfrnel  13147  xpsfeq  13148  xpsval  13155  ismgm  13160  plusffvalg  13165  grpidvalg  13176  gsumfzval  13194  gsumval2  13200  issgrp  13206  ismnddef  13221  prdsidlem  13250  pws0g  13254  ismhm  13264  mhmex  13265  mhmlin  13270  issubm  13275  mhmeql  13295  isgrp  13309  grpn0  13338  grpinvfvalg  13345  grpsubfvalg  13348  grpsubval  13349  grpinv11  13372  grpinvnz  13374  prdsinvlem  13411  pwsinvg  13415  pwssub  13416  mhmlem  13421  mulgfvalg  13428  mulgsubcl  13443  mulgaddcomlem  13452  mulgneg2  13463  mulgass  13466  issubg  13480  subgex  13483  issubg2m  13496  issubg4m  13500  0subg  13506  isnsg  13509  releqgg  13527  eqgex  13528  eqgval  13530  isghm  13550  ghmlin  13555  ghmrn  13564  ghmeql  13574  f1ghm0to0  13579  iscmn  13600  mgpvalg  13656  isrng  13667  issrg  13698  srgfcl  13706  isring  13733  iscrng  13736  mulgass2  13791  opprvalg  13802  reldvdsrsrg  13825  dvdsrvald  13826  isunitd  13839  invrfvald  13855  dvrfvald  13866  dvrvald  13867  isrhm  13891  rhmval  13906  isnzr  13914  islring  13925  issubrng  13932  issubrg  13954  rrgval  13995  isdomn  14002  aprval  14015  aprap  14019  islmod  14024  scaffvalg  14039  lsssetm  14089  lspfval  14121  sraval  14170  rlmvalg  14187  2idlval  14235  2idlvalg  14236  cnfldmulg  14309  zlmval  14360  znf1o  14384  psrlinv  14417  mplsubgfilemcl  14432  istps  14475  clsfval  14544  cnpval  14641  lmconst  14659  txcnp  14714  upxp  14715  uptx  14717  txlm  14722  lmcn2  14723  cnmpt11  14726  cnmpt11f  14727  cnmpt1t  14728  cnmpt21  14734  cnmpt21f  14735  cnmpt2t  14736  mopnval  14885  isxms  14894  isms  14896  comet  14942  mopnex  14948  xmetxp  14950  xmetxpbl  14951  txmetcnp  14961  txmetcn  14962  qtopbasss  14964  cncfi  15021  cncfmpt1f  15041  ivthinclemlm  15077  ivthinclemum  15078  ivthinclemlopn  15079  ivthinclemlr  15080  ivthinclemuopn  15081  ivthinclemur  15082  ivthinclemdisj  15083  ivthinclemloc  15084  ivthinc  15086  ivthdec  15087  ivthreinc  15088  cnlimci  15116  limccnpcntop  15118  eldvap  15125  dvcoapbr  15150  dvcj  15152  dvfre  15153  dvmptcjx  15167  dveflem  15169  elply2  15178  elplyd  15184  plymullem1  15191  plyadd  15194  plymul  15195  plycoeid3  15200  plycolemc  15201  plyco  15202  plycjlemc  15203  plycj  15204  dvply1  15208  sin0pilem2  15225  pilem3  15226  coseq0q4123  15277  coseq0negpitopi  15279  cos11  15296  logltb  15317  rpcxpef  15337  rplogbval  15388  mpodvdsmulf1o  15433  fsumdvdsmul  15434  zabsle1  15447  lgslem2  15449  lgslem3  15450  lgsfcl2  15454  lgsfle1  15457  lgsle1  15463  lgsdirprm  15482  lgseisenlem2  15519  lgsquadlem2  15526  2sqlem1  15562  2sqlem2  15563  mul2sq  15564  2sqlem3  15565  2sqlem9  15572  2sqlem10  15573  vtxvalg  15586  iedgvalg  15587  012of  15892  2o01f  15893  subctctexmid  15899  nnsf  15904  nninfalllem1  15907  nninffeq  15919  qdencn  15928  trilpolemclim  15937  trilpolemcl  15938  trilpolemisumle  15939  trilpolemeq1  15941  trilpolemlt1  15942  trilpo  15944  iswomni0  15952  redcwlpo  15956  dceqnconst  15961  dcapnconst  15962  nconstwlpolemgt0  15965  nconstwlpolem  15966  nconstwlpo  15967  neapmkv  15969