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

Theorem fveq2 5121
Description: Equality theorem for function value. (Contributed by NM, 29-Dec-1996.)
Assertion
Ref Expression
fveq2 (A = B → (𝐹A) = (𝐹B))

Proof of Theorem fveq2
Dummy variable x is distinct from all other variables.
StepHypRef Expression
1 breq1 3758 . . 3 (A = B → (A𝐹xB𝐹x))
21iotabidv 4831 . 2 (A = B → (℩xA𝐹x) = (℩xB𝐹x))
3 df-fv 4853 . 2 (𝐹A) = (℩xA𝐹x)
4 df-fv 4853 . 2 (𝐹B) = (℩xB𝐹x)
52, 3, 43eqtr4g 2094 1 (A = B → (𝐹A) = (𝐹B))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1242   class class class wbr 3755  cio 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-bnd 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  6491  genpelxp  6493  addcanprleml  6587  addcanprlemu  6588  recexprlemm  6595  recexprlemdisj  6601  recexprlemloc  6602  recexprlem1ssl  6604  recexprlem1ssu  6605  cauappcvgprlemm  6616  cauappcvgprlemdisj  6622  cauappcvgprlemloc  6623  cauappcvgprlemladdru  6627  cauappcvgprlemladdrl  6628  cauappcvgprlem1  6630  cauappcvgprlem2  6631  cauappcvgprlemlim  6632  cauappcvgpr  6633  uz11  8251  cnref1o  8337  fzprval  8694  fztpval  8695  frec2uzzd  8847  frec2uzuzd  8849  frec2uzltd  8850  frec2uzlt2d  8851  frecuzrdgrrn  8855  frec2uzrdg  8856  frecuzrdgfn  8859  frecfzennn  8864  iseqeq1  8874  iseqovex  8879  iseqval  8880  iseqfn  8881  iseq1  8882  iseqcl  8883  iseqp1  8884  iseqfveq2  8885  iseqfveq  8887  expivallem  8890  expival  8891  reval  9057  replim  9067  cj11  9113  absval  9190  abs00bd  9204
  Copyright terms: Public domain W3C validator