Theorem fveq2 5576

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 4047	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝑥 ↔ 𝐵𝐹𝑥))
2	1	iotabidv 5254	. 2 ⊢ (𝐴 = 𝐵 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐵𝐹𝑥))
3		df-fv 5279	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5279	. 2 ⊢ (𝐹‘𝐵) = (℩𝑥𝐵𝐹𝑥)
5	2, 3, 4	3eqtr4g 2263	1 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))

Syntax hints:   → wi 4   = wceq 1373   class class class wbr 4044  ℩cio 5230  ‘cfv 5271

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4045  df-iota 5232  df-fv 5279

This theorem is referenced by:  fveq2i  5579  fveq2d  5580  2fveq3  5581  fvifdc  5598  dffn5imf  5634  fvelimab  5635  ssimaex  5640  fvco4  5651  fvmptssdm  5664  fvmptf  5672  eqfnfv2f  5681  fvelrn  5711  ralrnmpt  5722  rexrnmpt  5723  ffnfvf  5739  fmptco  5746  cofmpt  5749  fcompt  5750  fcoconst  5751  fnressn  5770  fressnfv  5771  fconstfvm  5802  foco2  5822  funiunfvdmf  5833  f1veqaeq  5838  dff13f  5839  f1fveq  5841  f1elima  5842  f1ocnvfv  5848  f1ocnvfvb  5849  fcofo  5853  cocan2  5857  fliftfun  5865  isorel  5877  isocnv  5880  isotr  5885  f1oiso2  5896  canth  5897  imbrov2fvoveq  5969  ffnov  6049  eqfnov  6052  fnovim  6054  fnrnov  6092  foov  6093  funimassov  6096  ovelimab  6097  suppssfv  6154  ofvalg  6168  ofrval  6169  offval2  6174  ofrfval2  6175  ofco  6177  caofinvl  6184  op1std  6234  op2ndd  6235  1stval2  6241  2ndval2  6242  unielxp  6260  reldm  6272  oprabco  6303  2ndconst  6308  f1o2ndf1  6314  mpoxopn0yelv  6325  mpoxopoveq  6326  smoel  6386  tfrlem1  6394  tfrlem3-2d  6398  tfrlem5  6400  tfrlem9  6405  tfr0dm  6408  tfrlemiubacc  6416  tfrlemi1  6418  tfrexlem  6420  tfr1onlemsucfn  6426  tfr1onlemsucaccv  6427  tfr1onlembxssdm  6429  tfr1onlembfn  6430  tfr1onlemubacc  6432  tfr1onlemaccex  6434  tfr1onlemres  6435  tfri1dALT  6437  tfrcllemsucfn  6439  tfrcllemsucaccv  6440  tfrcllembxssdm  6442  tfrcllembfn  6443  tfrcllemubacc  6445  tfrcllemaccex  6447  tfrcllemres  6448  tfrcldm  6449  tfrcl  6450  tfri3  6453  rdgtfr  6460  rdgss  6469  rdgisuc1  6470  rdgisucinc  6471  rdgon  6472  frecabex  6484  frecabcl  6485  frecfcllem  6490  frecsuclem  6492  frecsuc  6493  frecrdg  6494  oav  6540  omv  6541  oeiv  6542  fvixp  6790  cbvixp  6802  mptelixpg  6821  elixpsn  6822  dom2lem  6863  xpcomco  6921  xpmapen  6947  fidceq  6966  fieq0  7078  ordiso2  7137  djune  7180  updjudhcoinlf  7182  updjudhcoinrg  7183  updjud  7184  omp1eom  7197  0ct  7209  ctmlemr  7210  ctssdclemn0  7212  ctssdccl  7213  ctssdc  7215  enumctlemm  7216  nninfninc  7225  nnnninfeq  7230  nnnninfeq2  7231  enomnilem  7240  finomni  7242  fodjuomnilemdc  7246  fodju0  7249  fodjuomni  7251  ismkvnex  7257  fodjumkv  7262  nninfwlporlemd  7274  nninfwlpor  7276  exmidaclem  7320  cc1  7377  cc2lem  7378  cc2  7379  cc3  7380  mulpipq2  7484  genipv  7622  genpelxp  7624  addcanprleml  7727  addcanprlemu  7728  recexprlemm  7737  recexprlemdisj  7743  recexprlemloc  7744  recexprlem1ssl  7746  recexprlem1ssu  7747  cauappcvgprlemm  7758  cauappcvgprlemdisj  7764  cauappcvgprlemloc  7765  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  cauappcvgprlem1  7772  cauappcvgprlem2  7773  cauappcvgprlemlim  7774  cauappcvgpr  7775  caucvgprlemnkj  7779  caucvgprlemnbj  7780  caucvgprlemm  7781  caucvgprlemdisj  7787  caucvgprlemloc  7788  caucvgprlemcl  7789  caucvgprlemladdfu  7790  caucvgprlemladdrl  7791  caucvgprlem1  7792  caucvgprlem2  7793  caucvgpr  7795  caucvgprprlemell  7798  caucvgprprlemelu  7799  caucvgprprlemcbv  7800  caucvgprprlemval  7801  caucvgprprlemnkeqj  7803  caucvgprprlemnbj  7806  caucvgprprlemml  7807  caucvgprprlemmu  7808  caucvgprprlemopl  7810  caucvgprprlemlol  7811  caucvgprprlemopu  7812  caucvgprprlemloc  7816  caucvgprprlemclphr  7818  caucvgprprlemexbt  7819  caucvgprprlem1  7822  caucvgprprlem2  7823  caucvgsrlemcl  7902  caucvgsrlemfv  7904  caucvgsrlembound  7907  caucvgsrlemgt1  7908  caucvgsrlemoffval  7909  caucvgsrlemoffres  7913  caucvgsrlembnd  7914  caucvgsr  7915  axcaucvglemcau  8011  axcaucvglemres  8012  uz11  9671  cnref1o  9772  fzprval  10204  fztpval  10205  zsupcllemex  10373  infssuzex  10376  suprzubdc  10379  frec2uzuzd  10547  frec2uzltd  10548  frec2uzlt2d  10549  frecuzrdgrrn  10553  frec2uzrdg  10554  frecuzrdgtcl  10557  frecuzrdgg  10561  frecuzrdgfunlem  10564  frecfzennn  10571  seqeq1  10595  iseqovex  10603  seq3val  10605  seqvalcd  10606  seq3-1  10607  seqf  10609  seq3p1  10610  seqovcd  10612  seqp1cd  10615  seq3clss  10616  seq3fveq2  10620  seqfveq2g  10622  seqfveqg  10623  seq3fveq  10624  seq3feq  10625  seq3shft2  10626  seqshft2g  10627  monoord  10630  monoord2  10631  ser3mono  10632  seq3split  10633  seqsplitg  10634  seq3caopr3  10636  seqcaopr3g  10637  seq3caopr2  10638  seqcaopr2g  10639  iseqf1olemkle  10642  iseqf1olemklt  10643  iseqf1olemqval  10645  iseqf1olemqk  10652  iseqf1olemjpcl  10653  iseqf1olemqpcl  10654  iseqf1olemfvp  10655  seq3f1olemqsumkj  10656  seq3f1olemqsum  10658  seq3f1olemstep  10659  seq3f1olemp  10660  seq3f1oleml  10661  seq3f1o  10662  seqf1oglem2a  10663  seqf1og  10666  seq3id2  10671  seq3homo  10672  seq3z  10673  seqhomog  10675  seqfeq4g  10676  ser3ge0  10681  ser3le  10682  exp3vallem  10685  exp3val  10686  facp1  10875  faccl  10880  facdiv  10883  facwordi  10885  faclbnd  10886  facubnd  10890  bcval  10894  bcval5  10908  fz1eqb  10935  omgadd  10947  hashxp  10971  zfz1isolem1  10985  zfz1iso  10986  seq3coll  10987  eqwrd  11034  lswwrd  11040  ccatfvalfi  11048  ccatval1  11053  ccatval2  11054  s1eq  11073  eqs1  11082  swrdval  11101  seq3shft  11149  reval  11160  replim  11170  cj11  11216  caucvgre  11292  cvg1nlemcau  11295  cvg1nlemres  11296  rexuz3  11301  absval  11312  resqrexlemover  11321  resqrexlemdecn  11323  resqrexlemlo  11324  resqrexlemcalc3  11327  resqrexlemnm  11329  resqrexlemcvg  11330  resqrexlemoverl  11332  resqrexlemglsq  11333  resqrexlemga  11334  resqrexlemsqa  11335  resqrexlemex  11336  abs00bd  11377  cau3lem  11425  caubnd2  11428  climconst  11601  climmpt  11611  climshftlemg  11613  climcn1  11619  climle  11645  climub  11655  climserle  11656  climcau  11658  climcvg1nlem  11660  climcvg1n  11661  serf0  11663  fsum3cvg  11689  summodclem3  11691  summodclem2a  11692  summodclem2  11693  summodc  11694  zsumdc  11695  fsum3  11698  fsumf1o  11701  fisumss  11703  fsum3cvg2  11705  fsum3ser  11708  fsumcl2lem  11709  fsumadd  11717  sumsnf  11720  isummulc2  11737  isumge0  11741  isumadd  11742  fsum2dlemstep  11745  fsummulc2  11759  fsumconst  11765  fsumrelem  11782  isumshft  11801  isum1p  11803  isumnn0nn  11804  isumrpcl  11805  isumlessdc  11807  cvgratnnlemnexp  11835  cvgratnnlemmn  11836  cvgratnnlemseq  11837  cvgratnnlemabsle  11838  cvgratnnlemfm  11840  cvgratnnlemrate  11841  cvgratnn  11842  cvgratz  11843  mertenslemi1  11846  mertenslem2  11847  mertensabs  11848  clim2prod  11850  prodfap0  11856  prodfrecap  11857  prodfdivap  11858  fproddccvg  11883  prodmodclem3  11886  prodmodclem2a  11887  prodmodclem2  11888  prodmodc  11889  zproddc  11890  fprodseq  11894  fprodf1o  11899  fprodssdc  11901  fprodmul  11902  prodsnf  11903  fprodfac  11926  fprodconst  11931  fprod2dlemstep  11933  eftvalcn  11968  ef0lem  11971  ege2le3  11982  efcj  11984  efaddlem  11985  eftlub  12001  efgt1p2  12006  reef11  12010  tanvalap  12019  efieq1re  12083  eirraplem  12088  dvdsabseq  12158  dvdsfac  12171  gcd0id  12300  nninfctlemfo  12361  nn0seqcvgd  12363  alginv  12369  algcvg  12370  algcvga  12373  algfx  12374  eucalglt  12379  lcmid  12402  qredeu  12419  prmfac1  12474  sqne2sq  12499  qnumdenbi  12514  dfphi2  12542  eulerthlemrprm  12551  eulerthlema  12552  eulerthlemh  12553  eulerthlemth  12554  phisum  12563  pcmpt  12666  pcfac  12673  1arithlem4  12689  elgz  12694  4sqlem4  12715  4sqlem12  12725  2expltfac  12762  ennnfonelemk  12771  ennnfonelemp1  12777  ennnfoneleminc  12782  ennnfonelemkh  12783  ennnfonelemhf1o  12784  ennnfonelemex  12785  ennnfonelemhom  12786  ennnfonelemrn  12790  ennnfonelemnn0  12793  ennnfonelemr  12794  ennnfonelemim  12795  ctinfomlemom  12798  ctinfom  12799  ctiunctlemfo  12810  nninfdclemlt  12822  nninfdclemf1  12823  sloteq  12837  ressvalsets  12896  topnvalg  13083  prdsbasprj  13114  prdsplusgfval  13116  prdsmulrfval  13118  imasex  13137  imasaddvallemg  13147  qusex  13157  xpsfrnel  13176  xpsfeq  13177  xpsval  13184  ismgm  13189  plusffvalg  13194  grpidvalg  13205  gsumfzval  13223  gsumval2  13229  issgrp  13235  ismnddef  13250  prdsidlem  13279  pws0g  13283  ismhm  13293  mhmex  13294  mhmlin  13299  issubm  13304  mhmeql  13324  isgrp  13338  grpn0  13367  grpinvfvalg  13374  grpsubfvalg  13377  grpsubval  13378  grpinv11  13401  grpinvnz  13403  prdsinvlem  13440  pwsinvg  13444  pwssub  13445  mhmlem  13450  mulgfvalg  13457  mulgsubcl  13472  mulgaddcomlem  13481  mulgneg2  13492  mulgass  13495  issubg  13509  subgex  13512  issubg2m  13525  issubg4m  13529  0subg  13535  isnsg  13538  releqgg  13556  eqgex  13557  eqgval  13559  isghm  13579  ghmlin  13584  ghmrn  13593  ghmeql  13603  f1ghm0to0  13608  iscmn  13629  mgpvalg  13685  isrng  13696  issrg  13727  srgfcl  13735  isring  13762  iscrng  13765  mulgass2  13820  opprvalg  13831  reldvdsrsrg  13854  dvdsrvald  13855  isunitd  13868  invrfvald  13884  dvrfvald  13895  dvrvald  13896  isrhm  13920  rhmval  13935  isnzr  13943  islring  13954  issubrng  13961  issubrg  13983  rrgval  14024  isdomn  14031  aprval  14044  aprap  14048  islmod  14053  scaffvalg  14068  lsssetm  14118  lspfval  14150  sraval  14199  rlmvalg  14216  2idlval  14264  2idlvalg  14265  cnfldmulg  14338  zlmval  14389  znf1o  14413  psrlinv  14446  mplsubgfilemcl  14461  istps  14504  clsfval  14573  cnpval  14670  lmconst  14688  txcnp  14743  upxp  14744  uptx  14746  txlm  14751  lmcn2  14752  cnmpt11  14755  cnmpt11f  14756  cnmpt1t  14757  cnmpt21  14763  cnmpt21f  14764  cnmpt2t  14765  mopnval  14914  isxms  14923  isms  14925  comet  14971  mopnex  14977  xmetxp  14979  xmetxpbl  14980  txmetcnp  14990  txmetcn  14991  qtopbasss  14993  cncfi  15050  cncfmpt1f  15070  ivthinclemlm  15106  ivthinclemum  15107  ivthinclemlopn  15108  ivthinclemlr  15109  ivthinclemuopn  15110  ivthinclemur  15111  ivthinclemdisj  15112  ivthinclemloc  15113  ivthinc  15115  ivthdec  15116  ivthreinc  15117  cnlimci  15145  limccnpcntop  15147  eldvap  15154  dvcoapbr  15179  dvcj  15181  dvfre  15182  dvmptcjx  15196  dveflem  15198  elply2  15207  elplyd  15213  plymullem1  15220  plyadd  15223  plymul  15224  plycoeid3  15229  plycolemc  15230  plyco  15231  plycjlemc  15232  plycj  15233  dvply1  15237  sin0pilem2  15254  pilem3  15255  coseq0q4123  15306  coseq0negpitopi  15308  cos11  15325  logltb  15346  rpcxpef  15366  rplogbval  15417  mpodvdsmulf1o  15462  fsumdvdsmul  15463  zabsle1  15476  lgslem2  15478  lgslem3  15479  lgsfcl2  15483  lgsfle1  15486  lgsle1  15492  lgsdirprm  15511  lgseisenlem2  15548  lgsquadlem2  15555  2sqlem1  15591  2sqlem2  15592  mul2sq  15593  2sqlem3  15594  2sqlem9  15601  2sqlem10  15602  vtxvalg  15615  iedgvalg  15616  edgopval  15654  edgstruct  15656  012of  15930  2o01f  15931  subctctexmid  15937  nnsf  15942  nninfalllem1  15945  nninffeq  15957  qdencn  15966  trilpolemclim  15975  trilpolemcl  15976  trilpolemisumle  15977  trilpolemeq1  15979  trilpolemlt1  15980  trilpo  15982  iswomni0  15990  redcwlpo  15994  dceqnconst  15999  dcapnconst  16000  nconstwlpolemgt0  16003  nconstwlpolem  16004  nconstwlpo  16005  neapmkv  16007