Theorem fveq2 5480

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 3979	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝑥 ↔ 𝐵𝐹𝑥))
2	1	iotabidv 5168	. 2 ⊢ (𝐴 = 𝐵 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐵𝐹𝑥))
3		df-fv 5190	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5190	. 2 ⊢ (𝐹‘𝐵) = (℩𝑥𝐵𝐹𝑥)
5	2, 3, 4	3eqtr4g 2222	1 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))

Syntax hints:   → wi 4   = wceq 1342   class class class wbr 3976  ℩cio 5145  ‘cfv 5182

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 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-rex 2448  df-v 2723  df-un 3115  df-sn 3576  df-pr 3577  df-op 3579  df-uni 3784  df-br 3977  df-iota 5147  df-fv 5190

This theorem is referenced by:  fveq2i  5483  fveq2d  5484  2fveq3  5485  fvifdc  5502  dffn5imf  5535  fvelimab  5536  ssimaex  5541  fvco4  5552  fvmptssdm  5564  fvmptf  5572  eqfnfv2f  5581  fvelrn  5610  ralrnmpt  5621  rexrnmpt  5622  ffnfvf  5638  fmptco  5645  cofmpt  5648  fcompt  5649  fcoconst  5650  fnressn  5665  fressnfv  5666  fconstfvm  5697  foco2  5716  funiunfvdmf  5726  f1veqaeq  5731  dff13f  5732  f1fveq  5734  f1elima  5735  f1ocnvfv  5741  f1ocnvfvb  5742  fcofo  5746  cocan2  5750  fliftfun  5758  isorel  5770  isocnv  5773  isotr  5778  f1oiso2  5789  canth  5790  imbrov2fvoveq  5861  ffnov  5937  eqfnov  5939  fnovim  5941  fnrnov  5978  foov  5979  funimassov  5982  ovelimab  5983  suppssfv  6040  ofvalg  6053  ofrval  6054  offval2  6059  ofrfval2  6060  ofco  6062  caofinvl  6066  op1std  6108  op2ndd  6109  1stval2  6115  2ndval2  6116  unielxp  6134  reldm  6146  oprabco  6176  2ndconst  6181  f1o2ndf1  6187  mpoxopn0yelv  6198  mpoxopoveq  6199  smoel  6259  tfrlem1  6267  tfrlem3-2d  6271  tfrlem5  6273  tfrlem9  6278  tfr0dm  6281  tfrlemiubacc  6289  tfrlemi1  6291  tfrexlem  6293  tfr1onlemsucfn  6299  tfr1onlemsucaccv  6300  tfr1onlembxssdm  6302  tfr1onlembfn  6303  tfr1onlemubacc  6305  tfr1onlemaccex  6307  tfr1onlemres  6308  tfri1dALT  6310  tfrcllemsucfn  6312  tfrcllemsucaccv  6313  tfrcllembxssdm  6315  tfrcllembfn  6316  tfrcllemubacc  6318  tfrcllemaccex  6320  tfrcllemres  6321  tfrcldm  6322  tfrcl  6323  tfri3  6326  rdgtfr  6333  rdgss  6342  rdgisuc1  6343  rdgisucinc  6344  rdgon  6345  frecabex  6357  frecabcl  6358  frecfcllem  6363  frecsuclem  6365  frecsuc  6366  frecrdg  6367  oav  6413  omv  6414  oeiv  6415  fvixp  6660  cbvixp  6672  mptelixpg  6691  elixpsn  6692  dom2lem  6729  xpcomco  6783  xpmapen  6807  fidceq  6826  fieq0  6932  ordiso2  6991  djune  7034  updjudhcoinlf  7036  updjudhcoinrg  7037  updjud  7038  omp1eom  7051  0ct  7063  ctmlemr  7064  ctssdclemn0  7066  ctssdccl  7067  ctssdc  7069  enumctlemm  7070  nnnninfeq  7083  nnnninfeq2  7084  enomnilem  7093  finomni  7095  fodjuomnilemdc  7099  fodju0  7102  fodjuomni  7104  ismkvnex  7110  fodjumkv  7115  exmidaclem  7155  cc1  7197  cc2lem  7198  cc2  7199  cc3  7200  mulpipq2  7303  genipv  7441  genpelxp  7443  addcanprleml  7546  addcanprlemu  7547  recexprlemm  7556  recexprlemdisj  7562  recexprlemloc  7563  recexprlem1ssl  7565  recexprlem1ssu  7566  cauappcvgprlemm  7577  cauappcvgprlemdisj  7583  cauappcvgprlemloc  7584  cauappcvgprlemladdru  7588  cauappcvgprlemladdrl  7589  cauappcvgprlem1  7591  cauappcvgprlem2  7592  cauappcvgprlemlim  7593  cauappcvgpr  7594  caucvgprlemnkj  7598  caucvgprlemnbj  7599  caucvgprlemm  7600  caucvgprlemdisj  7606  caucvgprlemloc  7607  caucvgprlemcl  7608  caucvgprlemladdfu  7609  caucvgprlemladdrl  7610  caucvgprlem1  7611  caucvgprlem2  7612  caucvgpr  7614  caucvgprprlemell  7617  caucvgprprlemelu  7618  caucvgprprlemcbv  7619  caucvgprprlemval  7620  caucvgprprlemnkeqj  7622  caucvgprprlemnbj  7625  caucvgprprlemml  7626  caucvgprprlemmu  7627  caucvgprprlemopl  7629  caucvgprprlemlol  7630  caucvgprprlemopu  7631  caucvgprprlemloc  7635  caucvgprprlemclphr  7637  caucvgprprlemexbt  7638  caucvgprprlem1  7641  caucvgprprlem2  7642  caucvgsrlemcl  7721  caucvgsrlemfv  7723  caucvgsrlembound  7726  caucvgsrlemgt1  7727  caucvgsrlemoffval  7728  caucvgsrlemoffres  7732  caucvgsrlembnd  7733  caucvgsr  7734  axcaucvglemcau  7830  axcaucvglemres  7831  uz11  9479  cnref1o  9579  fzprval  10007  fztpval  10008  frec2uzuzd  10327  frec2uzltd  10328  frec2uzlt2d  10329  frecuzrdgrrn  10333  frec2uzrdg  10334  frecuzrdgtcl  10337  frecuzrdgg  10341  frecuzrdgfunlem  10344  frecfzennn  10351  seqeq1  10373  iseqovex  10381  seq3val  10383  seqvalcd  10384  seq3-1  10385  seqf  10386  seq3p1  10387  seqovcd  10388  seqp1cd  10391  seq3clss  10392  seq3fveq2  10394  seq3fveq  10396  seq3feq  10397  seq3shft2  10398  monoord  10401  monoord2  10402  ser3mono  10403  seq3split  10404  seq3caopr3  10406  seq3caopr2  10407  iseqf1olemkle  10409  iseqf1olemklt  10410  iseqf1olemqval  10412  iseqf1olemqk  10419  iseqf1olemjpcl  10420  iseqf1olemqpcl  10421  iseqf1olemfvp  10422  seq3f1olemqsumkj  10423  seq3f1olemqsum  10425  seq3f1olemstep  10426  seq3f1olemp  10427  seq3f1oleml  10428  seq3f1o  10429  seq3id2  10434  seq3homo  10435  seq3z  10436  ser3ge0  10442  ser3le  10443  exp3vallem  10446  exp3val  10447  facp1  10632  faccl  10637  facdiv  10640  facwordi  10642  faclbnd  10643  facubnd  10647  bcval  10651  bcval5  10665  fz1eqb  10693  omgadd  10704  hashxp  10728  zfz1isolem1  10739  zfz1iso  10740  seq3coll  10741  seq3shft  10766  reval  10777  replim  10787  cj11  10833  caucvgre  10909  cvg1nlemcau  10912  cvg1nlemres  10913  rexuz3  10918  absval  10929  resqrexlemover  10938  resqrexlemdecn  10940  resqrexlemlo  10941  resqrexlemcalc3  10944  resqrexlemnm  10946  resqrexlemcvg  10947  resqrexlemoverl  10949  resqrexlemglsq  10950  resqrexlemga  10951  resqrexlemsqa  10952  resqrexlemex  10953  abs00bd  10994  cau3lem  11042  caubnd2  11045  climconst  11217  climmpt  11227  climshftlemg  11229  climcn1  11235  climle  11261  climub  11271  climserle  11272  climcau  11274  climcvg1nlem  11276  climcvg1n  11277  serf0  11279  fsum3cvg  11305  summodclem3  11307  summodclem2a  11308  summodclem2  11309  summodc  11310  zsumdc  11311  fsum3  11314  fsumf1o  11317  fisumss  11319  fsum3cvg2  11321  fsum3ser  11324  fsumcl2lem  11325  fsumadd  11333  sumsnf  11336  isummulc2  11353  isumge0  11357  isumadd  11358  fsum2dlemstep  11361  fsummulc2  11375  fsumconst  11381  fsumrelem  11398  isumshft  11417  isum1p  11419  isumnn0nn  11420  isumrpcl  11421  isumlessdc  11423  cvgratnnlemnexp  11451  cvgratnnlemmn  11452  cvgratnnlemseq  11453  cvgratnnlemabsle  11454  cvgratnnlemfm  11456  cvgratnnlemrate  11457  cvgratnn  11458  cvgratz  11459  mertenslemi1  11462  mertenslem2  11463  mertensabs  11464  clim2prod  11466  prodfap0  11472  prodfrecap  11473  prodfdivap  11474  fproddccvg  11499  prodmodclem3  11502  prodmodclem2a  11503  prodmodclem2  11504  prodmodc  11505  zproddc  11506  fprodseq  11510  fprodf1o  11515  fprodssdc  11517  fprodmul  11518  prodsnf  11519  fprodfac  11542  fprodconst  11547  fprod2dlemstep  11549  eftvalcn  11584  ef0lem  11587  ege2le3  11598  efcj  11600  efaddlem  11601  eftlub  11617  efgt1p2  11622  reef11  11626  tanvalap  11635  efieq1re  11698  eirraplem  11703  dvdsabseq  11770  dvdsfac  11783  zsupcllemex  11864  infssuzex  11867  suprzubdc  11870  gcd0id  11897  nn0seqcvgd  11952  alginv  11958  algcvg  11959  algcvga  11962  algfx  11963  eucalglt  11968  lcmid  11991  qredeu  12008  prmfac1  12061  sqne2sq  12086  qnumdenbi  12101  dfphi2  12129  eulerthlemrprm  12138  eulerthlema  12139  eulerthlemh  12140  eulerthlemth  12141  phisum  12149  pcmpt  12250  pcfac  12257  ennnfonelemk  12270  ennnfonelemp1  12276  ennnfoneleminc  12281  ennnfonelemkh  12282  ennnfonelemhf1o  12283  ennnfonelemex  12284  ennnfonelemhom  12285  ennnfonelemrn  12289  ennnfonelemnn0  12292  ennnfonelemr  12293  ennnfonelemim  12294  ctinfomlemom  12297  ctinfom  12298  ctiunctlemfo  12309  nninfdclemlt  12323  nninfdclemf1  12324  sloteq  12336  topnvalg  12504  istps  12571  clsfval  12642  cnpval  12739  lmconst  12757  txcnp  12812  upxp  12813  uptx  12815  txlm  12820  lmcn2  12821  cnmpt11  12824  cnmpt11f  12825  cnmpt1t  12826  cnmpt21  12832  cnmpt21f  12833  cnmpt2t  12834  mopnval  12983  isxms  12992  isms  12994  comet  13040  mopnex  13046  xmetxp  13048  xmetxpbl  13049  txmetcnp  13059  txmetcn  13060  qtopbasss  13062  cncfi  13106  cncfmpt1f  13125  ivthinclemlm  13153  ivthinclemum  13154  ivthinclemlopn  13155  ivthinclemlr  13156  ivthinclemuopn  13157  ivthinclemur  13158  ivthinclemdisj  13159  ivthinclemloc  13160  ivthinc  13162  ivthdec  13163  cnlimci  13183  limccnpcntop  13185  eldvap  13192  dvcoapbr  13212  dvcj  13214  dvfre  13215  dvmptcjx  13227  dveflem  13228  sin0pilem2  13244  pilem3  13245  coseq0q4123  13296  coseq0negpitopi  13298  cos11  13315  logltb  13336  rpcxpef  13356  rplogbval  13404  012of  13709  2o01f  13710  subctctexmid  13715  nnsf  13719  nninfalllem1  13722  nninffeq  13734  qdencn  13740  trilpolemclim  13749  trilpolemcl  13750  trilpolemisumle  13751  trilpolemeq1  13753  trilpolemlt1  13754  trilpo  13756  iswomni0  13764  redcwlpo  13768  dceqnconst  13772  dcapnconst  13773  nconstwlpolemgt0  13776  nconstwlpolem  13777  nconstwlpo  13778  neapmkv  13780