Theorem fveq2 5270

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 3825	. . 3 |- ( A = B -> ( A F x <-> B F x ) )
2	1	iotabidv 4969	. 2 |- ( A = B -> ( iota x A F x ) = ( iota x B F x ) )
3		df-fv 4991	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 4991	. 2 |- ( F ` B ) = ( iota x B F x )
5	2, 3, 4	3eqtr4g 2142	1 |- ( A = B -> ( F ` A ) = ( F ` B ) )

Syntax hints:   -> wi 4   = wceq 1287   class class class wbr 3822   iotacio 4946   ` cfv 4983

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-rex 2361  df-v 2617  df-un 2992  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3639  df-br 3823  df-iota 4948  df-fv 4991

This theorem is referenced by:  fveq2i  5273  fveq2d  5274  2fveq3  5275  fvifdc  5292  dffn5imf  5324  fvelimab  5325  ssimaex  5330  fvco4  5341  fvmptssdm  5352  fvmptf  5360  eqfnfv2f  5366  fvelrn  5395  ralrnmpt  5406  rexrnmpt  5407  ffnfvf  5422  fmptco  5429  fcompt  5432  fcoconst  5433  fnressn  5448  fressnfv  5449  fconstfvm  5478  foco2  5496  funiunfvdmf  5506  f1veqaeq  5511  dff13f  5512  f1fveq  5514  f1elima  5515  f1ocnvfv  5521  f1ocnvfvb  5522  fcofo  5526  cocan2  5530  fliftfun  5538  isorel  5550  isocnv  5553  isotr  5558  f1oiso2  5569  ffnov  5708  eqfnov  5710  fnovim  5712  fnrnov  5749  foov  5750  funimassov  5753  ovelimab  5754  suppssfv  5811  fnofval  5824  ofrval  5825  offval2  5829  ofrfval2  5830  ofco  5832  caofinvl  5836  op1std  5878  op2ndd  5879  1stval2  5885  2ndval2  5886  unielxp  5903  reldm  5915  oprabco  5941  2ndconst  5946  f1o2ndf1  5952  mpt2xopn0yelv  5960  mpt2xopoveq  5961  smoel  6021  tfrlem1  6029  tfrlem3-2d  6033  tfrlem5  6035  tfrlem9  6040  tfr0dm  6043  tfrlemiubacc  6051  tfrlemi1  6053  tfrexlem  6055  tfr1onlemsucfn  6061  tfr1onlemsucaccv  6062  tfr1onlembxssdm  6064  tfr1onlembfn  6065  tfr1onlemubacc  6067  tfr1onlemaccex  6069  tfr1onlemres  6070  tfri1dALT  6072  tfrcllemsucfn  6074  tfrcllemsucaccv  6075  tfrcllembxssdm  6077  tfrcllembfn  6078  tfrcllemubacc  6080  tfrcllemaccex  6082  tfrcllemres  6083  tfrcldm  6084  tfrcl  6085  tfri3  6088  rdgtfr  6095  rdgss  6104  rdgisuc1  6105  rdgisucinc  6106  rdgon  6107  frecabex  6119  frecabcl  6120  frecfcllem  6125  frecsuclem  6127  frecsuc  6128  frecrdg  6129  oav  6171  omv  6172  oeiv  6173  dom2lem  6443  xpcomco  6496  xpmapen  6520  fidceq  6539  ordiso2  6675  djur  6704  djune  6716  updjudhcoinlf  6718  updjudhcoinrg  6719  updjud  6720  enomnilem  6741  finomni  6743  fodjuomnilemdc  6746  fodjuomnilemm  6748  fodjuomnilem0  6749  fodjuomnilemres  6750  fodjuomni  6751  mulpipq2  6877  genipv  7015  genpelxp  7017  addcanprleml  7120  addcanprlemu  7121  recexprlemm  7130  recexprlemdisj  7136  recexprlemloc  7137  recexprlem1ssl  7139  recexprlem1ssu  7140  cauappcvgprlemm  7151  cauappcvgprlemdisj  7157  cauappcvgprlemloc  7158  cauappcvgprlemladdru  7162  cauappcvgprlemladdrl  7163  cauappcvgprlem1  7165  cauappcvgprlem2  7166  cauappcvgprlemlim  7167  cauappcvgpr  7168  caucvgprlemnkj  7172  caucvgprlemnbj  7173  caucvgprlemm  7174  caucvgprlemdisj  7180  caucvgprlemloc  7181  caucvgprlemcl  7182  caucvgprlemladdfu  7183  caucvgprlemladdrl  7184  caucvgprlem1  7185  caucvgprlem2  7186  caucvgpr  7188  caucvgprprlemell  7191  caucvgprprlemelu  7192  caucvgprprlemcbv  7193  caucvgprprlemval  7194  caucvgprprlemnkeqj  7196  caucvgprprlemnbj  7199  caucvgprprlemml  7200  caucvgprprlemmu  7201  caucvgprprlemopl  7203  caucvgprprlemlol  7204  caucvgprprlemopu  7205  caucvgprprlemloc  7209  caucvgprprlemclphr  7211  caucvgprprlemexbt  7212  caucvgprprlem1  7215  caucvgprprlem2  7216  caucvgsrlemcl  7281  caucvgsrlemfv  7283  caucvgsrlembound  7286  caucvgsrlemgt1  7287  caucvgsrlemoffval  7288  caucvgsrlemoffres  7292  caucvgsrlembnd  7293  caucvgsr  7294  axcaucvglemcau  7380  axcaucvglemres  7381  uz11  8976  cnref1o  9068  fzprval  9429  fztpval  9430  frec2uzuzd  9740  frec2uzltd  9741  frec2uzlt2d  9742  frecuzrdgrrn  9746  frec2uzrdg  9747  frecuzrdgtcl  9750  frecuzrdgg  9754  frecuzrdgfunlem  9757  frecfzennn  9764  iseqeq1  9785  iseqovex  9790  iseqval  9791  iseqvalt  9793  iseq1  9794  iseq1t  9795  iseqfcl  9796  iseqfclt  9797  iseqcl  9798  iseqp1  9799  iseqp1t  9800  iseqclt  9801  iseqoveq  9802  iseqss  9803  iseqsst  9804  iseqfveq2  9806  iseqfveq  9808  iseqfeq  9809  iseqshft2  9810  monoord  9813  monoord2  9814  isermono  9815  iseqsplit  9816  iseqcaopr3  9818  iseqcaopr2  9819  iseqf1olemkle  9821  iseqf1olemklt  9822  iseqf1olemqval  9824  iseqf1olemqk  9831  iseqf1olemjpcl  9832  iseqf1olemqpcl  9833  iseqf1olemfvp  9834  iseqf1olemqsumkj  9835  iseqf1olemqsum  9837  iseqf1olemstep  9838  iseqf1olemp  9839  iseqf1oleml  9840  iseqf1o  9841  iseqid3s  9845  iseqid2  9847  iseqhomo  9848  iseqz  9849  serile  9855  expivallem  9858  expival  9859  facp1  10038  faccl  10043  facdiv  10046  facwordi  10048  faclbnd  10049  facubnd  10053  bcval  10057  ibcval5  10071  fz1eqb  10099  omgadd  10110  hashxp  10134  zfz1isolem1  10145  zfz1iso  10146  iseqcoll  10147  reval  10182  replim  10192  cj11  10238  caucvgre  10313  cvg1nlemcau  10316  cvg1nlemres  10317  rexuz3  10322  absval  10333  resqrexlemover  10342  resqrexlemdecn  10344  resqrexlemlo  10345  resqrexlemcalc3  10348  resqrexlemnm  10350  resqrexlemcvg  10351  resqrexlemoverl  10353  resqrexlemglsq  10354  resqrexlemga  10355  resqrexlemsqa  10356  resqrexlemex  10357  abs00bd  10398  cau3lem  10446  caubnd2  10449  climconst  10576  climmpt  10586  climshftlemg  10588  climcn1  10594  climle  10619  climub  10629  climserile  10630  climcau  10631  climcvg1nlem  10633  climcvg1n  10634  serif0  10636  fisumcvg  10661  isummolem3  10664  isummolem2a  10665  isummolem2  10666  isummo  10667  zisum  10668  fisum  10670  fsumf1o  10673  fisumss  10675  fisumcvg2  10677  fsumcl2lem  10680  fsumadd  10688  sumsnf  10691  dvdsabseq  10754  dvdsfac  10767  zsupcllemex  10848  infssuzex  10851  gcd0id  10876  nn0seqcvgd  10929  ialginv  10935  ialgcvg  10936  ialgcvga  10939  ialgfx  10940  eucalglt  10945  lcmid  10968  qredeu  10985  prmfac1  11037  sqne2sq  11061  qnumdenbi  11076  dfphi2  11102  nnsf  11364  nninfalllemn  11367  nninfalllem1  11368  nninfomnilem  11379  qdencn  11384