ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fveq2 Unicode version

Theorem fveq2 5205
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.
StepHypRef Expression
1 breq1 3794 . . 3  |-  ( A  =  B  ->  ( A F x  <->  B F x ) )
21iotabidv 4915 . 2  |-  ( A  =  B  ->  ( iota x A F x )  =  ( iota
x B F x ) )
3 df-fv 4937 . 2  |-  ( F `
 A )  =  ( iota x A F x )
4 df-fv 4937 . 2  |-  ( F `
 B )  =  ( iota x B F x )
52, 3, 43eqtr4g 2113 1  |-  ( A  =  B  ->  ( F `  A )  =  ( F `  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1259   class class class wbr 3791   iotacio 4892   ` cfv 4929
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-rex 2329  df-v 2576  df-un 2949  df-sn 3408  df-pr 3409  df-op 3411  df-uni 3608  df-br 3792  df-iota 4894  df-fv 4937
This theorem is referenced by:  fveq2i  5208  fveq2d  5209  dffn5imf  5255  fvelimab  5256  ssimaex  5261  fvmptssdm  5282  fvmptf  5290  eqfnfv2f  5296  fvelrn  5325  ralrnmpt  5336  rexrnmpt  5337  foco2  5345  ffnfvf  5351  fmptco  5357  fcompt  5360  fcoconst  5361  fnressn  5376  fressnfv  5377  fconstfvm  5406  funiunfvdmf  5430  f1veqaeq  5435  dff13f  5436  f1fveq  5438  f1elima  5439  f1ocnvfv  5446  f1ocnvfvb  5447  fcofo  5451  cocan2  5455  fliftfun  5463  isorel  5475  isocnv  5478  isotr  5483  f1oiso2  5493  ffnov  5632  eqfnov  5634  fnovim  5636  fnrnov  5673  foov  5674  funimassov  5677  ovelimab  5678  suppssfv  5735  fnofval  5748  ofrval  5749  offval2  5753  ofrfval2  5754  ofco  5756  caofinvl  5760  op1std  5802  op2ndd  5803  1stval2  5809  2ndval2  5810  unielxp  5827  reldm  5839  oprabco  5865  2ndconst  5870  f1o2ndf1  5876  mpt2xopn0yelv  5884  mpt2xopoveq  5885  smoel  5945  tfrlem1  5953  tfrlem3-2  5957  tfrlem3-2d  5958  tfrlem5  5960  tfrlem9  5965  tfr0  5967  tfrlemiubacc  5974  tfrlemi1  5976  tfrexlem  5978  tfri3  5983  rdgtfr  5991  rdgss  6000  rdgisuc1  6001  rdgisucinc  6002  rdgon  6003  frecabex  6014  frecsuclem3  6020  frecsuc  6021  frecrdg  6022  freccl  6023  oav  6064  omv  6065  oeiv  6066  dom2lem  6282  xpcomco  6330  fidceq  6360  ordiso2  6414  mulpipq2  6526  genipv  6664  genpelxp  6666  addcanprleml  6769  addcanprlemu  6770  recexprlemm  6779  recexprlemdisj  6785  recexprlemloc  6786  recexprlem1ssl  6788  recexprlem1ssu  6789  cauappcvgprlemm  6800  cauappcvgprlemdisj  6806  cauappcvgprlemloc  6807  cauappcvgprlemladdru  6811  cauappcvgprlemladdrl  6812  cauappcvgprlem1  6814  cauappcvgprlem2  6815  cauappcvgprlemlim  6816  cauappcvgpr  6817  caucvgprlemnkj  6821  caucvgprlemnbj  6822  caucvgprlemm  6823  caucvgprlemdisj  6829  caucvgprlemloc  6830  caucvgprlemcl  6831  caucvgprlemladdfu  6832  caucvgprlemladdrl  6833  caucvgprlem1  6834  caucvgprlem2  6835  caucvgpr  6837  caucvgprprlemell  6840  caucvgprprlemelu  6841  caucvgprprlemcbv  6842  caucvgprprlemval  6843  caucvgprprlemnkeqj  6845  caucvgprprlemnbj  6848  caucvgprprlemml  6849  caucvgprprlemmu  6850  caucvgprprlemopl  6852  caucvgprprlemlol  6853  caucvgprprlemopu  6854  caucvgprprlemloc  6858  caucvgprprlemclphr  6860  caucvgprprlemexbt  6861  caucvgprprlem1  6864  caucvgprprlem2  6865  caucvgsrlemcl  6930  caucvgsrlemfv  6932  caucvgsrlembound  6935  caucvgsrlemgt1  6936  caucvgsrlemoffval  6937  caucvgsrlemoffres  6941  caucvgsrlembnd  6942  caucvgsr  6943  axcaucvglemcau  7029  axcaucvglemres  7030  uz11  8590  cnref1o  8679  fzprval  9045  fztpval  9046  frec2uzzd  9349  frec2uzuzd  9351  frec2uzltd  9352  frec2uzlt2d  9353  frecuzrdgrrn  9357  frec2uzrdg  9358  frecuzrdgfn  9361  frecfzennn  9366  iseqeq1  9377  iseqovex  9382  iseqval  9383  iseqfn  9384  iseq1  9385  iseqcl  9386  iseqp1  9388  iseqss  9389  iseqfveq2  9391  iseqfveq  9393  iseqfeq  9394  iseqshft2  9395  monoord  9398  monoord2  9399  isermono  9400  iseqsplit  9401  iseqcaopr3  9403  iseqcaopr2  9404  iseqid3s  9409  iseqhomo  9411  iseqz  9412  serile  9417  expivallem  9420  expival  9421  facp1  9597  faccl  9602  facdiv  9605  facwordi  9607  faclbnd  9608  facubnd  9612  bcval  9616  ibcval5  9630  reval  9676  replim  9686  cj11  9732  caucvgre  9807  cvg1nlemcau  9810  cvg1nlemres  9811  rexuz3  9816  absval  9827  resqrexlemover  9836  resqrexlemdecn  9838  resqrexlemlo  9839  resqrexlemcalc3  9842  resqrexlemnm  9844  resqrexlemcvg  9845  resqrexlemoverl  9847  resqrexlemglsq  9848  resqrexlemga  9849  resqrexlemsqa  9850  resqrexlemex  9851  abs00bd  9892  cau3lem  9940  caubnd2  9943  climconst  10041  climmpt  10051  climshftlemg  10053  climcn1  10059  climle  10084  climub  10094  climserile  10095  climcau  10096  climcvg1nlem  10098  climcvg1n  10099  serif0  10101  dvdsabseq  10158  dvdsfac  10171  nn0seqcvgd  10242  ialginv  10248  ialgcvg  10249  ialgcvga  10252  ialgfx  10253  qdencn  10490
  Copyright terms: Public domain W3C validator