Theorem fveq2 5486

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 3985	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝑥 ↔ 𝐵𝐹𝑥))
2	1	iotabidv 5174	. 2 ⊢ (𝐴 = 𝐵 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐵𝐹𝑥))
3		df-fv 5196	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5196	. 2 ⊢ (𝐹‘𝐵) = (℩𝑥𝐵𝐹𝑥)
5	2, 3, 4	3eqtr4g 2224	1 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))

Syntax hints:   → wi 4   = wceq 1343   class class class wbr 3982  ℩cio 5151  ‘cfv 5188

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-rex 2450  df-v 2728  df-un 3120  df-sn 3582  df-pr 3583  df-op 3585  df-uni 3790  df-br 3983  df-iota 5153  df-fv 5196

This theorem is referenced by:  fveq2i  5489  fveq2d  5490  2fveq3  5491  fvifdc  5508  dffn5imf  5541  fvelimab  5542  ssimaex  5547  fvco4  5558  fvmptssdm  5570  fvmptf  5578  eqfnfv2f  5587  fvelrn  5616  ralrnmpt  5627  rexrnmpt  5628  ffnfvf  5644  fmptco  5651  cofmpt  5654  fcompt  5655  fcoconst  5656  fnressn  5671  fressnfv  5672  fconstfvm  5703  foco2  5722  funiunfvdmf  5732  f1veqaeq  5737  dff13f  5738  f1fveq  5740  f1elima  5741  f1ocnvfv  5747  f1ocnvfvb  5748  fcofo  5752  cocan2  5756  fliftfun  5764  isorel  5776  isocnv  5779  isotr  5784  f1oiso2  5795  canth  5796  imbrov2fvoveq  5867  ffnov  5946  eqfnov  5948  fnovim  5950  fnrnov  5987  foov  5988  funimassov  5991  ovelimab  5992  suppssfv  6046  ofvalg  6059  ofrval  6060  offval2  6065  ofrfval2  6066  ofco  6068  caofinvl  6072  op1std  6116  op2ndd  6117  1stval2  6123  2ndval2  6124  unielxp  6142  reldm  6154  oprabco  6185  2ndconst  6190  f1o2ndf1  6196  mpoxopn0yelv  6207  mpoxopoveq  6208  smoel  6268  tfrlem1  6276  tfrlem3-2d  6280  tfrlem5  6282  tfrlem9  6287  tfr0dm  6290  tfrlemiubacc  6298  tfrlemi1  6300  tfrexlem  6302  tfr1onlemsucfn  6308  tfr1onlemsucaccv  6309  tfr1onlembxssdm  6311  tfr1onlembfn  6312  tfr1onlemubacc  6314  tfr1onlemaccex  6316  tfr1onlemres  6317  tfri1dALT  6319  tfrcllemsucfn  6321  tfrcllemsucaccv  6322  tfrcllembxssdm  6324  tfrcllembfn  6325  tfrcllemubacc  6327  tfrcllemaccex  6329  tfrcllemres  6330  tfrcldm  6331  tfrcl  6332  tfri3  6335  rdgtfr  6342  rdgss  6351  rdgisuc1  6352  rdgisucinc  6353  rdgon  6354  frecabex  6366  frecabcl  6367  frecfcllem  6372  frecsuclem  6374  frecsuc  6375  frecrdg  6376  oav  6422  omv  6423  oeiv  6424  fvixp  6669  cbvixp  6681  mptelixpg  6700  elixpsn  6701  dom2lem  6738  xpcomco  6792  xpmapen  6816  fidceq  6835  fieq0  6941  ordiso2  7000  djune  7043  updjudhcoinlf  7045  updjudhcoinrg  7046  updjud  7047  omp1eom  7060  0ct  7072  ctmlemr  7073  ctssdclemn0  7075  ctssdccl  7076  ctssdc  7078  enumctlemm  7079  nnnninfeq  7092  nnnninfeq2  7093  enomnilem  7102  finomni  7104  fodjuomnilemdc  7108  fodju0  7111  fodjuomni  7113  ismkvnex  7119  fodjumkv  7124  exmidaclem  7164  cc1  7206  cc2lem  7207  cc2  7208  cc3  7209  mulpipq2  7312  genipv  7450  genpelxp  7452  addcanprleml  7555  addcanprlemu  7556  recexprlemm  7565  recexprlemdisj  7571  recexprlemloc  7572  recexprlem1ssl  7574  recexprlem1ssu  7575  cauappcvgprlemm  7586  cauappcvgprlemdisj  7592  cauappcvgprlemloc  7593  cauappcvgprlemladdru  7597  cauappcvgprlemladdrl  7598  cauappcvgprlem1  7600  cauappcvgprlem2  7601  cauappcvgprlemlim  7602  cauappcvgpr  7603  caucvgprlemnkj  7607  caucvgprlemnbj  7608  caucvgprlemm  7609  caucvgprlemdisj  7615  caucvgprlemloc  7616  caucvgprlemcl  7617  caucvgprlemladdfu  7618  caucvgprlemladdrl  7619  caucvgprlem1  7620  caucvgprlem2  7621  caucvgpr  7623  caucvgprprlemell  7626  caucvgprprlemelu  7627  caucvgprprlemcbv  7628  caucvgprprlemval  7629  caucvgprprlemnkeqj  7631  caucvgprprlemnbj  7634  caucvgprprlemml  7635  caucvgprprlemmu  7636  caucvgprprlemopl  7638  caucvgprprlemlol  7639  caucvgprprlemopu  7640  caucvgprprlemloc  7644  caucvgprprlemclphr  7646  caucvgprprlemexbt  7647  caucvgprprlem1  7650  caucvgprprlem2  7651  caucvgsrlemcl  7730  caucvgsrlemfv  7732  caucvgsrlembound  7735  caucvgsrlemgt1  7736  caucvgsrlemoffval  7737  caucvgsrlemoffres  7741  caucvgsrlembnd  7742  caucvgsr  7743  axcaucvglemcau  7839  axcaucvglemres  7840  uz11  9488  cnref1o  9588  fzprval  10017  fztpval  10018  frec2uzuzd  10337  frec2uzltd  10338  frec2uzlt2d  10339  frecuzrdgrrn  10343  frec2uzrdg  10344  frecuzrdgtcl  10347  frecuzrdgg  10351  frecuzrdgfunlem  10354  frecfzennn  10361  seqeq1  10383  iseqovex  10391  seq3val  10393  seqvalcd  10394  seq3-1  10395  seqf  10396  seq3p1  10397  seqovcd  10398  seqp1cd  10401  seq3clss  10402  seq3fveq2  10404  seq3fveq  10406  seq3feq  10407  seq3shft2  10408  monoord  10411  monoord2  10412  ser3mono  10413  seq3split  10414  seq3caopr3  10416  seq3caopr2  10417  iseqf1olemkle  10419  iseqf1olemklt  10420  iseqf1olemqval  10422  iseqf1olemqk  10429  iseqf1olemjpcl  10430  iseqf1olemqpcl  10431  iseqf1olemfvp  10432  seq3f1olemqsumkj  10433  seq3f1olemqsum  10435  seq3f1olemstep  10436  seq3f1olemp  10437  seq3f1oleml  10438  seq3f1o  10439  seq3id2  10444  seq3homo  10445  seq3z  10446  ser3ge0  10452  ser3le  10453  exp3vallem  10456  exp3val  10457  facp1  10643  faccl  10648  facdiv  10651  facwordi  10653  faclbnd  10654  facubnd  10658  bcval  10662  bcval5  10676  fz1eqb  10704  omgadd  10715  hashxp  10739  zfz1isolem1  10753  zfz1iso  10754  seq3coll  10755  seq3shft  10780  reval  10791  replim  10801  cj11  10847  caucvgre  10923  cvg1nlemcau  10926  cvg1nlemres  10927  rexuz3  10932  absval  10943  resqrexlemover  10952  resqrexlemdecn  10954  resqrexlemlo  10955  resqrexlemcalc3  10958  resqrexlemnm  10960  resqrexlemcvg  10961  resqrexlemoverl  10963  resqrexlemglsq  10964  resqrexlemga  10965  resqrexlemsqa  10966  resqrexlemex  10967  abs00bd  11008  cau3lem  11056  caubnd2  11059  climconst  11231  climmpt  11241  climshftlemg  11243  climcn1  11249  climle  11275  climub  11285  climserle  11286  climcau  11288  climcvg1nlem  11290  climcvg1n  11291  serf0  11293  fsum3cvg  11319  summodclem3  11321  summodclem2a  11322  summodclem2  11323  summodc  11324  zsumdc  11325  fsum3  11328  fsumf1o  11331  fisumss  11333  fsum3cvg2  11335  fsum3ser  11338  fsumcl2lem  11339  fsumadd  11347  sumsnf  11350  isummulc2  11367  isumge0  11371  isumadd  11372  fsum2dlemstep  11375  fsummulc2  11389  fsumconst  11395  fsumrelem  11412  isumshft  11431  isum1p  11433  isumnn0nn  11434  isumrpcl  11435  isumlessdc  11437  cvgratnnlemnexp  11465  cvgratnnlemmn  11466  cvgratnnlemseq  11467  cvgratnnlemabsle  11468  cvgratnnlemfm  11470  cvgratnnlemrate  11471  cvgratnn  11472  cvgratz  11473  mertenslemi1  11476  mertenslem2  11477  mertensabs  11478  clim2prod  11480  prodfap0  11486  prodfrecap  11487  prodfdivap  11488  fproddccvg  11513  prodmodclem3  11516  prodmodclem2a  11517  prodmodclem2  11518  prodmodc  11519  zproddc  11520  fprodseq  11524  fprodf1o  11529  fprodssdc  11531  fprodmul  11532  prodsnf  11533  fprodfac  11556  fprodconst  11561  fprod2dlemstep  11563  eftvalcn  11598  ef0lem  11601  ege2le3  11612  efcj  11614  efaddlem  11615  eftlub  11631  efgt1p2  11636  reef11  11640  tanvalap  11649  efieq1re  11712  eirraplem  11717  dvdsabseq  11785  dvdsfac  11798  zsupcllemex  11879  infssuzex  11882  suprzubdc  11885  gcd0id  11912  nn0seqcvgd  11973  alginv  11979  algcvg  11980  algcvga  11983  algfx  11984  eucalglt  11989  lcmid  12012  qredeu  12029  prmfac1  12084  sqne2sq  12109  qnumdenbi  12124  dfphi2  12152  eulerthlemrprm  12161  eulerthlema  12162  eulerthlemh  12163  eulerthlemth  12164  phisum  12172  pcmpt  12273  pcfac  12280  1arithlem4  12296  elgz  12301  4sqlem4  12322  ennnfonelemk  12333  ennnfonelemp1  12339  ennnfoneleminc  12344  ennnfonelemkh  12345  ennnfonelemhf1o  12346  ennnfonelemex  12347  ennnfonelemhom  12348  ennnfonelemrn  12352  ennnfonelemnn0  12355  ennnfonelemr  12356  ennnfonelemim  12357  ctinfomlemom  12360  ctinfom  12361  ctiunctlemfo  12372  nninfdclemlt  12384  nninfdclemf1  12385  sloteq  12399  topnvalg  12568  ismgm  12588  plusffvalg  12593  grpidvalg  12604  istps  12670  clsfval  12741  cnpval  12838  lmconst  12856  txcnp  12911  upxp  12912  uptx  12914  txlm  12919  lmcn2  12920  cnmpt11  12923  cnmpt11f  12924  cnmpt1t  12925  cnmpt21  12931  cnmpt21f  12932  cnmpt2t  12933  mopnval  13082  isxms  13091  isms  13093  comet  13139  mopnex  13145  xmetxp  13147  xmetxpbl  13148  txmetcnp  13158  txmetcn  13159  qtopbasss  13161  cncfi  13205  cncfmpt1f  13224  ivthinclemlm  13252  ivthinclemum  13253  ivthinclemlopn  13254  ivthinclemlr  13255  ivthinclemuopn  13256  ivthinclemur  13257  ivthinclemdisj  13258  ivthinclemloc  13259  ivthinc  13261  ivthdec  13262  cnlimci  13282  limccnpcntop  13284  eldvap  13291  dvcoapbr  13311  dvcj  13313  dvfre  13314  dvmptcjx  13326  dveflem  13327  sin0pilem2  13343  pilem3  13344  coseq0q4123  13395  coseq0negpitopi  13397  cos11  13414  logltb  13435  rpcxpef  13455  rplogbval  13503  zabsle1  13540  lgslem2  13542  lgslem3  13543  lgsfcl2  13547  lgsfle1  13550  lgsle1  13556  lgsdirprm  13575  2sqlem1  13590  2sqlem2  13591  mul2sq  13592  2sqlem3  13593  2sqlem9  13600  2sqlem10  13601  012of  13875  2o01f  13876  subctctexmid  13881  nnsf  13885  nninfalllem1  13888  nninffeq  13900  qdencn  13906  trilpolemclim  13915  trilpolemcl  13916  trilpolemisumle  13917  trilpolemeq1  13919  trilpolemlt1  13920  trilpo  13922  iswomni0  13930  redcwlpo  13934  dceqnconst  13938  dcapnconst  13939  nconstwlpolemgt0  13942  nconstwlpolem  13943  nconstwlpo  13944  neapmkv  13946