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  seq3shft  11091  reval  11102  replim  11112  cj11  11158  caucvgre  11234  cvg1nlemcau  11237  cvg1nlemres  11238  rexuz3  11243  absval  11254  resqrexlemover  11263  resqrexlemdecn  11265  resqrexlemlo  11266  resqrexlemcalc3  11269  resqrexlemnm  11271  resqrexlemcvg  11272  resqrexlemoverl  11274  resqrexlemglsq  11275  resqrexlemga  11276  resqrexlemsqa  11277  resqrexlemex  11278  abs00bd  11319  cau3lem  11367  caubnd2  11370  climconst  11543  climmpt  11553  climshftlemg  11555  climcn1  11561  climle  11587  climub  11597  climserle  11598  climcau  11600  climcvg1nlem  11602  climcvg1n  11603  serf0  11605  fsum3cvg  11631  summodclem3  11633  summodclem2a  11634  summodclem2  11635  summodc  11636  zsumdc  11637  fsum3  11640  fsumf1o  11643  fisumss  11645  fsum3cvg2  11647  fsum3ser  11650  fsumcl2lem  11651  fsumadd  11659  sumsnf  11662  isummulc2  11679  isumge0  11683  isumadd  11684  fsum2dlemstep  11687  fsummulc2  11701  fsumconst  11707  fsumrelem  11724  isumshft  11743  isum1p  11745  isumnn0nn  11746  isumrpcl  11747  isumlessdc  11749  cvgratnnlemnexp  11777  cvgratnnlemmn  11778  cvgratnnlemseq  11779  cvgratnnlemabsle  11780  cvgratnnlemfm  11782  cvgratnnlemrate  11783  cvgratnn  11784  cvgratz  11785  mertenslemi1  11788  mertenslem2  11789  mertensabs  11790  clim2prod  11792  prodfap0  11798  prodfrecap  11799  prodfdivap  11800  fproddccvg  11825  prodmodclem3  11828  prodmodclem2a  11829  prodmodclem2  11830  prodmodc  11831  zproddc  11832  fprodseq  11836  fprodf1o  11841  fprodssdc  11843  fprodmul  11844  prodsnf  11845  fprodfac  11868  fprodconst  11873  fprod2dlemstep  11875  eftvalcn  11910  ef0lem  11913  ege2le3  11924  efcj  11926  efaddlem  11927  eftlub  11943  efgt1p2  11948  reef11  11952  tanvalap  11961  efieq1re  12025  eirraplem  12030  dvdsabseq  12100  dvdsfac  12113  gcd0id  12242  nninfctlemfo  12303  nn0seqcvgd  12305  alginv  12311  algcvg  12312  algcvga  12315  algfx  12316  eucalglt  12321  lcmid  12344  qredeu  12361  prmfac1  12416  sqne2sq  12441  qnumdenbi  12456  dfphi2  12484  eulerthlemrprm  12493  eulerthlema  12494  eulerthlemh  12495  eulerthlemth  12496  phisum  12505  pcmpt  12608  pcfac  12615  1arithlem4  12631  elgz  12636  4sqlem4  12657  4sqlem12  12667  2expltfac  12704  ennnfonelemk  12713  ennnfonelemp1  12719  ennnfoneleminc  12724  ennnfonelemkh  12725  ennnfonelemhf1o  12726  ennnfonelemex  12727  ennnfonelemhom  12728  ennnfonelemrn  12732  ennnfonelemnn0  12735  ennnfonelemr  12736  ennnfonelemim  12737  ctinfomlemom  12740  ctinfom  12741  ctiunctlemfo  12752  nninfdclemlt  12764  nninfdclemf1  12765  sloteq  12779  ressvalsets  12838  topnvalg  13025  prdsbasprj  13056  prdsplusgfval  13058  prdsmulrfval  13060  imasex  13079  imasaddvallemg  13089  qusex  13099  xpsfrnel  13118  xpsfeq  13119  xpsval  13126  ismgm  13131  plusffvalg  13136  grpidvalg  13147  gsumfzval  13165  gsumval2  13171  issgrp  13177  ismnddef  13192  prdsidlem  13221  pws0g  13225  ismhm  13235  mhmex  13236  mhmlin  13241  issubm  13246  mhmeql  13266  isgrp  13280  grpn0  13309  grpinvfvalg  13316  grpsubfvalg  13319  grpsubval  13320  grpinv11  13343  grpinvnz  13345  prdsinvlem  13382  pwsinvg  13386  pwssub  13387  mhmlem  13392  mulgfvalg  13399  mulgsubcl  13414  mulgaddcomlem  13423  mulgneg2  13434  mulgass  13437  issubg  13451  subgex  13454  issubg2m  13467  issubg4m  13471  0subg  13477  isnsg  13480  releqgg  13498  eqgex  13499  eqgval  13501  isghm  13521  ghmlin  13526  ghmrn  13535  ghmeql  13545  f1ghm0to0  13550  iscmn  13571  mgpvalg  13627  isrng  13638  issrg  13669  srgfcl  13677  isring  13704  iscrng  13707  mulgass2  13762  opprvalg  13773  reldvdsrsrg  13796  dvdsrvald  13797  isunitd  13810  invrfvald  13826  dvrfvald  13837  dvrvald  13838  isrhm  13862  rhmval  13877  isnzr  13885  islring  13896  issubrng  13903  issubrg  13925  rrgval  13966  isdomn  13973  aprval  13986  aprap  13990  islmod  13995  scaffvalg  14010  lsssetm  14060  lspfval  14092  sraval  14141  rlmvalg  14158  2idlval  14206  2idlvalg  14207  cnfldmulg  14280  zlmval  14331  znf1o  14355  psrlinv  14388  mplsubgfilemcl  14403  istps  14446  clsfval  14515  cnpval  14612  lmconst  14630  txcnp  14685  upxp  14686  uptx  14688  txlm  14693  lmcn2  14694  cnmpt11  14697  cnmpt11f  14698  cnmpt1t  14699  cnmpt21  14705  cnmpt21f  14706  cnmpt2t  14707  mopnval  14856  isxms  14865  isms  14867  comet  14913  mopnex  14919  xmetxp  14921  xmetxpbl  14922  txmetcnp  14932  txmetcn  14933  qtopbasss  14935  cncfi  14992  cncfmpt1f  15012  ivthinclemlm  15048  ivthinclemum  15049  ivthinclemlopn  15050  ivthinclemlr  15051  ivthinclemuopn  15052  ivthinclemur  15053  ivthinclemdisj  15054  ivthinclemloc  15055  ivthinc  15057  ivthdec  15058  ivthreinc  15059  cnlimci  15087  limccnpcntop  15089  eldvap  15096  dvcoapbr  15121  dvcj  15123  dvfre  15124  dvmptcjx  15138  dveflem  15140  elply2  15149  elplyd  15155  plymullem1  15162  plyadd  15165  plymul  15166  plycoeid3  15171  plycolemc  15172  plyco  15173  plycjlemc  15174  plycj  15175  dvply1  15179  sin0pilem2  15196  pilem3  15197  coseq0q4123  15248  coseq0negpitopi  15250  cos11  15267  logltb  15288  rpcxpef  15308  rplogbval  15359  mpodvdsmulf1o  15404  fsumdvdsmul  15405  zabsle1  15418  lgslem2  15420  lgslem3  15421  lgsfcl2  15425  lgsfle1  15428  lgsle1  15434  lgsdirprm  15453  lgseisenlem2  15490  lgsquadlem2  15497  2sqlem1  15533  2sqlem2  15534  mul2sq  15535  2sqlem3  15536  2sqlem9  15543  2sqlem10  15544  vtxvalg  15557  iedgvalg  15558  012of  15863  2o01f  15864  subctctexmid  15870  nnsf  15875  nninfalllem1  15878  nninffeq  15890  qdencn  15899  trilpolemclim  15908  trilpolemcl  15909  trilpolemisumle  15910  trilpolemeq1  15912  trilpolemlt1  15913  trilpo  15915  iswomni0  15923  redcwlpo  15927  dceqnconst  15932  dcapnconst  15933  nconstwlpolemgt0  15936  nconstwlpolem  15937  nconstwlpo  15938  neapmkv  15940