Theorem fveq2 5635

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 4089	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝑥 ↔ 𝐵𝐹𝑥))
2	1	iotabidv 5307	. 2 ⊢ (𝐴 = 𝐵 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐵𝐹𝑥))
3		df-fv 5332	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5332	. 2 ⊢ (𝐹‘𝐵) = (℩𝑥𝐵𝐹𝑥)
5	2, 3, 4	3eqtr4g 2287	1 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))

Syntax hints:   → wi 4   = wceq 1395   class class class wbr 4086  ℩cio 5282  ‘cfv 5324

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-iota 5284  df-fv 5332

This theorem is referenced by:  fveq2i  5638  fveq2d  5639  2fveq3  5640  fvifdc  5657  dffn5imf  5697  fvelimab  5698  ssimaex  5703  fvco4  5714  fvmptssdm  5727  fvmptf  5735  eqfnfv2f  5744  fvelrn  5774  ralrnmpt  5785  rexrnmpt  5786  ffnfvf  5802  fmptco  5809  cofmpt  5812  fcompt  5813  fcoconst  5814  fnressn  5835  fressnfv  5836  fconstfvm  5867  foco2  5889  funiunfvdmf  5900  f1veqaeq  5905  dff13f  5906  f1fveq  5908  f1elima  5909  f1ocnvfv  5915  f1ocnvfvb  5916  fcofo  5920  cocan2  5924  fliftfun  5932  isorel  5944  isocnv  5947  isotr  5952  f1oiso2  5963  canth  5964  imbrov2fvoveq  6038  ffnov  6120  eqfnov  6123  fnovim  6125  fnrnov  6163  foov  6164  funimassov  6167  ovelimab  6168  suppssfv  6226  ofvalg  6240  ofrval  6241  offval2  6246  ofrfval2  6247  ofco  6249  caofinvl  6256  op1std  6306  op2ndd  6307  1stval2  6313  2ndval2  6314  unielxp  6332  reldm  6344  oprabco  6377  2ndconst  6382  f1o2ndf1  6388  mpoxopn0yelv  6400  mpoxopoveq  6401  smoel  6461  tfrlem1  6469  tfrlem3-2d  6473  tfrlem5  6475  tfrlem9  6480  tfr0dm  6483  tfrlemiubacc  6491  tfrlemi1  6493  tfrexlem  6495  tfr1onlemsucfn  6501  tfr1onlemsucaccv  6502  tfr1onlembxssdm  6504  tfr1onlembfn  6505  tfr1onlemubacc  6507  tfr1onlemaccex  6509  tfr1onlemres  6510  tfri1dALT  6512  tfrcllemsucfn  6514  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllembfn  6518  tfrcllemubacc  6520  tfrcllemaccex  6522  tfrcllemres  6523  tfrcldm  6524  tfrcl  6525  tfri3  6528  rdgtfr  6535  rdgss  6544  rdgisuc1  6545  rdgisucinc  6546  rdgon  6547  frecabex  6559  frecabcl  6560  frecfcllem  6565  frecsuclem  6567  frecsuc  6568  frecrdg  6569  oav  6617  omv  6618  oeiv  6619  fvixp  6867  cbvixp  6879  mptelixpg  6898  elixpsn  6899  dom2lem  6940  xpcomco  7005  xpmapen  7031  fidceq  7051  fieq0  7166  ordiso2  7225  djune  7268  updjudhcoinlf  7270  updjudhcoinrg  7271  updjud  7272  omp1eom  7285  0ct  7297  ctmlemr  7298  ctssdclemn0  7300  ctssdccl  7301  ctssdc  7303  enumctlemm  7304  nninfninc  7313  nnnninfeq  7318  nnnninfeq2  7319  enomnilem  7328  finomni  7330  fodjuomnilemdc  7334  fodju0  7337  fodjuomni  7339  ismkvnex  7345  fodjumkv  7350  nninfwlporlemd  7362  nninfwlpor  7364  exmidaclem  7413  cc1  7474  cc2lem  7475  cc2  7476  cc3  7477  mulpipq2  7581  genipv  7719  genpelxp  7721  addcanprleml  7824  addcanprlemu  7825  recexprlemm  7834  recexprlemdisj  7840  recexprlemloc  7841  recexprlem1ssl  7843  recexprlem1ssu  7844  cauappcvgprlemm  7855  cauappcvgprlemdisj  7861  cauappcvgprlemloc  7862  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  cauappcvgprlem1  7869  cauappcvgprlem2  7870  cauappcvgprlemlim  7871  cauappcvgpr  7872  caucvgprlemnkj  7876  caucvgprlemnbj  7877  caucvgprlemm  7878  caucvgprlemdisj  7884  caucvgprlemloc  7885  caucvgprlemcl  7886  caucvgprlemladdfu  7887  caucvgprlemladdrl  7888  caucvgprlem1  7889  caucvgprlem2  7890  caucvgpr  7892  caucvgprprlemell  7895  caucvgprprlemelu  7896  caucvgprprlemcbv  7897  caucvgprprlemval  7898  caucvgprprlemnkeqj  7900  caucvgprprlemnbj  7903  caucvgprprlemml  7904  caucvgprprlemmu  7905  caucvgprprlemopl  7907  caucvgprprlemlol  7908  caucvgprprlemopu  7909  caucvgprprlemloc  7913  caucvgprprlemclphr  7915  caucvgprprlemexbt  7916  caucvgprprlem1  7919  caucvgprprlem2  7920  caucvgsrlemcl  7999  caucvgsrlemfv  8001  caucvgsrlembound  8004  caucvgsrlemgt1  8005  caucvgsrlemoffval  8006  caucvgsrlemoffres  8010  caucvgsrlembnd  8011  caucvgsr  8012  axcaucvglemcau  8108  axcaucvglemres  8109  uz11  9769  cnref1o  9875  fzprval  10307  fztpval  10308  zsupcllemex  10480  infssuzex  10483  suprzubdc  10486  frec2uzuzd  10654  frec2uzltd  10655  frec2uzlt2d  10656  frecuzrdgrrn  10660  frec2uzrdg  10661  frecuzrdgtcl  10664  frecuzrdgg  10668  frecuzrdgfunlem  10671  frecfzennn  10678  seqeq1  10702  iseqovex  10710  seq3val  10712  seqvalcd  10713  seq3-1  10714  seqf  10716  seq3p1  10717  seqovcd  10719  seqp1cd  10722  seq3clss  10723  seq3fveq2  10727  seqfveq2g  10729  seqfveqg  10730  seq3fveq  10731  seq3feq  10732  seq3shft2  10733  seqshft2g  10734  monoord  10737  monoord2  10738  ser3mono  10739  seq3split  10740  seqsplitg  10741  seq3caopr3  10743  seqcaopr3g  10744  seq3caopr2  10745  seqcaopr2g  10746  iseqf1olemkle  10749  iseqf1olemklt  10750  iseqf1olemqval  10752  iseqf1olemqk  10759  iseqf1olemjpcl  10760  iseqf1olemqpcl  10761  iseqf1olemfvp  10762  seq3f1olemqsumkj  10763  seq3f1olemqsum  10765  seq3f1olemstep  10766  seq3f1olemp  10767  seq3f1oleml  10768  seq3f1o  10769  seqf1oglem2a  10770  seqf1og  10773  seq3id2  10778  seq3homo  10779  seq3z  10780  seqhomog  10782  seqfeq4g  10783  ser3ge0  10788  ser3le  10789  exp3vallem  10792  exp3val  10793  facp1  10982  faccl  10987  facdiv  10990  facwordi  10992  faclbnd  10993  facubnd  10997  bcval  11001  bcval5  11015  fz1eqb  11042  omgadd  11055  hashxp  11080  zfz1isolem1  11094  zfz1iso  11095  seq3coll  11096  eqwrd  11144  lswwrd  11150  lswex  11155  ccatfvalfi  11159  ccatval1  11164  ccatval2  11165  ccatalpha  11180  s1eq  11186  eqs1  11195  swrdval  11219  ccatopth2  11288  wrd2ind  11294  seq3shft  11389  reval  11400  replim  11410  cj11  11456  caucvgre  11532  cvg1nlemcau  11535  cvg1nlemres  11536  rexuz3  11541  absval  11552  resqrexlemover  11561  resqrexlemdecn  11563  resqrexlemlo  11564  resqrexlemcalc3  11567  resqrexlemnm  11569  resqrexlemcvg  11570  resqrexlemoverl  11572  resqrexlemglsq  11573  resqrexlemga  11574  resqrexlemsqa  11575  resqrexlemex  11576  abs00bd  11617  cau3lem  11665  caubnd2  11668  climconst  11841  climmpt  11851  climshftlemg  11853  climcn1  11859  climle  11885  climub  11895  climserle  11896  climcau  11898  climcvg1nlem  11900  climcvg1n  11901  serf0  11903  fsum3cvg  11929  summodclem3  11931  summodclem2a  11932  summodclem2  11933  summodc  11934  zsumdc  11935  fsum3  11938  fsumf1o  11941  fisumss  11943  fsum3cvg2  11945  fsum3ser  11948  fsumcl2lem  11949  fsumadd  11957  sumsnf  11960  isummulc2  11977  isumge0  11981  isumadd  11982  fsum2dlemstep  11985  fsummulc2  11999  fsumconst  12005  fsumrelem  12022  isumshft  12041  isum1p  12043  isumnn0nn  12044  isumrpcl  12045  isumlessdc  12047  cvgratnnlemnexp  12075  cvgratnnlemmn  12076  cvgratnnlemseq  12077  cvgratnnlemabsle  12078  cvgratnnlemfm  12080  cvgratnnlemrate  12081  cvgratnn  12082  cvgratz  12083  mertenslemi1  12086  mertenslem2  12087  mertensabs  12088  clim2prod  12090  prodfap0  12096  prodfrecap  12097  prodfdivap  12098  fproddccvg  12123  prodmodclem3  12126  prodmodclem2a  12127  prodmodclem2  12128  prodmodc  12129  zproddc  12130  fprodseq  12134  fprodf1o  12139  fprodssdc  12141  fprodmul  12142  prodsnf  12143  fprodfac  12166  fprodconst  12171  fprod2dlemstep  12173  eftvalcn  12208  ef0lem  12211  ege2le3  12222  efcj  12224  efaddlem  12225  eftlub  12241  efgt1p2  12246  reef11  12250  tanvalap  12259  efieq1re  12323  eirraplem  12328  dvdsabseq  12398  dvdsfac  12411  gcd0id  12540  nninfctlemfo  12601  nn0seqcvgd  12603  alginv  12609  algcvg  12610  algcvga  12613  algfx  12614  eucalglt  12619  lcmid  12642  qredeu  12659  prmfac1  12714  sqne2sq  12739  qnumdenbi  12754  dfphi2  12782  eulerthlemrprm  12791  eulerthlema  12792  eulerthlemh  12793  eulerthlemth  12794  phisum  12803  pcmpt  12906  pcfac  12913  1arithlem4  12929  elgz  12934  4sqlem4  12955  4sqlem12  12965  2expltfac  13002  ennnfonelemk  13011  ennnfonelemp1  13017  ennnfoneleminc  13022  ennnfonelemkh  13023  ennnfonelemhf1o  13024  ennnfonelemex  13025  ennnfonelemhom  13026  ennnfonelemrn  13030  ennnfonelemnn0  13033  ennnfonelemr  13034  ennnfonelemim  13035  ctinfomlemom  13038  ctinfom  13039  ctiunctlemfo  13050  nninfdclemlt  13062  nninfdclemf1  13063  sloteq  13077  ressvalsets  13137  topnvalg  13324  prdsbasprj  13355  prdsplusgfval  13357  prdsmulrfval  13359  imasex  13378  imasaddvallemg  13388  qusex  13398  xpsfrnel  13417  xpsfeq  13418  xpsval  13425  ismgm  13430  plusffvalg  13435  grpidvalg  13446  gsumfzval  13464  gsumval2  13470  issgrp  13476  ismnddef  13491  prdsidlem  13520  pws0g  13524  ismhm  13534  mhmex  13535  mhmlin  13540  issubm  13545  mhmeql  13565  isgrp  13579  grpn0  13608  grpinvfvalg  13615  grpsubfvalg  13618  grpsubval  13619  grpinv11  13642  grpinvnz  13644  prdsinvlem  13681  pwsinvg  13685  pwssub  13686  mhmlem  13691  mulgfvalg  13698  mulgsubcl  13713  mulgaddcomlem  13722  mulgneg2  13733  mulgass  13736  issubg  13750  subgex  13753  issubg2m  13766  issubg4m  13770  0subg  13776  isnsg  13779  releqgg  13797  eqgex  13798  eqgval  13800  isghm  13820  ghmlin  13825  ghmrn  13834  ghmeql  13844  f1ghm0to0  13849  iscmn  13870  mgpvalg  13926  isrng  13937  issrg  13968  srgfcl  13976  isring  14003  iscrng  14006  mulgass2  14061  opprvalg  14072  dvdsrvald  14097  isunitd  14110  invrfvald  14126  dvrfvald  14137  dvrvald  14138  isrhm  14162  rhmval  14177  isnzr  14185  islring  14196  issubrng  14203  issubrg  14225  rrgval  14266  isdomn  14273  aprval  14286  aprap  14290  islmod  14295  scaffvalg  14310  lsssetm  14360  lspfval  14392  sraval  14441  rlmvalg  14458  2idlval  14506  2idlvalg  14507  cnfldmulg  14580  zlmval  14631  znf1o  14655  psrlinv  14688  mplsubgfilemcl  14703  istps  14746  clsfval  14815  cnpval  14912  lmconst  14930  txcnp  14985  upxp  14986  uptx  14988  txlm  14993  lmcn2  14994  cnmpt11  14997  cnmpt11f  14998  cnmpt1t  14999  cnmpt21  15005  cnmpt21f  15006  cnmpt2t  15007  mopnval  15156  isxms  15165  isms  15167  comet  15213  mopnex  15219  xmetxp  15221  xmetxpbl  15222  txmetcnp  15232  txmetcn  15233  qtopbasss  15235  cncfi  15292  cncfmpt1f  15312  ivthinclemlm  15348  ivthinclemum  15349  ivthinclemlopn  15350  ivthinclemlr  15351  ivthinclemuopn  15352  ivthinclemur  15353  ivthinclemdisj  15354  ivthinclemloc  15355  ivthinc  15357  ivthdec  15358  ivthreinc  15359  cnlimci  15387  limccnpcntop  15389  eldvap  15396  dvcoapbr  15421  dvcj  15423  dvfre  15424  dvmptcjx  15438  dveflem  15440  elply2  15449  elplyd  15455  plymullem1  15462  plyadd  15465  plymul  15466  plycoeid3  15471  plycolemc  15472  plyco  15473  plycjlemc  15474  plycj  15475  dvply1  15479  sin0pilem2  15496  pilem3  15497  coseq0q4123  15548  coseq0negpitopi  15550  cos11  15567  logltb  15588  rpcxpef  15608  rplogbval  15659  mpodvdsmulf1o  15704  fsumdvdsmul  15705  zabsle1  15718  lgslem2  15720  lgslem3  15721  lgsfcl2  15725  lgsfle1  15728  lgsle1  15734  lgsdirprm  15753  lgseisenlem2  15790  lgsquadlem2  15797  2sqlem1  15833  2sqlem2  15834  mul2sq  15835  2sqlem3  15836  2sqlem9  15843  2sqlem10  15844  vtxvalg  15857  iedgvalg  15858  edgvalg  15900  edgopval  15903  edgstruct  15905  isuhgrm  15912  isushgrm  15913  isupgren  15936  isumgren  15946  isuspgren  15996  isusgren  15997  umgr2edg1  16048  usgredg2vlem1  16061  usgredg2vlem2  16062  ushgredgedg  16065  vtxdgfval  16094  vtxedgfi  16095  vtxdg0v  16100  vtxdumgrfival  16104  1loopgrvd0fi  16112  1hevtxdg0fi  16113  wkslem1  16117  wkslem2  16118  wksfval  16119  iswlk  16120  uspgr2wlkeq  16162  uspgr2wlkeqi  16164  2wlklem  16171  trlsfvalg  16178  clwwlkg  16188  isclwwlk  16189  clwwlkccatlem  16195  clwwlkng  16200  clwwlkn2  16216  clwwlkext2edg  16217  umgr2cwwk2dif  16219  umgr2cwwkdifex  16220  clwwlknonmpo  16223  clwwlknonel  16227  clwwlknonex2lem2  16233  eupthsg  16240  iseupth  16242  eupthseg  16247  012of  16528  2o01f  16529  subctctexmid  16537  nnsf  16543  nninfalllem1  16546  nninffeq  16558  qdencn  16567  trilpolemclim  16576  trilpolemcl  16577  trilpolemisumle  16578  trilpolemeq1  16580  trilpolemlt1  16581  trilpo  16583  iswomni0  16591  redcwlpo  16595  dceqnconst  16600  dcapnconst  16601  nconstwlpolemgt0  16604  nconstwlpolem  16605  nconstwlpo  16606  neapmkv  16608