Theorem fveq2 5353

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 3878	. . 3 |- ( A = B -> ( A F x <-> B F x ) )
2	1	iotabidv 5045	. 2 |- ( A = B -> ( iota x A F x ) = ( iota x B F x ) )
3		df-fv 5067	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5067	. 2 |- ( F ` B ) = ( iota x B F x )
5	2, 3, 4	3eqtr4g 2157	1 |- ( A = B -> ( F ` A ) = ( F ` B ) )

Syntax hints:   -> wi 4   = wceq 1299   class class class wbr 3875   iotacio 5022   ` cfv 5059

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-3an 932  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-rex 2381  df-v 2643  df-un 3025  df-sn 3480  df-pr 3481  df-op 3483  df-uni 3684  df-br 3876  df-iota 5024  df-fv 5067

This theorem is referenced by:  fveq2i  5356  fveq2d  5357  2fveq3  5358  fvifdc  5375  dffn5imf  5408  fvelimab  5409  ssimaex  5414  fvco4  5425  fvmptssdm  5437  fvmptf  5445  eqfnfv2f  5454  fvelrn  5483  ralrnmpt  5494  rexrnmpt  5495  ffnfvf  5511  fmptco  5518  cofmpt  5521  fcompt  5522  fcoconst  5523  fnressn  5538  fressnfv  5539  fconstfvm  5570  foco2  5587  funiunfvdmf  5597  f1veqaeq  5602  dff13f  5603  f1fveq  5605  f1elima  5606  f1ocnvfv  5612  f1ocnvfvb  5613  fcofo  5617  cocan2  5621  fliftfun  5629  isorel  5641  isocnv  5644  isotr  5649  f1oiso2  5660  imbrov2fvoveq  5731  ffnov  5807  eqfnov  5809  fnovim  5811  fnrnov  5848  foov  5849  funimassov  5852  ovelimab  5853  suppssfv  5910  fnofval  5923  ofrval  5924  offval2  5928  ofrfval2  5929  ofco  5931  caofinvl  5935  op1std  5977  op2ndd  5978  1stval2  5984  2ndval2  5985  unielxp  6002  reldm  6014  oprabco  6044  2ndconst  6049  f1o2ndf1  6055  mpoxopn0yelv  6066  mpoxopoveq  6067  smoel  6127  tfrlem1  6135  tfrlem3-2d  6139  tfrlem5  6141  tfrlem9  6146  tfr0dm  6149  tfrlemiubacc  6157  tfrlemi1  6159  tfrexlem  6161  tfr1onlemsucfn  6167  tfr1onlemsucaccv  6168  tfr1onlembxssdm  6170  tfr1onlembfn  6171  tfr1onlemubacc  6173  tfr1onlemaccex  6175  tfr1onlemres  6176  tfri1dALT  6178  tfrcllemsucfn  6180  tfrcllemsucaccv  6181  tfrcllembxssdm  6183  tfrcllembfn  6184  tfrcllemubacc  6186  tfrcllemaccex  6188  tfrcllemres  6189  tfrcldm  6190  tfrcl  6191  tfri3  6194  rdgtfr  6201  rdgss  6210  rdgisuc1  6211  rdgisucinc  6212  rdgon  6213  frecabex  6225  frecabcl  6226  frecfcllem  6231  frecsuclem  6233  frecsuc  6234  frecrdg  6235  oav  6280  omv  6281  oeiv  6282  fvixp  6527  cbvixp  6539  mptelixpg  6558  elixpsn  6559  dom2lem  6596  xpcomco  6649  xpmapen  6673  fidceq  6692  ordiso2  6835  djune  6878  updjudhcoinlf  6880  updjudhcoinrg  6881  updjud  6882  omp1eom  6895  0ct  6907  ctmlemr  6908  ctssdclemn0  6910  ctssdclemr  6911  ctssdc  6912  enumctlemm  6913  enomnilem  6922  finomni  6924  fodjuomnilemdc  6928  fodju0  6931  fodjuomni  6933  fodjumkv  6945  mulpipq2  7080  genipv  7218  genpelxp  7220  addcanprleml  7323  addcanprlemu  7324  recexprlemm  7333  recexprlemdisj  7339  recexprlemloc  7340  recexprlem1ssl  7342  recexprlem1ssu  7343  cauappcvgprlemm  7354  cauappcvgprlemdisj  7360  cauappcvgprlemloc  7361  cauappcvgprlemladdru  7365  cauappcvgprlemladdrl  7366  cauappcvgprlem1  7368  cauappcvgprlem2  7369  cauappcvgprlemlim  7370  cauappcvgpr  7371  caucvgprlemnkj  7375  caucvgprlemnbj  7376  caucvgprlemm  7377  caucvgprlemdisj  7383  caucvgprlemloc  7384  caucvgprlemcl  7385  caucvgprlemladdfu  7386  caucvgprlemladdrl  7387  caucvgprlem1  7388  caucvgprlem2  7389  caucvgpr  7391  caucvgprprlemell  7394  caucvgprprlemelu  7395  caucvgprprlemcbv  7396  caucvgprprlemval  7397  caucvgprprlemnkeqj  7399  caucvgprprlemnbj  7402  caucvgprprlemml  7403  caucvgprprlemmu  7404  caucvgprprlemopl  7406  caucvgprprlemlol  7407  caucvgprprlemopu  7408  caucvgprprlemloc  7412  caucvgprprlemclphr  7414  caucvgprprlemexbt  7415  caucvgprprlem1  7418  caucvgprprlem2  7419  caucvgsrlemcl  7484  caucvgsrlemfv  7486  caucvgsrlembound  7489  caucvgsrlemgt1  7490  caucvgsrlemoffval  7491  caucvgsrlemoffres  7495  caucvgsrlembnd  7496  caucvgsr  7497  axcaucvglemcau  7583  axcaucvglemres  7584  uz11  9198  cnref1o  9290  fzprval  9703  fztpval  9704  frec2uzuzd  10016  frec2uzltd  10017  frec2uzlt2d  10018  frecuzrdgrrn  10022  frec2uzrdg  10023  frecuzrdgtcl  10026  frecuzrdgg  10030  frecuzrdgfunlem  10033  frecfzennn  10040  seqeq1  10062  iseqovex  10070  seq3val  10072  seqvalcd  10073  seq3-1  10074  seqf  10075  seq3p1  10076  seqovcd  10077  seqp1cd  10080  seq3clss  10081  seq3fveq2  10083  seq3fveq  10085  seq3feq  10086  seq3shft2  10087  monoord  10090  monoord2  10091  ser3mono  10092  seq3split  10093  seq3caopr3  10095  seq3caopr2  10096  iseqf1olemkle  10098  iseqf1olemklt  10099  iseqf1olemqval  10101  iseqf1olemqk  10108  iseqf1olemjpcl  10109  iseqf1olemqpcl  10110  iseqf1olemfvp  10111  seq3f1olemqsumkj  10112  seq3f1olemqsum  10114  seq3f1olemstep  10115  seq3f1olemp  10116  seq3f1oleml  10117  seq3f1o  10118  seq3id2  10123  seq3homo  10124  seq3z  10125  ser3ge0  10131  ser3le  10132  exp3vallem  10135  exp3val  10136  facp1  10317  faccl  10322  facdiv  10325  facwordi  10327  faclbnd  10328  facubnd  10332  bcval  10336  bcval5  10350  fz1eqb  10378  omgadd  10389  hashxp  10413  zfz1isolem1  10424  zfz1iso  10425  seq3coll  10426  seq3shft  10451  reval  10462  replim  10472  cj11  10518  caucvgre  10593  cvg1nlemcau  10596  cvg1nlemres  10597  rexuz3  10602  absval  10613  resqrexlemover  10622  resqrexlemdecn  10624  resqrexlemlo  10625  resqrexlemcalc3  10628  resqrexlemnm  10630  resqrexlemcvg  10631  resqrexlemoverl  10633  resqrexlemglsq  10634  resqrexlemga  10635  resqrexlemsqa  10636  resqrexlemex  10637  abs00bd  10678  cau3lem  10726  caubnd2  10729  climconst  10898  climmpt  10908  climshftlemg  10910  climcn1  10916  climle  10942  climub  10952  climserle  10953  climcau  10955  climcvg1nlem  10957  climcvg1n  10958  serf0  10960  fsum3cvg  10985  summodclem3  10988  summodclem2a  10989  summodclem2  10990  summodc  10991  zsumdc  10992  fsum3  10995  fsumf1o  10998  fisumss  11000  fsum3cvg2  11002  fsum3ser  11005  fsumcl2lem  11006  fsumadd  11014  sumsnf  11017  isummulc2  11034  isumge0  11038  isumadd  11039  fsum2dlemstep  11042  fsummulc2  11056  fsumconst  11062  fsumrelem  11079  isumshft  11098  isum1p  11100  isumnn0nn  11101  isumrpcl  11102  isumlessdc  11104  cvgratnnlemnexp  11132  cvgratnnlemmn  11133  cvgratnnlemseq  11134  cvgratnnlemabsle  11135  cvgratnnlemfm  11137  cvgratnnlemrate  11138  cvgratnn  11139  cvgratz  11140  mertenslemi1  11143  mertenslem2  11144  mertensabs  11145  eftvalcn  11161  ef0lem  11164  ege2le3  11175  efcj  11177  efaddlem  11178  eftlub  11194  efgt1p2  11199  reef11  11204  tanvalap  11213  efieq1re  11275  eirraplem  11278  dvdsabseq  11340  dvdsfac  11353  zsupcllemex  11434  infssuzex  11437  gcd0id  11462  nn0seqcvgd  11515  alginv  11521  algcvg  11522  algcvga  11525  algfx  11526  eucalglt  11531  lcmid  11554  qredeu  11571  prmfac1  11623  sqne2sq  11647  qnumdenbi  11662  dfphi2  11688  ennnfonelemk  11705  ennnfonelemp1  11711  ennnfoneleminc  11716  ennnfonelemkh  11717  ennnfonelemhf1o  11718  ennnfonelemex  11719  ennnfonelemhom  11720  ennnfonelemrn  11724  ennnfonelemnn0  11727  ennnfonelemr  11728  ennnfonelemim  11729  ctinfomlemom  11732  ctinfom  11733  sloteq  11746  topnvalg  11914  istps  11981  clsfval  12052  cnpval  12148  lmconst  12166  txcnp  12221  upxp  12222  uptx  12224  txlm  12229  lmcn2  12230  cnmpt11  12233  cnmpt11f  12234  cnmpt1t  12235  cnmpt21  12241  cnmpt21f  12242  cnmpt2t  12243  mopnval  12370  isxms  12379  isms  12381  comet  12427  mopnex  12433  qtopbasss  12443  cncfi  12478  cncfmpt1f  12497  cnlimci  12518  limccnpcntop  12520  eldvap  12524  nnsf  12783  nninfalllemn  12786  nninfalllem1  12787  nninfomnilem  12798  nninffeq  12800  qdencn  12806  isomninnlem  12809  trilpolemclim  12813  trilpolemcl  12814  trilpolemisumle  12815  trilpolemeq1  12817  trilpolemlt1  12818  trilpo  12820