Theorem fveq2 5561

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 4037	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝑥 ↔ 𝐵𝐹𝑥))
2	1	iotabidv 5242	. 2 ⊢ (𝐴 = 𝐵 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐵𝐹𝑥))
3		df-fv 5267	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5267	. 2 ⊢ (𝐹‘𝐵) = (℩𝑥𝐵𝐹𝑥)
5	2, 3, 4	3eqtr4g 2254	1 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))

Syntax hints:   → wi 4   = wceq 1364   class class class wbr 4034  ℩cio 5218  ‘cfv 5259

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267

This theorem is referenced by:  fveq2i  5564  fveq2d  5565  2fveq3  5566  fvifdc  5583  dffn5imf  5619  fvelimab  5620  ssimaex  5625  fvco4  5636  fvmptssdm  5649  fvmptf  5657  eqfnfv2f  5666  fvelrn  5696  ralrnmpt  5707  rexrnmpt  5708  ffnfvf  5724  fmptco  5731  cofmpt  5734  fcompt  5735  fcoconst  5736  fnressn  5751  fressnfv  5752  fconstfvm  5783  foco2  5803  funiunfvdmf  5814  f1veqaeq  5819  dff13f  5820  f1fveq  5822  f1elima  5823  f1ocnvfv  5829  f1ocnvfvb  5830  fcofo  5834  cocan2  5838  fliftfun  5846  isorel  5858  isocnv  5861  isotr  5866  f1oiso2  5877  canth  5878  imbrov2fvoveq  5950  ffnov  6030  eqfnov  6033  fnovim  6035  fnrnov  6073  foov  6074  funimassov  6077  ovelimab  6078  suppssfv  6135  ofvalg  6149  ofrval  6150  offval2  6155  ofrfval2  6156  ofco  6158  caofinvl  6164  op1std  6210  op2ndd  6211  1stval2  6217  2ndval2  6218  unielxp  6236  reldm  6248  oprabco  6279  2ndconst  6284  f1o2ndf1  6290  mpoxopn0yelv  6301  mpoxopoveq  6302  smoel  6362  tfrlem1  6370  tfrlem3-2d  6374  tfrlem5  6376  tfrlem9  6381  tfr0dm  6384  tfrlemiubacc  6392  tfrlemi1  6394  tfrexlem  6396  tfr1onlemsucfn  6402  tfr1onlemsucaccv  6403  tfr1onlembxssdm  6405  tfr1onlembfn  6406  tfr1onlemubacc  6408  tfr1onlemaccex  6410  tfr1onlemres  6411  tfri1dALT  6413  tfrcllemsucfn  6415  tfrcllemsucaccv  6416  tfrcllembxssdm  6418  tfrcllembfn  6419  tfrcllemubacc  6421  tfrcllemaccex  6423  tfrcllemres  6424  tfrcldm  6425  tfrcl  6426  tfri3  6429  rdgtfr  6436  rdgss  6445  rdgisuc1  6446  rdgisucinc  6447  rdgon  6448  frecabex  6460  frecabcl  6461  frecfcllem  6466  frecsuclem  6468  frecsuc  6469  frecrdg  6470  oav  6516  omv  6517  oeiv  6518  fvixp  6766  cbvixp  6778  mptelixpg  6797  elixpsn  6798  dom2lem  6835  xpcomco  6889  xpmapen  6915  fidceq  6934  fieq0  7046  ordiso2  7105  djune  7148  updjudhcoinlf  7150  updjudhcoinrg  7151  updjud  7152  omp1eom  7165  0ct  7177  ctmlemr  7178  ctssdclemn0  7180  ctssdccl  7181  ctssdc  7183  enumctlemm  7184  nninfninc  7193  nnnninfeq  7198  nnnninfeq2  7199  enomnilem  7208  finomni  7210  fodjuomnilemdc  7214  fodju0  7217  fodjuomni  7219  ismkvnex  7225  fodjumkv  7230  nninfwlporlemd  7242  nninfwlpor  7244  exmidaclem  7280  cc1  7337  cc2lem  7338  cc2  7339  cc3  7340  mulpipq2  7443  genipv  7581  genpelxp  7583  addcanprleml  7686  addcanprlemu  7687  recexprlemm  7696  recexprlemdisj  7702  recexprlemloc  7703  recexprlem1ssl  7705  recexprlem1ssu  7706  cauappcvgprlemm  7717  cauappcvgprlemdisj  7723  cauappcvgprlemloc  7724  cauappcvgprlemladdru  7728  cauappcvgprlemladdrl  7729  cauappcvgprlem1  7731  cauappcvgprlem2  7732  cauappcvgprlemlim  7733  cauappcvgpr  7734  caucvgprlemnkj  7738  caucvgprlemnbj  7739  caucvgprlemm  7740  caucvgprlemdisj  7746  caucvgprlemloc  7747  caucvgprlemcl  7748  caucvgprlemladdfu  7749  caucvgprlemladdrl  7750  caucvgprlem1  7751  caucvgprlem2  7752  caucvgpr  7754  caucvgprprlemell  7757  caucvgprprlemelu  7758  caucvgprprlemcbv  7759  caucvgprprlemval  7760  caucvgprprlemnkeqj  7762  caucvgprprlemnbj  7765  caucvgprprlemml  7766  caucvgprprlemmu  7767  caucvgprprlemopl  7769  caucvgprprlemlol  7770  caucvgprprlemopu  7771  caucvgprprlemloc  7775  caucvgprprlemclphr  7777  caucvgprprlemexbt  7778  caucvgprprlem1  7781  caucvgprprlem2  7782  caucvgsrlemcl  7861  caucvgsrlemfv  7863  caucvgsrlembound  7866  caucvgsrlemgt1  7867  caucvgsrlemoffval  7868  caucvgsrlemoffres  7872  caucvgsrlembnd  7873  caucvgsr  7874  axcaucvglemcau  7970  axcaucvglemres  7971  uz11  9629  cnref1o  9730  fzprval  10162  fztpval  10163  zsupcllemex  10325  infssuzex  10328  suprzubdc  10331  frec2uzuzd  10499  frec2uzltd  10500  frec2uzlt2d  10501  frecuzrdgrrn  10505  frec2uzrdg  10506  frecuzrdgtcl  10509  frecuzrdgg  10513  frecuzrdgfunlem  10516  frecfzennn  10523  seqeq1  10547  iseqovex  10555  seq3val  10557  seqvalcd  10558  seq3-1  10559  seqf  10561  seq3p1  10562  seqovcd  10564  seqp1cd  10567  seq3clss  10568  seq3fveq2  10572  seqfveq2g  10574  seqfveqg  10575  seq3fveq  10576  seq3feq  10577  seq3shft2  10578  seqshft2g  10579  monoord  10582  monoord2  10583  ser3mono  10584  seq3split  10585  seqsplitg  10586  seq3caopr3  10588  seqcaopr3g  10589  seq3caopr2  10590  seqcaopr2g  10591  iseqf1olemkle  10594  iseqf1olemklt  10595  iseqf1olemqval  10597  iseqf1olemqk  10604  iseqf1olemjpcl  10605  iseqf1olemqpcl  10606  iseqf1olemfvp  10607  seq3f1olemqsumkj  10608  seq3f1olemqsum  10610  seq3f1olemstep  10611  seq3f1olemp  10612  seq3f1oleml  10613  seq3f1o  10614  seqf1oglem2a  10615  seqf1og  10618  seq3id2  10623  seq3homo  10624  seq3z  10625  seqhomog  10627  seqfeq4g  10628  ser3ge0  10633  ser3le  10634  exp3vallem  10637  exp3val  10638  facp1  10827  faccl  10832  facdiv  10835  facwordi  10837  faclbnd  10838  facubnd  10842  bcval  10846  bcval5  10860  fz1eqb  10887  omgadd  10899  hashxp  10923  zfz1isolem1  10937  zfz1iso  10938  seq3coll  10939  eqwrd  10980  seq3shft  11008  reval  11019  replim  11029  cj11  11075  caucvgre  11151  cvg1nlemcau  11154  cvg1nlemres  11155  rexuz3  11160  absval  11171  resqrexlemover  11180  resqrexlemdecn  11182  resqrexlemlo  11183  resqrexlemcalc3  11186  resqrexlemnm  11188  resqrexlemcvg  11189  resqrexlemoverl  11191  resqrexlemglsq  11192  resqrexlemga  11193  resqrexlemsqa  11194  resqrexlemex  11195  abs00bd  11236  cau3lem  11284  caubnd2  11287  climconst  11460  climmpt  11470  climshftlemg  11472  climcn1  11478  climle  11504  climub  11514  climserle  11515  climcau  11517  climcvg1nlem  11519  climcvg1n  11520  serf0  11522  fsum3cvg  11548  summodclem3  11550  summodclem2a  11551  summodclem2  11552  summodc  11553  zsumdc  11554  fsum3  11557  fsumf1o  11560  fisumss  11562  fsum3cvg2  11564  fsum3ser  11567  fsumcl2lem  11568  fsumadd  11576  sumsnf  11579  isummulc2  11596  isumge0  11600  isumadd  11601  fsum2dlemstep  11604  fsummulc2  11618  fsumconst  11624  fsumrelem  11641  isumshft  11660  isum1p  11662  isumnn0nn  11663  isumrpcl  11664  isumlessdc  11666  cvgratnnlemnexp  11694  cvgratnnlemmn  11695  cvgratnnlemseq  11696  cvgratnnlemabsle  11697  cvgratnnlemfm  11699  cvgratnnlemrate  11700  cvgratnn  11701  cvgratz  11702  mertenslemi1  11705  mertenslem2  11706  mertensabs  11707  clim2prod  11709  prodfap0  11715  prodfrecap  11716  prodfdivap  11717  fproddccvg  11742  prodmodclem3  11745  prodmodclem2a  11746  prodmodclem2  11747  prodmodc  11748  zproddc  11749  fprodseq  11753  fprodf1o  11758  fprodssdc  11760  fprodmul  11761  prodsnf  11762  fprodfac  11785  fprodconst  11790  fprod2dlemstep  11792  eftvalcn  11827  ef0lem  11830  ege2le3  11841  efcj  11843  efaddlem  11844  eftlub  11860  efgt1p2  11865  reef11  11869  tanvalap  11878  efieq1re  11942  eirraplem  11947  dvdsabseq  12017  dvdsfac  12030  gcd0id  12159  nninfctlemfo  12220  nn0seqcvgd  12222  alginv  12228  algcvg  12229  algcvga  12232  algfx  12233  eucalglt  12238  lcmid  12261  qredeu  12278  prmfac1  12333  sqne2sq  12358  qnumdenbi  12373  dfphi2  12401  eulerthlemrprm  12410  eulerthlema  12411  eulerthlemh  12412  eulerthlemth  12413  phisum  12422  pcmpt  12525  pcfac  12532  1arithlem4  12548  elgz  12553  4sqlem4  12574  4sqlem12  12584  2expltfac  12621  ennnfonelemk  12630  ennnfonelemp1  12636  ennnfoneleminc  12641  ennnfonelemkh  12642  ennnfonelemhf1o  12643  ennnfonelemex  12644  ennnfonelemhom  12645  ennnfonelemrn  12649  ennnfonelemnn0  12652  ennnfonelemr  12653  ennnfonelemim  12654  ctinfomlemom  12657  ctinfom  12658  ctiunctlemfo  12669  nninfdclemlt  12681  nninfdclemf1  12682  sloteq  12696  ressvalsets  12755  topnvalg  12941  prdsbasprj  12972  prdsplusgfval  12974  prdsmulrfval  12976  imasex  12995  imasaddvallemg  13005  qusex  13015  xpsfrnel  13034  xpsfeq  13035  xpsval  13042  ismgm  13047  plusffvalg  13052  grpidvalg  13063  gsumfzval  13081  gsumval2  13087  issgrp  13093  ismnddef  13106  ismhm  13140  mhmex  13141  mhmlin  13146  issubm  13151  mhmeql  13171  isgrp  13185  grpn0  13214  grpinvfvalg  13221  grpsubfvalg  13224  grpsubval  13225  grpinv11  13248  grpinvnz  13250  mhmlem  13291  mulgfvalg  13298  mulgsubcl  13313  mulgaddcomlem  13322  mulgneg2  13333  mulgass  13336  issubg  13350  subgex  13353  issubg2m  13366  issubg4m  13370  0subg  13376  isnsg  13379  releqgg  13397  eqgex  13398  eqgval  13400  isghm  13420  ghmlin  13425  ghmrn  13434  ghmeql  13444  f1ghm0to0  13449  iscmn  13470  mgpvalg  13526  isrng  13537  issrg  13568  srgfcl  13576  isring  13603  iscrng  13606  mulgass2  13661  opprvalg  13672  reldvdsrsrg  13695  dvdsrvald  13696  isunitd  13709  invrfvald  13725  dvrfvald  13736  dvrvald  13737  isrhm  13761  rhmval  13776  isnzr  13784  islring  13795  issubrng  13802  issubrg  13824  rrgval  13865  isdomn  13872  aprval  13885  aprap  13889  islmod  13894  scaffvalg  13909  lsssetm  13959  lspfval  13991  sraval  14040  rlmvalg  14057  2idlval  14105  2idlvalg  14106  cnfldmulg  14179  zlmval  14230  znf1o  14254  istps  14315  clsfval  14384  cnpval  14481  lmconst  14499  txcnp  14554  upxp  14555  uptx  14557  txlm  14562  lmcn2  14563  cnmpt11  14566  cnmpt11f  14567  cnmpt1t  14568  cnmpt21  14574  cnmpt21f  14575  cnmpt2t  14576  mopnval  14725  isxms  14734  isms  14736  comet  14782  mopnex  14788  xmetxp  14790  xmetxpbl  14791  txmetcnp  14801  txmetcn  14802  qtopbasss  14804  cncfi  14861  cncfmpt1f  14881  ivthinclemlm  14917  ivthinclemum  14918  ivthinclemlopn  14919  ivthinclemlr  14920  ivthinclemuopn  14921  ivthinclemur  14922  ivthinclemdisj  14923  ivthinclemloc  14924  ivthinc  14926  ivthdec  14927  ivthreinc  14928  cnlimci  14956  limccnpcntop  14958  eldvap  14965  dvcoapbr  14990  dvcj  14992  dvfre  14993  dvmptcjx  15007  dveflem  15009  elply2  15018  elplyd  15024  plymullem1  15031  plyadd  15034  plymul  15035  plycoeid3  15040  plycolemc  15041  plyco  15042  plycjlemc  15043  plycj  15044  dvply1  15048  sin0pilem2  15065  pilem3  15066  coseq0q4123  15117  coseq0negpitopi  15119  cos11  15136  logltb  15157  rpcxpef  15177  rplogbval  15228  mpodvdsmulf1o  15273  fsumdvdsmul  15274  zabsle1  15287  lgslem2  15289  lgslem3  15290  lgsfcl2  15294  lgsfle1  15297  lgsle1  15303  lgsdirprm  15322  lgseisenlem2  15359  lgsquadlem2  15366  2sqlem1  15402  2sqlem2  15403  mul2sq  15404  2sqlem3  15405  2sqlem9  15412  2sqlem10  15413  012of  15687  2o01f  15688  subctctexmid  15694  nnsf  15699  nninfalllem1  15702  nninffeq  15714  qdencn  15721  trilpolemclim  15730  trilpolemcl  15731  trilpolemisumle  15732  trilpolemeq1  15734  trilpolemlt1  15735  trilpo  15737  iswomni0  15745  redcwlpo  15749  dceqnconst  15754  dcapnconst  15755  nconstwlpolemgt0  15758  nconstwlpolem  15759  nconstwlpo  15760  neapmkv  15762