Theorem fveq2 5494

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 3990	. . 3 |- ( A = B -> ( A F x <-> B F x ) )
2	1	iotabidv 5179	. 2 |- ( A = B -> ( iota x A F x ) = ( iota x B F x ) )
3		df-fv 5204	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5204	. 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 3987   iotacio 5156   ` cfv 5196

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 3587  df-pr 3588  df-op 3590  df-uni 3795  df-br 3988  df-iota 5158  df-fv 5204

This theorem is referenced by:  fveq2i  5497  fveq2d  5498  2fveq3  5499  fvifdc  5516  dffn5imf  5549  fvelimab  5550  ssimaex  5555  fvco4  5566  fvmptssdm  5578  fvmptf  5586  eqfnfv2f  5595  fvelrn  5624  ralrnmpt  5635  rexrnmpt  5636  ffnfvf  5652  fmptco  5659  cofmpt  5662  fcompt  5663  fcoconst  5664  fnressn  5679  fressnfv  5680  fconstfvm  5711  foco2  5730  funiunfvdmf  5740  f1veqaeq  5745  dff13f  5746  f1fveq  5748  f1elima  5749  f1ocnvfv  5755  f1ocnvfvb  5756  fcofo  5760  cocan2  5764  fliftfun  5772  isorel  5784  isocnv  5787  isotr  5792  f1oiso2  5803  canth  5804  imbrov2fvoveq  5875  ffnov  5954  eqfnov  5956  fnovim  5958  fnrnov  5995  foov  5996  funimassov  5999  ovelimab  6000  suppssfv  6054  ofvalg  6067  ofrval  6068  offval2  6073  ofrfval2  6074  ofco  6076  caofinvl  6080  op1std  6124  op2ndd  6125  1stval2  6131  2ndval2  6132  unielxp  6150  reldm  6162  oprabco  6193  2ndconst  6198  f1o2ndf1  6204  mpoxopn0yelv  6215  mpoxopoveq  6216  smoel  6276  tfrlem1  6284  tfrlem3-2d  6288  tfrlem5  6290  tfrlem9  6295  tfr0dm  6298  tfrlemiubacc  6306  tfrlemi1  6308  tfrexlem  6310  tfr1onlemsucfn  6316  tfr1onlemsucaccv  6317  tfr1onlembxssdm  6319  tfr1onlembfn  6320  tfr1onlemubacc  6322  tfr1onlemaccex  6324  tfr1onlemres  6325  tfri1dALT  6327  tfrcllemsucfn  6329  tfrcllemsucaccv  6330  tfrcllembxssdm  6332  tfrcllembfn  6333  tfrcllemubacc  6335  tfrcllemaccex  6337  tfrcllemres  6338  tfrcldm  6339  tfrcl  6340  tfri3  6343  rdgtfr  6350  rdgss  6359  rdgisuc1  6360  rdgisucinc  6361  rdgon  6362  frecabex  6374  frecabcl  6375  frecfcllem  6380  frecsuclem  6382  frecsuc  6383  frecrdg  6384  oav  6430  omv  6431  oeiv  6432  fvixp  6677  cbvixp  6689  mptelixpg  6708  elixpsn  6709  dom2lem  6746  xpcomco  6800  xpmapen  6824  fidceq  6843  fieq0  6949  ordiso2  7008  djune  7051  updjudhcoinlf  7053  updjudhcoinrg  7054  updjud  7055  omp1eom  7068  0ct  7080  ctmlemr  7081  ctssdclemn0  7083  ctssdccl  7084  ctssdc  7086  enumctlemm  7087  nnnninfeq  7100  nnnninfeq2  7101  enomnilem  7110  finomni  7112  fodjuomnilemdc  7116  fodju0  7119  fodjuomni  7121  ismkvnex  7127  fodjumkv  7132  exmidaclem  7172  cc1  7214  cc2lem  7215  cc2  7216  cc3  7217  mulpipq2  7320  genipv  7458  genpelxp  7460  addcanprleml  7563  addcanprlemu  7564  recexprlemm  7573  recexprlemdisj  7579  recexprlemloc  7580  recexprlem1ssl  7582  recexprlem1ssu  7583  cauappcvgprlemm  7594  cauappcvgprlemdisj  7600  cauappcvgprlemloc  7601  cauappcvgprlemladdru  7605  cauappcvgprlemladdrl  7606  cauappcvgprlem1  7608  cauappcvgprlem2  7609  cauappcvgprlemlim  7610  cauappcvgpr  7611  caucvgprlemnkj  7615  caucvgprlemnbj  7616  caucvgprlemm  7617  caucvgprlemdisj  7623  caucvgprlemloc  7624  caucvgprlemcl  7625  caucvgprlemladdfu  7626  caucvgprlemladdrl  7627  caucvgprlem1  7628  caucvgprlem2  7629  caucvgpr  7631  caucvgprprlemell  7634  caucvgprprlemelu  7635  caucvgprprlemcbv  7636  caucvgprprlemval  7637  caucvgprprlemnkeqj  7639  caucvgprprlemnbj  7642  caucvgprprlemml  7643  caucvgprprlemmu  7644  caucvgprprlemopl  7646  caucvgprprlemlol  7647  caucvgprprlemopu  7648  caucvgprprlemloc  7652  caucvgprprlemclphr  7654  caucvgprprlemexbt  7655  caucvgprprlem1  7658  caucvgprprlem2  7659  caucvgsrlemcl  7738  caucvgsrlemfv  7740  caucvgsrlembound  7743  caucvgsrlemgt1  7744  caucvgsrlemoffval  7745  caucvgsrlemoffres  7749  caucvgsrlembnd  7750  caucvgsr  7751  axcaucvglemcau  7847  axcaucvglemres  7848  uz11  9496  cnref1o  9596  fzprval  10025  fztpval  10026  frec2uzuzd  10345  frec2uzltd  10346  frec2uzlt2d  10347  frecuzrdgrrn  10351  frec2uzrdg  10352  frecuzrdgtcl  10355  frecuzrdgg  10359  frecuzrdgfunlem  10362  frecfzennn  10369  seqeq1  10391  iseqovex  10399  seq3val  10401  seqvalcd  10402  seq3-1  10403  seqf  10404  seq3p1  10405  seqovcd  10406  seqp1cd  10409  seq3clss  10410  seq3fveq2  10412  seq3fveq  10414  seq3feq  10415  seq3shft2  10416  monoord  10419  monoord2  10420  ser3mono  10421  seq3split  10422  seq3caopr3  10424  seq3caopr2  10425  iseqf1olemkle  10427  iseqf1olemklt  10428  iseqf1olemqval  10430  iseqf1olemqk  10437  iseqf1olemjpcl  10438  iseqf1olemqpcl  10439  iseqf1olemfvp  10440  seq3f1olemqsumkj  10441  seq3f1olemqsum  10443  seq3f1olemstep  10444  seq3f1olemp  10445  seq3f1oleml  10446  seq3f1o  10447  seq3id2  10452  seq3homo  10453  seq3z  10454  ser3ge0  10460  ser3le  10461  exp3vallem  10464  exp3val  10465  facp1  10651  faccl  10656  facdiv  10659  facwordi  10661  faclbnd  10662  facubnd  10666  bcval  10670  bcval5  10684  fz1eqb  10712  omgadd  10724  hashxp  10748  zfz1isolem1  10762  zfz1iso  10763  seq3coll  10764  seq3shft  10789  reval  10800  replim  10810  cj11  10856  caucvgre  10932  cvg1nlemcau  10935  cvg1nlemres  10936  rexuz3  10941  absval  10952  resqrexlemover  10961  resqrexlemdecn  10963  resqrexlemlo  10964  resqrexlemcalc3  10967  resqrexlemnm  10969  resqrexlemcvg  10970  resqrexlemoverl  10972  resqrexlemglsq  10973  resqrexlemga  10974  resqrexlemsqa  10975  resqrexlemex  10976  abs00bd  11017  cau3lem  11065  caubnd2  11068  climconst  11240  climmpt  11250  climshftlemg  11252  climcn1  11258  climle  11284  climub  11294  climserle  11295  climcau  11297  climcvg1nlem  11299  climcvg1n  11300  serf0  11302  fsum3cvg  11328  summodclem3  11330  summodclem2a  11331  summodclem2  11332  summodc  11333  zsumdc  11334  fsum3  11337  fsumf1o  11340  fisumss  11342  fsum3cvg2  11344  fsum3ser  11347  fsumcl2lem  11348  fsumadd  11356  sumsnf  11359  isummulc2  11376  isumge0  11380  isumadd  11381  fsum2dlemstep  11384  fsummulc2  11398  fsumconst  11404  fsumrelem  11421  isumshft  11440  isum1p  11442  isumnn0nn  11443  isumrpcl  11444  isumlessdc  11446  cvgratnnlemnexp  11474  cvgratnnlemmn  11475  cvgratnnlemseq  11476  cvgratnnlemabsle  11477  cvgratnnlemfm  11479  cvgratnnlemrate  11480  cvgratnn  11481  cvgratz  11482  mertenslemi1  11485  mertenslem2  11486  mertensabs  11487  clim2prod  11489  prodfap0  11495  prodfrecap  11496  prodfdivap  11497  fproddccvg  11522  prodmodclem3  11525  prodmodclem2a  11526  prodmodclem2  11527  prodmodc  11528  zproddc  11529  fprodseq  11533  fprodf1o  11538  fprodssdc  11540  fprodmul  11541  prodsnf  11542  fprodfac  11565  fprodconst  11570  fprod2dlemstep  11572  eftvalcn  11607  ef0lem  11610  ege2le3  11621  efcj  11623  efaddlem  11624  eftlub  11640  efgt1p2  11645  reef11  11649  tanvalap  11658  efieq1re  11721  eirraplem  11726  dvdsabseq  11794  dvdsfac  11807  zsupcllemex  11888  infssuzex  11891  suprzubdc  11894  gcd0id  11921  nn0seqcvgd  11982  alginv  11988  algcvg  11989  algcvga  11992  algfx  11993  eucalglt  11998  lcmid  12021  qredeu  12038  prmfac1  12093  sqne2sq  12118  qnumdenbi  12133  dfphi2  12161  eulerthlemrprm  12170  eulerthlema  12171  eulerthlemh  12172  eulerthlemth  12173  phisum  12181  pcmpt  12282  pcfac  12289  1arithlem4  12305  elgz  12310  4sqlem4  12331  ennnfonelemk  12342  ennnfonelemp1  12348  ennnfoneleminc  12353  ennnfonelemkh  12354  ennnfonelemhf1o  12355  ennnfonelemex  12356  ennnfonelemhom  12357  ennnfonelemrn  12361  ennnfonelemnn0  12364  ennnfonelemr  12365  ennnfonelemim  12366  ctinfomlemom  12369  ctinfom  12370  ctiunctlemfo  12381  nninfdclemlt  12393  nninfdclemf1  12394  sloteq  12408  topnvalg  12577  ismgm  12597  plusffvalg  12602  grpidvalg  12613  issgrp  12630  ismnddef  12640  ismhm  12671  mhmlin  12676  issubm  12681  mhmeql  12693  istps  12745  clsfval  12816  cnpval  12913  lmconst  12931  txcnp  12986  upxp  12987  uptx  12989  txlm  12994  lmcn2  12995  cnmpt11  12998  cnmpt11f  12999  cnmpt1t  13000  cnmpt21  13006  cnmpt21f  13007  cnmpt2t  13008  mopnval  13157  isxms  13166  isms  13168  comet  13214  mopnex  13220  xmetxp  13222  xmetxpbl  13223  txmetcnp  13233  txmetcn  13234  qtopbasss  13236  cncfi  13280  cncfmpt1f  13299  ivthinclemlm  13327  ivthinclemum  13328  ivthinclemlopn  13329  ivthinclemlr  13330  ivthinclemuopn  13331  ivthinclemur  13332  ivthinclemdisj  13333  ivthinclemloc  13334  ivthinc  13336  ivthdec  13337  cnlimci  13357  limccnpcntop  13359  eldvap  13366  dvcoapbr  13386  dvcj  13388  dvfre  13389  dvmptcjx  13401  dveflem  13402  sin0pilem2  13418  pilem3  13419  coseq0q4123  13470  coseq0negpitopi  13472  cos11  13489  logltb  13510  rpcxpef  13530  rplogbval  13578  zabsle1  13615  lgslem2  13617  lgslem3  13618  lgsfcl2  13622  lgsfle1  13625  lgsle1  13631  lgsdirprm  13650  2sqlem1  13665  2sqlem2  13666  mul2sq  13667  2sqlem3  13668  2sqlem9  13675  2sqlem10  13676  012of  13950  2o01f  13951  subctctexmid  13956  nnsf  13960  nninfalllem1  13963  nninffeq  13975  qdencn  13981  trilpolemclim  13990  trilpolemcl  13991  trilpolemisumle  13992  trilpolemeq1  13994  trilpolemlt1  13995  trilpo  13997  iswomni0  14005  redcwlpo  14009  dceqnconst  14013  dcapnconst  14014  nconstwlpolemgt0  14017  nconstwlpolem  14018  nconstwlpo  14019  neapmkv  14021