Theorem fveq2 5429

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 3940	. . 3 |- ( A = B -> ( A F x <-> B F x ) )
2	1	iotabidv 5117	. 2 |- ( A = B -> ( iota x A F x ) = ( iota x B F x ) )
3		df-fv 5139	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5139	. 2 |- ( F ` B ) = ( iota x B F x )
5	2, 3, 4	3eqtr4g 2198	1 |- ( A = B -> ( F ` A ) = ( F ` B ) )

Syntax hints:   -> wi 4   = wceq 1332   class class class wbr 3937   iotacio 5094   ` cfv 5131

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rex 2423  df-v 2691  df-un 3080  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-br 3938  df-iota 5096  df-fv 5139

This theorem is referenced by:  fveq2i  5432  fveq2d  5433  2fveq3  5434  fvifdc  5451  dffn5imf  5484  fvelimab  5485  ssimaex  5490  fvco4  5501  fvmptssdm  5513  fvmptf  5521  eqfnfv2f  5530  fvelrn  5559  ralrnmpt  5570  rexrnmpt  5571  ffnfvf  5587  fmptco  5594  cofmpt  5597  fcompt  5598  fcoconst  5599  fnressn  5614  fressnfv  5615  fconstfvm  5646  foco2  5663  funiunfvdmf  5673  f1veqaeq  5678  dff13f  5679  f1fveq  5681  f1elima  5682  f1ocnvfv  5688  f1ocnvfvb  5689  fcofo  5693  cocan2  5697  fliftfun  5705  isorel  5717  isocnv  5720  isotr  5725  f1oiso2  5736  imbrov2fvoveq  5807  ffnov  5883  eqfnov  5885  fnovim  5887  fnrnov  5924  foov  5925  funimassov  5928  ovelimab  5929  suppssfv  5986  ofvalg  5999  ofrval  6000  offval2  6005  ofrfval2  6006  ofco  6008  caofinvl  6012  op1std  6054  op2ndd  6055  1stval2  6061  2ndval2  6062  unielxp  6080  reldm  6092  oprabco  6122  2ndconst  6127  f1o2ndf1  6133  mpoxopn0yelv  6144  mpoxopoveq  6145  smoel  6205  tfrlem1  6213  tfrlem3-2d  6217  tfrlem5  6219  tfrlem9  6224  tfr0dm  6227  tfrlemiubacc  6235  tfrlemi1  6237  tfrexlem  6239  tfr1onlemsucfn  6245  tfr1onlemsucaccv  6246  tfr1onlembxssdm  6248  tfr1onlembfn  6249  tfr1onlemubacc  6251  tfr1onlemaccex  6253  tfr1onlemres  6254  tfri1dALT  6256  tfrcllemsucfn  6258  tfrcllemsucaccv  6259  tfrcllembxssdm  6261  tfrcllembfn  6262  tfrcllemubacc  6264  tfrcllemaccex  6266  tfrcllemres  6267  tfrcldm  6268  tfrcl  6269  tfri3  6272  rdgtfr  6279  rdgss  6288  rdgisuc1  6289  rdgisucinc  6290  rdgon  6291  frecabex  6303  frecabcl  6304  frecfcllem  6309  frecsuclem  6311  frecsuc  6312  frecrdg  6313  oav  6358  omv  6359  oeiv  6360  fvixp  6605  cbvixp  6617  mptelixpg  6636  elixpsn  6637  dom2lem  6674  xpcomco  6728  xpmapen  6752  fidceq  6771  fieq0  6872  ordiso2  6928  djune  6971  updjudhcoinlf  6973  updjudhcoinrg  6974  updjud  6975  omp1eom  6988  0ct  7000  ctmlemr  7001  ctssdclemn0  7003  ctssdccl  7004  ctssdc  7006  enumctlemm  7007  enomnilem  7018  finomni  7020  fodjuomnilemdc  7024  fodju0  7027  fodjuomni  7029  ismkvnex  7037  fodjumkv  7042  exmidaclem  7081  cc1  7097  cc2lem  7098  cc2  7099  cc3  7100  mulpipq2  7203  genipv  7341  genpelxp  7343  addcanprleml  7446  addcanprlemu  7447  recexprlemm  7456  recexprlemdisj  7462  recexprlemloc  7463  recexprlem1ssl  7465  recexprlem1ssu  7466  cauappcvgprlemm  7477  cauappcvgprlemdisj  7483  cauappcvgprlemloc  7484  cauappcvgprlemladdru  7488  cauappcvgprlemladdrl  7489  cauappcvgprlem1  7491  cauappcvgprlem2  7492  cauappcvgprlemlim  7493  cauappcvgpr  7494  caucvgprlemnkj  7498  caucvgprlemnbj  7499  caucvgprlemm  7500  caucvgprlemdisj  7506  caucvgprlemloc  7507  caucvgprlemcl  7508  caucvgprlemladdfu  7509  caucvgprlemladdrl  7510  caucvgprlem1  7511  caucvgprlem2  7512  caucvgpr  7514  caucvgprprlemell  7517  caucvgprprlemelu  7518  caucvgprprlemcbv  7519  caucvgprprlemval  7520  caucvgprprlemnkeqj  7522  caucvgprprlemnbj  7525  caucvgprprlemml  7526  caucvgprprlemmu  7527  caucvgprprlemopl  7529  caucvgprprlemlol  7530  caucvgprprlemopu  7531  caucvgprprlemloc  7535  caucvgprprlemclphr  7537  caucvgprprlemexbt  7538  caucvgprprlem1  7541  caucvgprprlem2  7542  caucvgsrlemcl  7621  caucvgsrlemfv  7623  caucvgsrlembound  7626  caucvgsrlemgt1  7627  caucvgsrlemoffval  7628  caucvgsrlemoffres  7632  caucvgsrlembnd  7633  caucvgsr  7634  axcaucvglemcau  7730  axcaucvglemres  7731  uz11  9372  cnref1o  9469  fzprval  9893  fztpval  9894  frec2uzuzd  10206  frec2uzltd  10207  frec2uzlt2d  10208  frecuzrdgrrn  10212  frec2uzrdg  10213  frecuzrdgtcl  10216  frecuzrdgg  10220  frecuzrdgfunlem  10223  frecfzennn  10230  seqeq1  10252  iseqovex  10260  seq3val  10262  seqvalcd  10263  seq3-1  10264  seqf  10265  seq3p1  10266  seqovcd  10267  seqp1cd  10270  seq3clss  10271  seq3fveq2  10273  seq3fveq  10275  seq3feq  10276  seq3shft2  10277  monoord  10280  monoord2  10281  ser3mono  10282  seq3split  10283  seq3caopr3  10285  seq3caopr2  10286  iseqf1olemkle  10288  iseqf1olemklt  10289  iseqf1olemqval  10291  iseqf1olemqk  10298  iseqf1olemjpcl  10299  iseqf1olemqpcl  10300  iseqf1olemfvp  10301  seq3f1olemqsumkj  10302  seq3f1olemqsum  10304  seq3f1olemstep  10305  seq3f1olemp  10306  seq3f1oleml  10307  seq3f1o  10308  seq3id2  10313  seq3homo  10314  seq3z  10315  ser3ge0  10321  ser3le  10322  exp3vallem  10325  exp3val  10326  facp1  10508  faccl  10513  facdiv  10516  facwordi  10518  faclbnd  10519  facubnd  10523  bcval  10527  bcval5  10541  fz1eqb  10569  omgadd  10580  hashxp  10604  zfz1isolem1  10615  zfz1iso  10616  seq3coll  10617  seq3shft  10642  reval  10653  replim  10663  cj11  10709  caucvgre  10785  cvg1nlemcau  10788  cvg1nlemres  10789  rexuz3  10794  absval  10805  resqrexlemover  10814  resqrexlemdecn  10816  resqrexlemlo  10817  resqrexlemcalc3  10820  resqrexlemnm  10822  resqrexlemcvg  10823  resqrexlemoverl  10825  resqrexlemglsq  10826  resqrexlemga  10827  resqrexlemsqa  10828  resqrexlemex  10829  abs00bd  10870  cau3lem  10918  caubnd2  10921  climconst  11091  climmpt  11101  climshftlemg  11103  climcn1  11109  climle  11135  climub  11145  climserle  11146  climcau  11148  climcvg1nlem  11150  climcvg1n  11151  serf0  11153  fsum3cvg  11179  summodclem3  11181  summodclem2a  11182  summodclem2  11183  summodc  11184  zsumdc  11185  fsum3  11188  fsumf1o  11191  fisumss  11193  fsum3cvg2  11195  fsum3ser  11198  fsumcl2lem  11199  fsumadd  11207  sumsnf  11210  isummulc2  11227  isumge0  11231  isumadd  11232  fsum2dlemstep  11235  fsummulc2  11249  fsumconst  11255  fsumrelem  11272  isumshft  11291  isum1p  11293  isumnn0nn  11294  isumrpcl  11295  isumlessdc  11297  cvgratnnlemnexp  11325  cvgratnnlemmn  11326  cvgratnnlemseq  11327  cvgratnnlemabsle  11328  cvgratnnlemfm  11330  cvgratnnlemrate  11331  cvgratnn  11332  cvgratz  11333  mertenslemi1  11336  mertenslem2  11337  mertensabs  11338  clim2prod  11340  prodfap0  11346  prodfrecap  11347  prodfdivap  11348  fproddccvg  11373  prodmodclem3  11376  prodmodclem2a  11377  prodmodclem2  11378  prodmodc  11379  zproddc  11380  fprodseq  11384  eftvalcn  11400  ef0lem  11403  ege2le3  11414  efcj  11416  efaddlem  11417  eftlub  11433  efgt1p2  11438  reef11  11442  tanvalap  11451  efieq1re  11514  eirraplem  11519  dvdsabseq  11581  dvdsfac  11594  zsupcllemex  11675  infssuzex  11678  gcd0id  11703  nn0seqcvgd  11758  alginv  11764  algcvg  11765  algcvga  11768  algfx  11769  eucalglt  11774  lcmid  11797  qredeu  11814  prmfac1  11866  sqne2sq  11891  qnumdenbi  11906  dfphi2  11932  ennnfonelemk  11949  ennnfonelemp1  11955  ennnfoneleminc  11960  ennnfonelemkh  11961  ennnfonelemhf1o  11962  ennnfonelemex  11963  ennnfonelemhom  11964  ennnfonelemrn  11968  ennnfonelemnn0  11971  ennnfonelemr  11972  ennnfonelemim  11973  ctinfomlemom  11976  ctinfom  11977  ctiunctlemfo  11988  sloteq  12003  topnvalg  12171  istps  12238  clsfval  12309  cnpval  12406  lmconst  12424  txcnp  12479  upxp  12480  uptx  12482  txlm  12487  lmcn2  12488  cnmpt11  12491  cnmpt11f  12492  cnmpt1t  12493  cnmpt21  12499  cnmpt21f  12500  cnmpt2t  12501  mopnval  12650  isxms  12659  isms  12661  comet  12707  mopnex  12713  xmetxp  12715  xmetxpbl  12716  txmetcnp  12726  txmetcn  12727  qtopbasss  12729  cncfi  12773  cncfmpt1f  12792  ivthinclemlm  12820  ivthinclemum  12821  ivthinclemlopn  12822  ivthinclemlr  12823  ivthinclemuopn  12824  ivthinclemur  12825  ivthinclemdisj  12826  ivthinclemloc  12827  ivthinc  12829  ivthdec  12830  cnlimci  12850  limccnpcntop  12852  eldvap  12859  dvcoapbr  12879  dvcj  12881  dvfre  12882  dvmptcjx  12894  dveflem  12895  sin0pilem2  12911  pilem3  12912  coseq0q4123  12963  coseq0negpitopi  12965  cos11  12982  logltb  13003  rpcxpef  13023  rplogbval  13070  012of  13363  2o01f  13364  subctctexmid  13369  nnsf  13374  nninfalllemn  13377  nninfalllem1  13378  nninfomnilem  13389  nninffeq  13391  qdencn  13397  trilpolemclim  13404  trilpolemcl  13405  trilpolemisumle  13406  trilpolemeq1  13408  trilpolemlt1  13409  trilpo  13411  redcwlpo  13422  dceqnconst  13423  neapmkv  13425