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

Theorem fveq2 5103
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 3741 . . 3 (A = B → (A𝐹xB𝐹x))
21iotabidv 4815 . 2 (A = B → (℩xA𝐹x) = (℩xB𝐹x))
3 df-fv 4837 . 2 (𝐹A) = (℩xA𝐹x)
4 df-fv 4837 . 2 (𝐹B) = (℩xB𝐹x)
52, 3, 43eqtr4g 2079 1 (A = B → (𝐹A) = (𝐹B))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1228   class class class wbr 3738  cio 4792  cfv 4829
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 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-3an 875  df-tru 1231  df-nf 1330  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-rex 2290  df-v 2537  df-un 2899  df-sn 3356  df-pr 3357  df-op 3359  df-uni 3555  df-br 3739  df-iota 4794  df-fv 4837
This theorem is referenced by:  fveq2i  5106  fveq2d  5107  dffn5imf  5153  fvelimab  5154  ssimaex  5159  fvmptssdm  5180  fvmptf  5188  eqfnfv2f  5194  fvelrn  5223  ralrnmpt  5234  rexrnmpt  5235  foco2  5243  ffnfvf  5249  fmptco  5255  fcompt  5258  fcoconst  5259  fnressn  5274  fressnfv  5275  fconstfvm  5304  funiunfvdmf  5328  f1veqaeq  5333  dff13f  5334  f1fveq  5336  f1elima  5337  f1ocnvfv  5344  f1ocnvfvb  5345  fcofo  5349  cocan2  5353  fliftfun  5361  isorel  5373  isocnv  5376  isotr  5381  f1oiso2  5391  ffnov  5528  eqfnov  5530  fnovim  5532  fnrnov  5569  foov  5570  funimassov  5573  ovelimab  5574  suppssfv  5631  fnofval  5644  ofrval  5645  offval2  5649  ofrfval2  5650  ofco  5652  caofinvl  5656  op1std  5698  op2ndd  5699  1stval2  5705  2ndval2  5706  unielxp  5723  reldm  5735  oprabco  5761  2ndconst  5766  f1o2ndf1  5772  mpt2xopn0yelv  5776  mpt2xopoveq  5777  smoel  5837  tfrlem1  5845  tfrlem3-2  5849  tfrlem3-2d  5850  tfrlem5  5852  tfrlem9  5857  tfrlemiubacc  5865  tfrlemi1  5867  tfrexlem  5870  tfri3  5875  rdgss  5890  rdgisuc1  5891  rdgisucinc  5892  rdgon  5893  frecsuclem3  5906  frecsuc  5907  frecrdg  5908  oav  5949  omv  5950  oeiv  5951  mulpipq2  6230  genipv  6363  genpelxp  6365  genpelpw  6371  addcanprleml  6451  addcanprlemu  6452  recexprlemm  6458  recexprlemdisj  6464  recexprlemloc  6465  recexprlem1ssl  6467  recexprlem1ssu  6468
  Copyright terms: Public domain W3C validator