Theorem fveq2 5253

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 3814	. . 3 |- ( A = B -> ( A F x <-> B F x ) )
2	1	iotabidv 4955	. 2 |- ( A = B -> ( iota x A F x ) = ( iota x B F x ) )
3		df-fv 4977	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 4977	. 2 |- ( F ` B ) = ( iota x B F x )
5	2, 3, 4	3eqtr4g 2140	1 |- ( A = B -> ( F ` A ) = ( F ` B ) )

Syntax hints:   -> wi 4   = wceq 1285   class class class wbr 3811   iotacio 4932   ` cfv 4969

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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065

This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-rex 2359  df-v 2614  df-un 2988  df-sn 3428  df-pr 3429  df-op 3431  df-uni 3628  df-br 3812  df-iota 4934  df-fv 4977

This theorem is referenced by:  fveq2i  5256  fveq2d  5257  fvifdc  5272  dffn5imf  5304  fvelimab  5305  ssimaex  5310  fvco4  5321  fvmptssdm  5332  fvmptf  5340  eqfnfv2f  5346  fvelrn  5375  ralrnmpt  5386  rexrnmpt  5387  ffnfvf  5399  fmptco  5406  fcompt  5409  fcoconst  5410  fnressn  5425  fressnfv  5426  fconstfvm  5455  foco2  5473  funiunfvdmf  5483  f1veqaeq  5488  dff13f  5489  f1fveq  5491  f1elima  5492  f1ocnvfv  5498  f1ocnvfvb  5499  fcofo  5503  cocan2  5507  fliftfun  5515  isorel  5527  isocnv  5530  isotr  5535  f1oiso2  5545  ffnov  5684  eqfnov  5686  fnovim  5688  fnrnov  5725  foov  5726  funimassov  5729  ovelimab  5730  suppssfv  5787  fnofval  5800  ofrval  5801  offval2  5805  ofrfval2  5806  ofco  5808  caofinvl  5812  op1std  5854  op2ndd  5855  1stval2  5861  2ndval2  5862  unielxp  5879  reldm  5891  oprabco  5917  2ndconst  5922  f1o2ndf1  5928  mpt2xopn0yelv  5936  mpt2xopoveq  5937  smoel  5997  tfrlem1  6005  tfrlem3-2d  6009  tfrlem5  6011  tfrlem9  6016  tfr0dm  6019  tfrlemiubacc  6027  tfrlemi1  6029  tfrexlem  6031  tfr1onlemsucfn  6037  tfr1onlemsucaccv  6038  tfr1onlembxssdm  6040  tfr1onlembfn  6041  tfr1onlemubacc  6043  tfr1onlemaccex  6045  tfr1onlemres  6046  tfri1dALT  6048  tfrcllemsucfn  6050  tfrcllemsucaccv  6051  tfrcllembxssdm  6053  tfrcllembfn  6054  tfrcllemubacc  6056  tfrcllemaccex  6058  tfrcllemres  6059  tfrcldm  6060  tfrcl  6061  tfri3  6064  rdgtfr  6071  rdgss  6080  rdgisuc1  6081  rdgisucinc  6082  rdgon  6083  frecabex  6095  frecabcl  6096  frecfcllem  6101  frecsuclem  6103  frecsuc  6104  frecrdg  6105  oav  6147  omv  6148  oeiv  6149  dom2lem  6419  xpcomco  6472  xpmapen  6496  fidceq  6515  ordiso2  6635  djur  6664  djune  6676  updjudhcoinlf  6678  updjudhcoinrg  6679  updjud  6680  enomnilem  6699  finomni  6701  fodjuomnilemdc  6704  fodjuomnilemm  6706  fodjuomnilem0  6707  fodjuomnilemres  6708  fodjuomni  6709  mulpipq2  6833  genipv  6971  genpelxp  6973  addcanprleml  7076  addcanprlemu  7077  recexprlemm  7086  recexprlemdisj  7092  recexprlemloc  7093  recexprlem1ssl  7095  recexprlem1ssu  7096  cauappcvgprlemm  7107  cauappcvgprlemdisj  7113  cauappcvgprlemloc  7114  cauappcvgprlemladdru  7118  cauappcvgprlemladdrl  7119  cauappcvgprlem1  7121  cauappcvgprlem2  7122  cauappcvgprlemlim  7123  cauappcvgpr  7124  caucvgprlemnkj  7128  caucvgprlemnbj  7129  caucvgprlemm  7130  caucvgprlemdisj  7136  caucvgprlemloc  7137  caucvgprlemcl  7138  caucvgprlemladdfu  7139  caucvgprlemladdrl  7140  caucvgprlem1  7141  caucvgprlem2  7142  caucvgpr  7144  caucvgprprlemell  7147  caucvgprprlemelu  7148  caucvgprprlemcbv  7149  caucvgprprlemval  7150  caucvgprprlemnkeqj  7152  caucvgprprlemnbj  7155  caucvgprprlemml  7156  caucvgprprlemmu  7157  caucvgprprlemopl  7159  caucvgprprlemlol  7160  caucvgprprlemopu  7161  caucvgprprlemloc  7165  caucvgprprlemclphr  7167  caucvgprprlemexbt  7168  caucvgprprlem1  7171  caucvgprprlem2  7172  caucvgsrlemcl  7237  caucvgsrlemfv  7239  caucvgsrlembound  7242  caucvgsrlemgt1  7243  caucvgsrlemoffval  7244  caucvgsrlemoffres  7248  caucvgsrlembnd  7249  caucvgsr  7250  axcaucvglemcau  7336  axcaucvglemres  7337  uz11  8936  cnref1o  9028  fzprval  9389  fztpval  9390  frec2uzuzd  9698  frec2uzltd  9699  frec2uzlt2d  9700  frecuzrdgrrn  9704  frec2uzrdg  9705  frecuzrdgtcl  9708  frecuzrdgg  9712  frecuzrdgfunlem  9715  frecfzennn  9722  iseqeq1  9743  iseqovex  9748  iseqval  9749  iseqvalt  9751  iseq1  9752  iseq1t  9753  iseqfcl  9754  iseqfclt  9755  iseqcl  9756  iseqp1  9757  iseqp1t  9758  iseqoveq  9759  iseqss  9760  iseqsst  9761  iseqfveq2  9763  iseqfveq  9765  iseqfeq  9766  iseqshft2  9767  monoord  9770  monoord2  9771  isermono  9772  iseqsplit  9773  iseqcaopr3  9775  iseqcaopr2  9776  iseqid3s  9781  iseqid2  9783  iseqhomo  9784  iseqz  9785  serile  9790  expivallem  9793  expival  9794  facp1  9973  faccl  9978  facdiv  9981  facwordi  9983  faclbnd  9984  facubnd  9988  bcval  9992  ibcval5  10006  fz1eqb  10034  omgadd  10045  hashxp  10069  reval  10110  replim  10120  cj11  10166  caucvgre  10241  cvg1nlemcau  10244  cvg1nlemres  10245  rexuz3  10250  absval  10261  resqrexlemover  10270  resqrexlemdecn  10272  resqrexlemlo  10273  resqrexlemcalc3  10276  resqrexlemnm  10278  resqrexlemcvg  10279  resqrexlemoverl  10281  resqrexlemglsq  10282  resqrexlemga  10283  resqrexlemsqa  10284  resqrexlemex  10285  abs00bd  10326  cau3lem  10374  caubnd2  10377  climconst  10503  climmpt  10513  climshftlemg  10515  climcn1  10521  climle  10546  climub  10556  climserile  10557  climcau  10558  climcvg1nlem  10560  climcvg1n  10561  serif0  10563  fisumcvg  10574  dvdsabseq  10628  dvdsfac  10641  zsupcllemex  10722  infssuzex  10725  gcd0id  10750  nn0seqcvgd  10803  ialginv  10809  ialgcvg  10810  ialgcvga  10813  ialgfx  10814  eucalglt  10819  lcmid  10842  qredeu  10859  prmfac1  10911  sqne2sq  10935  qnumdenbi  10950  dfphi2  10976  qdencn  11228