Theorem fveq2 5675

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 4117	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝑥 ↔ 𝐵𝐹𝑥))
2	1	iotabidv 5340	. 2 ⊢ (𝐴 = 𝐵 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐵𝐹𝑥))
3		df-fv 5365	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5365	. 2 ⊢ (𝐹‘𝐵) = (℩𝑥𝐵𝐹𝑥)
5	2, 3, 4	3eqtr4g 2292	1 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))

Syntax hints:   → wi 4   = wceq 1398   class class class wbr 4114  ℩cio 5315  ‘cfv 5357

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 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-iota 5317  df-fv 5365

This theorem is referenced by:  fveq2i  5678  fveq2d  5679  2fveq3  5680  fvifdc  5697  dffn5imf  5737  fvelimab  5738  ssimaex  5743  fvco4  5754  fvmptssdm  5767  fvmptf  5775  eqfnfv2f  5784  fvelrn  5813  ralrnmpt  5824  rexrnmpt  5825  ffnfvf  5841  fmptco  5848  cofmpt  5851  fcompt  5852  fcoconst  5853  fsn2g  5857  fnressn  5875  fressnfv  5876  fconstfvm  5907  dfimafnf  5928  foco2  5932  funiunfvdmf  5943  f1veqaeq  5948  dff13f  5949  f1fveq  5951  f1elima  5952  f1ocnvfv  5958  f1ocnvfvb  5959  fcofo  5963  cocan2  5967  fliftfun  5975  isorel  5987  isocnv  5990  isotr  5995  f1oiso2  6006  canth  6009  imbrov2fvoveq  6083  ffnov  6165  eqfnov  6168  fnovim  6170  fnrnov  6208  foov  6209  funimassov  6212  ovelimab  6213  ofvalg  6285  ofrval  6286  offval2  6291  ofrfval2  6292  ofco  6294  caofinvl  6301  op1std  6355  op2ndd  6356  1stval2  6362  2ndval2  6363  unielxp  6381  reldm  6393  oprabco  6426  2ndconst  6431  f1o2ndf1  6437  elsuppfng  6455  elsuppfn  6456  mpoxopn0yelv  6483  mpoxopoveq  6484  smoel  6544  tfrlem1  6552  tfrlem3-2d  6556  tfrlem5  6558  tfrlem9  6563  tfr0dm  6566  tfrlemiubacc  6574  tfrlemi1  6576  tfrexlem  6578  tfr1onlemsucfn  6584  tfr1onlemsucaccv  6585  tfr1onlembxssdm  6587  tfr1onlembfn  6588  tfr1onlemubacc  6590  tfr1onlemaccex  6592  tfr1onlemres  6593  tfri1dALT  6595  tfrcllemsucfn  6597  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllembfn  6601  tfrcllemubacc  6603  tfrcllemaccex  6605  tfrcllemres  6606  tfrcldm  6607  tfrcl  6608  tfri3  6611  rdgtfr  6618  rdgss  6627  rdgisuc1  6628  rdgisucinc  6629  rdgon  6630  frecabex  6642  frecabcl  6643  frecfcllem  6648  frecsuclem  6650  frecsuc  6651  frecrdg  6652  oav  6700  omv  6701  oeiv  6702  fvixp  6951  cbvixp  6963  mptelixpg  6982  elixpsn  6983  dom2lem  7024  xpcomco  7090  xpmapen  7116  fidceq  7137  fieq0  7276  ordiso2  7339  djune  7382  updjudhcoinlf  7384  updjudhcoinrg  7385  updjud  7386  omp1eom  7399  0ct  7411  ctmlemr  7412  ctssdclemn0  7414  ctssdccl  7415  ctssdc  7417  enumctlemm  7418  nninfninc  7427  nnnninfeq  7432  nnnninfeq2  7433  enomnilem  7442  finomni  7444  fodjuomnilemdc  7448  fodju0  7451  fodjuomni  7453  ismkvnex  7459  fodjumkv  7464  nninfwlporlemd  7476  nninfwlpor  7478  exmidaclem  7528  cc1  7595  cc2lem  7596  cc2  7597  cc3  7598  mulpipq2  7702  genipv  7840  genpelxp  7842  addcanprleml  7945  addcanprlemu  7946  recexprlemm  7955  recexprlemdisj  7961  recexprlemloc  7962  recexprlem1ssl  7964  recexprlem1ssu  7965  cauappcvgprlemm  7976  cauappcvgprlemdisj  7982  cauappcvgprlemloc  7983  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  cauappcvgprlem1  7990  cauappcvgprlem2  7991  cauappcvgprlemlim  7992  cauappcvgpr  7993  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprlemm  7999  caucvgprlemdisj  8005  caucvgprlemloc  8006  caucvgprlemcl  8007  caucvgprlemladdfu  8008  caucvgprlemladdrl  8009  caucvgprlem1  8010  caucvgprlem2  8011  caucvgpr  8013  caucvgprprlemell  8016  caucvgprprlemelu  8017  caucvgprprlemcbv  8018  caucvgprprlemval  8019  caucvgprprlemnkeqj  8021  caucvgprprlemnbj  8024  caucvgprprlemml  8025  caucvgprprlemmu  8026  caucvgprprlemopl  8028  caucvgprprlemlol  8029  caucvgprprlemopu  8030  caucvgprprlemloc  8034  caucvgprprlemclphr  8036  caucvgprprlemexbt  8037  caucvgprprlem1  8040  caucvgprprlem2  8041  caucvgsrlemcl  8120  caucvgsrlemfv  8122  caucvgsrlembound  8125  caucvgsrlemgt1  8126  caucvgsrlemoffval  8127  caucvgsrlemoffres  8131  caucvgsrlembnd  8132  caucvgsr  8133  axcaucvglemcau  8229  axcaucvglemres  8230  uz11  9895  cnref1o  10001  fzprval  10438  fztpval  10439  zsupcllemex  10612  infssuzex  10615  suprzubdc  10620  frec2uzuzd  10788  frec2uzltd  10789  frec2uzlt2d  10790  frecuzrdgrrn  10794  frec2uzrdg  10795  frecuzrdgtcl  10798  frecuzrdgg  10802  frecuzrdgfunlem  10805  frecfzennn  10812  seqeq1  10836  iseqovex  10844  seq3val  10846  seqvalcd  10847  seq3-1  10848  seqf  10850  seq3p1  10851  seqovcd  10853  seqp1cd  10856  seq3clss  10857  seq3fveq2  10861  seqfveq2g  10863  seqfveqg  10864  seq3fveq  10865  seq3feq  10866  seq3shft2  10867  seqshft2g  10868  monoord  10871  monoord2  10872  ser3mono  10873  seq3split  10874  seqsplitg  10875  seq3caopr3  10877  seqcaopr3g  10878  seq3caopr2  10879  seqcaopr2g  10880  iseqf1olemkle  10883  iseqf1olemklt  10884  iseqf1olemqval  10886  iseqf1olemqk  10893  iseqf1olemjpcl  10894  iseqf1olemqpcl  10895  iseqf1olemfvp  10896  seq3f1olemqsumkj  10897  seq3f1olemqsum  10899  seq3f1olemstep  10900  seq3f1olemp  10901  seq3f1oleml  10902  seq3f1o  10903  seqf1oglem2a  10904  seqf1og  10907  seq3id2  10912  seq3homo  10913  seq3z  10914  seqhomog  10916  seqfeq4g  10917  ser3ge0  10922  ser3le  10923  exp3vallem  10926  exp3val  10927  facp1  11117  faccl  11122  facdiv  11125  facwordi  11127  faclbnd  11128  facubnd  11132  bcval  11136  bcval5  11150  fz1eqb  11178  omgadd  11191  hashxp  11216  hashmap  11217  hashfibc  11232  zfz1isolem1  11237  zfz1iso  11238  seq3coll  11239  eqwrd  11290  lswwrd  11296  lswex  11301  ccatfvalfi  11305  ccatval1  11310  ccatval2  11311  ccatalpha  11326  s1eq  11332  eqs1  11341  swrdval  11365  ccatopth2  11434  wrd2ind  11440  seq3shft  11548  reval  11559  replim  11569  cj11  11615  caucvgre  11691  cvg1nlemcau  11694  cvg1nlemres  11695  rexuz3  11700  absval  11711  resqrexlemover  11720  resqrexlemdecn  11722  resqrexlemlo  11723  resqrexlemcalc3  11726  resqrexlemnm  11728  resqrexlemcvg  11729  resqrexlemoverl  11731  resqrexlemglsq  11732  resqrexlemga  11733  resqrexlemsqa  11734  resqrexlemex  11735  abs00bd  11776  cau3lem  11824  caubnd2  11827  climconst  12000  climmpt  12010  climshftlemg  12012  climcn1  12018  climle  12044  climub  12054  climserle  12055  climcau  12057  climcvg1nlem  12059  climcvg1n  12060  serf0  12062  fsum3cvg  12089  summodclem3  12091  summodclem2a  12092  summodclem2  12093  summodc  12094  zsumdc  12095  fsum3  12098  fsumf1o  12101  fisumss  12103  fsum3cvg2  12105  fsum3ser  12108  fsumcl2lem  12109  fsumadd  12117  sumsnf  12120  isummulc2  12137  isumge0  12141  isumadd  12142  fsum2dlemstep  12145  fsummulc2  12159  fsumconst  12165  fsumrelem  12182  isumshft  12201  isum1p  12203  isumnn0nn  12204  isumrpcl  12205  isumlessdc  12207  cvgratnnlemnexp  12235  cvgratnnlemmn  12236  cvgratnnlemseq  12237  cvgratnnlemabsle  12238  cvgratnnlemfm  12240  cvgratnnlemrate  12241  cvgratnn  12242  cvgratz  12243  mertenslemi1  12246  mertenslem2  12247  mertensabs  12248  clim2prod  12250  prodfap0  12256  prodfrecap  12257  prodfdivap  12258  fproddccvg  12283  prodmodclem3  12286  prodmodclem2a  12287  prodmodclem2  12288  prodmodc  12289  zproddc  12290  fprodseq  12294  fprodf1o  12299  fprodssdc  12301  fprodmul  12302  prodsnf  12303  fprodfac  12326  fprodconst  12331  fprod2dlemstep  12333  eftvalcn  12368  ef0lem  12371  ege2le3  12382  efcj  12384  efaddlem  12385  eftlub  12401  efgt1p2  12406  reef11  12410  tanvalap  12419  efieq1re  12483  eirraplem  12488  dvdsabseq  12558  dvdsfac  12571  gcd0id  12700  nninfctlemfo  12761  nn0seqcvgd  12763  alginv  12769  algcvg  12770  algcvga  12773  algfx  12774  eucalglt  12779  lcmid  12802  qredeu  12819  prmfac1  12874  sqne2sq  12899  qnumdenbi  12914  dfphi2  12942  eulerthlemrprm  12951  eulerthlema  12952  eulerthlemh  12953  eulerthlemth  12954  phisum  12963  pcmpt  13066  pcfac  13073  1arithlem4  13089  elgz  13094  4sqlem4  13115  4sqlem12  13125  2expltfac  13162  ballotfilem2  13172  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfileme  13180  ballotfilemefi  13181  ballotfilemodife  13184  ballotfilem4  13185  ballotfilemi  13187  ballotfilemic  13194  ballotfilem1c  13195  ballotfilemrval  13205  ballotfilemrc  13218  ballotfilemrinv  13221  ballotfilemth  13225  ballotfi  13226  ennnfonelemk  13235  ennnfonelemp1  13241  ennnfoneleminc  13246  ennnfonelemkh  13247  ennnfonelemhf1o  13248  ennnfonelemex  13249  ennnfonelemhom  13250  ennnfonelemrn  13254  ennnfonelemnn0  13257  ennnfonelemr  13258  ennnfonelemim  13259  ctinfomlemom  13262  ctinfom  13263  ctiunctlemfo  13274  nninfdclemlt  13286  nninfdclemf1  13287  sloteq  13301  ressvalsets  13361  topnvalg  13548  imasex  13569  imasaddvallemg  13579  qusex  13589  xpsfrnel  13608  xpsfeq  13609  ismgm  13620  plusffvalg  13625  grpidvalg  13636  gsumfzval  13654  gsumval2  13660  issgrp  13666  ismnddef  13679  ismhm  13716  mhmex  13717  mhmlin  13722  issubm  13727  mhmeql  13747  isgrp  13761  grpn0  13790  grpinvfvalg  13797  grpsubfvalg  13800  grpsubval  13801  grpinv11  13824  grpinvnz  13826  mhmlem  13867  mulgfvalg  13874  mulgsubcl  13889  mulgaddcomlem  13898  mulgneg2  13909  mulgass  13912  issubg  13926  subgex  13929  issubg2m  13942  issubg4m  13946  0subg  13952  isnsg  13955  releqgg  13973  eqgex  13974  eqgval  13976  isghm  13996  ghmlin  14001  ghmrn  14010  ghmeql  14020  f1ghm0to0  14025  iscmn  14046  prdsbasprj  14124  prdsplusgfval  14126  prdsmulrfval  14128  prdsidlem  14135  prdsinvlem  14138  xpsval  14143  pws0g  14155  pwsinvg  14157  pwssub  14158  mgpvalg  14162  isrng  14173  issrg  14208  srgfcl  14216  isring  14243  iscrng  14246  mulgass2  14301  opprvalg  14312  dvdsrvald  14338  isunitd  14351  invrfvald  14367  dvrfvald  14378  dvrvald  14379  isrhm  14403  rhmval  14418  isnzr  14426  islring  14437  issubrng  14445  issubrg  14467  rrgval  14508  rrgsupp  14512  isdomn  14516  aprval  14529  aprap  14536  aprprop  14539  isdrngtap  14544  islmod  14565  scaffvalg  14580  lsssetm  14630  lspfval  14662  sraval  14711  rlmvalg  14728  2idlval  14776  2idlvalg  14777  cnfldmulg  14850  zlmval  14901  znf1o  14925  psrlinv  14965  mplsubgfilemcl  14980  istps  15023  clsfval  15092  cnpval  15189  lmconst  15207  txcnp  15262  upxp  15263  uptx  15265  txlm  15270  lmcn2  15271  cnmpt11  15274  cnmpt11f  15275  cnmpt1t  15276  cnmpt21  15282  cnmpt21f  15283  cnmpt2t  15284  mopnval  15433  isxms  15442  isms  15444  comet  15490  mopnex  15496  xmetxp  15498  xmetxpbl  15499  txmetcnp  15509  txmetcn  15510  qtopbasss  15512  cncfi  15569  cncfmpt1f  15589  ivthinclemlm  15625  ivthinclemum  15626  ivthinclemlopn  15627  ivthinclemlr  15628  ivthinclemuopn  15629  ivthinclemur  15630  ivthinclemdisj  15631  ivthinclemloc  15632  ivthinc  15634  ivthdec  15635  ivthreinc  15636  cnlimci  15664  limccnpcntop  15666  eldvap  15673  dvcoapbr  15698  dvcj  15700  dvfre  15701  dvmptcjx  15715  dveflem  15717  elply2  15726  elplyd  15732  plymullem1  15739  plyadd  15742  plymul  15743  plycoeid3  15748  plycolemc  15749  plyco  15750  plycjlemc  15751  plycj  15752  dvply1  15756  sin0pilem2  15773  pilem3  15774  coseq0q4123  15825  coseq0negpitopi  15827  cos11  15844  logltb  15865  rpcxpef  15885  rplogbval  15936  pellexlem1  15971  pellexlem3  15973  mpodvdsmulf1o  15984  fsumdvdsmul  15985  zabsle1  15998  lgslem2  16000  lgslem3  16001  lgsfcl2  16005  lgsfle1  16008  lgsle1  16014  lgsdirprm  16033  lgseisenlem2  16070  lgsquadlem2  16077  2sqlem1  16113  2sqlem2  16114  mul2sq  16115  2sqlem3  16116  2sqlem9  16123  2sqlem10  16124  vtxvalg  16137  iedgvalg  16138  edgvalg  16180  edgopval  16183  edgstruct  16185  isuhgrm  16192  isushgrm  16193  isupgren  16216  isumgren  16226  isuspgren  16278  isusgren  16279  umgr2edg1  16330  usgredg2vlem1  16343  usgredg2vlem2  16344  ushgredgedg  16347  issubgr  16378  vtxdgfval  16409  vtxedgfi  16410  vtxdg0v  16415  vtxdumgrfival  16419  1loopgrvd0fi  16427  1hevtxdg0fi  16428  1hevtxdg1en  16429  wkslem1  16441  wkslem2  16442  wksfval  16443  iswlk  16444  uspgr2wlkeq  16486  uspgr2wlkeqi  16488  2wlklem  16497  trlsfvalg  16504  clwwlkg  16514  isclwwlk  16515  clwwlkccatlem  16521  clwwlkng  16526  clwwlkn2  16542  clwwlkext2edg  16543  umgr2cwwk2dif  16545  umgr2cwwkdifex  16546  clwwlknonmpo  16549  clwwlknonel  16553  clwwlknonex2lem2  16559  eupthsg  16566  iseupth  16568  eupthseg  16573  eupth2lem3lem3fi  16591  eupth2lem3lem6fi  16592  eupth2lem3lem4fi  16594  eupth2lem3fi  16597  eupth2lemsfi  16599  eupth2fi  16600  eulerpathprum  16601  konigsberglem4  16612  depindlem1  16627  depindlem2  16628  depindlem3  16629  012of  16893  2o01f  16894  subctctexmid  16900  nnsf  16909  nninfalllem1  16912  nninffeq  16924  qdencn  16933  trilpolemclim  16946  trilpolemcl  16947  trilpolemisumle  16948  trilpolemeq1  16950  trilpolemlt1  16951  trilpo  16953  iswomni0  16962  redcwlpo  16966  dceqnconst  16972  dcapnconst  16973  nconstwlpolemgt0  16976  nconstwlpolem  16977  nconstwlpo  16978  neapmkv  16980