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

Theorem fveq2 5121
Description: Equality theorem for function value. (Contributed by NM, 29-Dec-1996.)
Assertion
Ref Expression
fveq2  F `  F `

Proof of Theorem fveq2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 breq1 3758 . . 3  F  F
21iotabidv 4831 . 2  iota F  iota F
3 df-fv 4853 . 2  F `
 iota F
4 df-fv 4853 . 2  F `
 iota F
52, 3, 43eqtr4g 2094 1  F `  F `
Colors of variables: wff set class
Syntax hints:   wi 4   wceq 1242   class class class wbr 3755   iotacio 4808   ` cfv 4845
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-rex 2306  df-v 2553  df-un 2916  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-iota 4810  df-fv 4853
This theorem is referenced by:  fveq2i  5124  fveq2d  5125  dffn5imf  5171  fvelimab  5172  ssimaex  5177  fvmptssdm  5198  fvmptf  5206  eqfnfv2f  5212  fvelrn  5241  ralrnmpt  5252  rexrnmpt  5253  foco2  5261  ffnfvf  5267  fmptco  5273  fcompt  5276  fcoconst  5277  fnressn  5292  fressnfv  5293  fconstfvm  5322  funiunfvdmf  5346  f1veqaeq  5351  dff13f  5352  f1fveq  5354  f1elima  5355  f1ocnvfv  5362  f1ocnvfvb  5363  fcofo  5367  cocan2  5371  fliftfun  5379  isorel  5391  isocnv  5394  isotr  5399  f1oiso2  5409  ffnov  5547  eqfnov  5549  fnovim  5551  fnrnov  5588  foov  5589  funimassov  5592  ovelimab  5593  suppssfv  5650  fnofval  5663  ofrval  5664  offval2  5668  ofrfval2  5669  ofco  5671  caofinvl  5675  op1std  5717  op2ndd  5718  1stval2  5724  2ndval2  5725  unielxp  5742  reldm  5754  oprabco  5780  2ndconst  5785  f1o2ndf1  5791  mpt2xopn0yelv  5795  mpt2xopoveq  5796  smoel  5856  tfrlem1  5864  tfrlem3-2  5868  tfrlem3-2d  5869  tfrlem5  5871  tfrlem9  5876  tfr0  5878  tfrlemiubacc  5885  tfrlemi1  5887  tfrexlem  5889  tfri3  5894  rdgtfr  5901  rdgss  5910  rdgisuc1  5911  rdgisucinc  5912  rdgon  5913  frecabex  5923  frecsuclem3  5929  frecsuc  5930  frecrdg  5931  freccl  5932  oav  5973  omv  5974  oeiv  5975  dom2lem  6188  xpcomco  6236  mulpipq2  6355  genipv  6492  genpelxp  6494  addcanprleml  6588  addcanprlemu  6589  recexprlemm  6596  recexprlemdisj  6602  recexprlemloc  6603  recexprlem1ssl  6605  recexprlem1ssu  6606  cauappcvgprlemm  6617  cauappcvgprlemdisj  6623  cauappcvgprlemloc  6624  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  cauappcvgprlem1  6631  cauappcvgprlem2  6632  cauappcvgprlemlim  6633  cauappcvgpr  6634  caucvgprlemnkj  6637  caucvgprlemnbj  6638  caucvgprlemm  6639  caucvgprlemdisj  6645  caucvgprlemloc  6646  caucvgprlemcl  6647  caucvgprlemladdfu  6648  caucvgprlemladdrl  6649  caucvgprlem1  6650  caucvgprlem2  6651  caucvgpr  6653  uz11  8271  cnref1o  8357  fzprval  8714  fztpval  8715  frec2uzzd  8867  frec2uzuzd  8869  frec2uzltd  8870  frec2uzlt2d  8871  frecuzrdgrrn  8875  frec2uzrdg  8876  frecuzrdgfn  8879  frecfzennn  8884  iseqeq1  8894  iseqovex  8899  iseqval  8900  iseqfn  8901  iseq1  8902  iseqcl  8903  iseqp1  8904  iseqfveq2  8905  iseqfveq  8907  expivallem  8910  expival  8911  reval  9077  replim  9087  cj11  9133  absval  9210  abs00bd  9224
  Copyright terms: Public domain W3C validator