Theorem fveq2 5496

Description: Equality theorem for function value. (Contributed by NM, 29-Dec-1996.)

Assertion

Ref	Expression
fveq2	|- ( A = B -> ( F ` A ) = ( F ` B ) )

Proof of Theorem fveq2

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq1 3992	. . 3 |- ( A = B -> ( A F x <-> B F x ) )
2	1	iotabidv 5181	. 2 |- ( A = B -> ( iota x A F x ) = ( iota x B F x ) )
3		df-fv 5206	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5206	. 2 |- ( F ` B ) = ( iota x B F x )
5	2, 3, 4	3eqtr4g 2228	1 |- ( A = B -> ( F ` A ) = ( F ` B ) )

Syntax hints:   -> wi 4   = wceq 1348   class class class wbr 3989   iotacio 5158   ` cfv 5198

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rex 2454  df-v 2732  df-un 3125  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-br 3990  df-iota 5160  df-fv 5206

This theorem is referenced by:  fveq2i  5499  fveq2d  5500  2fveq3  5501  fvifdc  5518  dffn5imf  5551  fvelimab  5552  ssimaex  5557  fvco4  5568  fvmptssdm  5580  fvmptf  5588  eqfnfv2f  5597  fvelrn  5627  ralrnmpt  5638  rexrnmpt  5639  ffnfvf  5655  fmptco  5662  cofmpt  5665  fcompt  5666  fcoconst  5667  fnressn  5682  fressnfv  5683  fconstfvm  5714  foco2  5733  funiunfvdmf  5743  f1veqaeq  5748  dff13f  5749  f1fveq  5751  f1elima  5752  f1ocnvfv  5758  f1ocnvfvb  5759  fcofo  5763  cocan2  5767  fliftfun  5775  isorel  5787  isocnv  5790  isotr  5795  f1oiso2  5806  canth  5807  imbrov2fvoveq  5878  ffnov  5957  eqfnov  5959  fnovim  5961  fnrnov  5998  foov  5999  funimassov  6002  ovelimab  6003  suppssfv  6057  ofvalg  6070  ofrval  6071  offval2  6076  ofrfval2  6077  ofco  6079  caofinvl  6083  op1std  6127  op2ndd  6128  1stval2  6134  2ndval2  6135  unielxp  6153  reldm  6165  oprabco  6196  2ndconst  6201  f1o2ndf1  6207  mpoxopn0yelv  6218  mpoxopoveq  6219  smoel  6279  tfrlem1  6287  tfrlem3-2d  6291  tfrlem5  6293  tfrlem9  6298  tfr0dm  6301  tfrlemiubacc  6309  tfrlemi1  6311  tfrexlem  6313  tfr1onlemsucfn  6319  tfr1onlemsucaccv  6320  tfr1onlembxssdm  6322  tfr1onlembfn  6323  tfr1onlemubacc  6325  tfr1onlemaccex  6327  tfr1onlemres  6328  tfri1dALT  6330  tfrcllemsucfn  6332  tfrcllemsucaccv  6333  tfrcllembxssdm  6335  tfrcllembfn  6336  tfrcllemubacc  6338  tfrcllemaccex  6340  tfrcllemres  6341  tfrcldm  6342  tfrcl  6343  tfri3  6346  rdgtfr  6353  rdgss  6362  rdgisuc1  6363  rdgisucinc  6364  rdgon  6365  frecabex  6377  frecabcl  6378  frecfcllem  6383  frecsuclem  6385  frecsuc  6386  frecrdg  6387  oav  6433  omv  6434  oeiv  6435  fvixp  6681  cbvixp  6693  mptelixpg  6712  elixpsn  6713  dom2lem  6750  xpcomco  6804  xpmapen  6828  fidceq  6847  fieq0  6953  ordiso2  7012  djune  7055  updjudhcoinlf  7057  updjudhcoinrg  7058  updjud  7059  omp1eom  7072  0ct  7084  ctmlemr  7085  ctssdclemn0  7087  ctssdccl  7088  ctssdc  7090  enumctlemm  7091  nnnninfeq  7104  nnnninfeq2  7105  enomnilem  7114  finomni  7116  fodjuomnilemdc  7120  fodju0  7123  fodjuomni  7125  ismkvnex  7131  fodjumkv  7136  nninfwlporlemd  7148  nninfwlpor  7150  exmidaclem  7185  cc1  7227  cc2lem  7228  cc2  7229  cc3  7230  mulpipq2  7333  genipv  7471  genpelxp  7473  addcanprleml  7576  addcanprlemu  7577  recexprlemm  7586  recexprlemdisj  7592  recexprlemloc  7593  recexprlem1ssl  7595  recexprlem1ssu  7596  cauappcvgprlemm  7607  cauappcvgprlemdisj  7613  cauappcvgprlemloc  7614  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  cauappcvgprlem1  7621  cauappcvgprlem2  7622  cauappcvgprlemlim  7623  cauappcvgpr  7624  caucvgprlemnkj  7628  caucvgprlemnbj  7629  caucvgprlemm  7630  caucvgprlemdisj  7636  caucvgprlemloc  7637  caucvgprlemcl  7638  caucvgprlemladdfu  7639  caucvgprlemladdrl  7640  caucvgprlem1  7641  caucvgprlem2  7642  caucvgpr  7644  caucvgprprlemell  7647  caucvgprprlemelu  7648  caucvgprprlemcbv  7649  caucvgprprlemval  7650  caucvgprprlemnkeqj  7652  caucvgprprlemnbj  7655  caucvgprprlemml  7656  caucvgprprlemmu  7657  caucvgprprlemopl  7659  caucvgprprlemlol  7660  caucvgprprlemopu  7661  caucvgprprlemloc  7665  caucvgprprlemclphr  7667  caucvgprprlemexbt  7668  caucvgprprlem1  7671  caucvgprprlem2  7672  caucvgsrlemcl  7751  caucvgsrlemfv  7753  caucvgsrlembound  7756  caucvgsrlemgt1  7757  caucvgsrlemoffval  7758  caucvgsrlemoffres  7762  caucvgsrlembnd  7763  caucvgsr  7764  axcaucvglemcau  7860  axcaucvglemres  7861  uz11  9509  cnref1o  9609  fzprval  10038  fztpval  10039  frec2uzuzd  10358  frec2uzltd  10359  frec2uzlt2d  10360  frecuzrdgrrn  10364  frec2uzrdg  10365  frecuzrdgtcl  10368  frecuzrdgg  10372  frecuzrdgfunlem  10375  frecfzennn  10382  seqeq1  10404  iseqovex  10412  seq3val  10414  seqvalcd  10415  seq3-1  10416  seqf  10417  seq3p1  10418  seqovcd  10419  seqp1cd  10422  seq3clss  10423  seq3fveq2  10425  seq3fveq  10427  seq3feq  10428  seq3shft2  10429  monoord  10432  monoord2  10433  ser3mono  10434  seq3split  10435  seq3caopr3  10437  seq3caopr2  10438  iseqf1olemkle  10440  iseqf1olemklt  10441  iseqf1olemqval  10443  iseqf1olemqk  10450  iseqf1olemjpcl  10451  iseqf1olemqpcl  10452  iseqf1olemfvp  10453  seq3f1olemqsumkj  10454  seq3f1olemqsum  10456  seq3f1olemstep  10457  seq3f1olemp  10458  seq3f1oleml  10459  seq3f1o  10460  seq3id2  10465  seq3homo  10466  seq3z  10467  ser3ge0  10473  ser3le  10474  exp3vallem  10477  exp3val  10478  facp1  10664  faccl  10669  facdiv  10672  facwordi  10674  faclbnd  10675  facubnd  10679  bcval  10683  bcval5  10697  fz1eqb  10725  omgadd  10737  hashxp  10761  zfz1isolem1  10775  zfz1iso  10776  seq3coll  10777  seq3shft  10802  reval  10813  replim  10823  cj11  10869  caucvgre  10945  cvg1nlemcau  10948  cvg1nlemres  10949  rexuz3  10954  absval  10965  resqrexlemover  10974  resqrexlemdecn  10976  resqrexlemlo  10977  resqrexlemcalc3  10980  resqrexlemnm  10982  resqrexlemcvg  10983  resqrexlemoverl  10985  resqrexlemglsq  10986  resqrexlemga  10987  resqrexlemsqa  10988  resqrexlemex  10989  abs00bd  11030  cau3lem  11078  caubnd2  11081  climconst  11253  climmpt  11263  climshftlemg  11265  climcn1  11271  climle  11297  climub  11307  climserle  11308  climcau  11310  climcvg1nlem  11312  climcvg1n  11313  serf0  11315  fsum3cvg  11341  summodclem3  11343  summodclem2a  11344  summodclem2  11345  summodc  11346  zsumdc  11347  fsum3  11350  fsumf1o  11353  fisumss  11355  fsum3cvg2  11357  fsum3ser  11360  fsumcl2lem  11361  fsumadd  11369  sumsnf  11372  isummulc2  11389  isumge0  11393  isumadd  11394  fsum2dlemstep  11397  fsummulc2  11411  fsumconst  11417  fsumrelem  11434  isumshft  11453  isum1p  11455  isumnn0nn  11456  isumrpcl  11457  isumlessdc  11459  cvgratnnlemnexp  11487  cvgratnnlemmn  11488  cvgratnnlemseq  11489  cvgratnnlemabsle  11490  cvgratnnlemfm  11492  cvgratnnlemrate  11493  cvgratnn  11494  cvgratz  11495  mertenslemi1  11498  mertenslem2  11499  mertensabs  11500  clim2prod  11502  prodfap0  11508  prodfrecap  11509  prodfdivap  11510  fproddccvg  11535  prodmodclem3  11538  prodmodclem2a  11539  prodmodclem2  11540  prodmodc  11541  zproddc  11542  fprodseq  11546  fprodf1o  11551  fprodssdc  11553  fprodmul  11554  prodsnf  11555  fprodfac  11578  fprodconst  11583  fprod2dlemstep  11585  eftvalcn  11620  ef0lem  11623  ege2le3  11634  efcj  11636  efaddlem  11637  eftlub  11653  efgt1p2  11658  reef11  11662  tanvalap  11671  efieq1re  11734  eirraplem  11739  dvdsabseq  11807  dvdsfac  11820  zsupcllemex  11901  infssuzex  11904  suprzubdc  11907  gcd0id  11934  nn0seqcvgd  11995  alginv  12001  algcvg  12002  algcvga  12005  algfx  12006  eucalglt  12011  lcmid  12034  qredeu  12051  prmfac1  12106  sqne2sq  12131  qnumdenbi  12146  dfphi2  12174  eulerthlemrprm  12183  eulerthlema  12184  eulerthlemh  12185  eulerthlemth  12186  phisum  12194  pcmpt  12295  pcfac  12302  1arithlem4  12318  elgz  12323  4sqlem4  12344  ennnfonelemk  12355  ennnfonelemp1  12361  ennnfoneleminc  12366  ennnfonelemkh  12367  ennnfonelemhf1o  12368  ennnfonelemex  12369  ennnfonelemhom  12370  ennnfonelemrn  12374  ennnfonelemnn0  12377  ennnfonelemr  12378  ennnfonelemim  12379  ctinfomlemom  12382  ctinfom  12383  ctiunctlemfo  12394  nninfdclemlt  12406  nninfdclemf1  12407  sloteq  12421  topnvalg  12591  ismgm  12611  plusffvalg  12616  grpidvalg  12627  issgrp  12644  ismnddef  12654  ismhm  12685  mhmlin  12690  issubm  12695  mhmeql  12707  isgrp  12714  grpn0  12738  grpinvfvalg  12745  grpsubfvalg  12748  grpsubval  12749  grpinv11  12768  grpinvnz  12770  istps  12824  clsfval  12895  cnpval  12992  lmconst  13010  txcnp  13065  upxp  13066  uptx  13068  txlm  13073  lmcn2  13074  cnmpt11  13077  cnmpt11f  13078  cnmpt1t  13079  cnmpt21  13085  cnmpt21f  13086  cnmpt2t  13087  mopnval  13236  isxms  13245  isms  13247  comet  13293  mopnex  13299  xmetxp  13301  xmetxpbl  13302  txmetcnp  13312  txmetcn  13313  qtopbasss  13315  cncfi  13359  cncfmpt1f  13378  ivthinclemlm  13406  ivthinclemum  13407  ivthinclemlopn  13408  ivthinclemlr  13409  ivthinclemuopn  13410  ivthinclemur  13411  ivthinclemdisj  13412  ivthinclemloc  13413  ivthinc  13415  ivthdec  13416  cnlimci  13436  limccnpcntop  13438  eldvap  13445  dvcoapbr  13465  dvcj  13467  dvfre  13468  dvmptcjx  13480  dveflem  13481  sin0pilem2  13497  pilem3  13498  coseq0q4123  13549  coseq0negpitopi  13551  cos11  13568  logltb  13589  rpcxpef  13609  rplogbval  13657  zabsle1  13694  lgslem2  13696  lgslem3  13697  lgsfcl2  13701  lgsfle1  13704  lgsle1  13710  lgsdirprm  13729  2sqlem1  13744  2sqlem2  13745  mul2sq  13746  2sqlem3  13747  2sqlem9  13754  2sqlem10  13755  012of  14028  2o01f  14029  subctctexmid  14034  nnsf  14038  nninfalllem1  14041  nninffeq  14053  qdencn  14059  trilpolemclim  14068  trilpolemcl  14069  trilpolemisumle  14070  trilpolemeq1  14072  trilpolemlt1  14073  trilpo  14075  iswomni0  14083  redcwlpo  14087  dceqnconst  14091  dcapnconst  14092  nconstwlpolemgt0  14095  nconstwlpolem  14096  nconstwlpo  14097  neapmkv  14099