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

Theorem fveq1d 5389
Description: Equality deduction for function value. (Contributed by NM, 2-Sep-2003.)
Hypothesis
Ref Expression
fveq1d.1 (𝜑𝐹 = 𝐺)
Assertion
Ref Expression
fveq1d (𝜑 → (𝐹𝐴) = (𝐺𝐴))

Proof of Theorem fveq1d
StepHypRef Expression
1 fveq1d.1 . 2 (𝜑𝐹 = 𝐺)
2 fveq1 5386 . 2 (𝐹 = 𝐺 → (𝐹𝐴) = (𝐺𝐴))
31, 2syl 14 1 (𝜑 → (𝐹𝐴) = (𝐺𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1314  cfv 5091
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-rex 2397  df-uni 3705  df-br 3898  df-iota 5056  df-fv 5099
This theorem is referenced by:  fveq12d  5394  funssfv  5413  csbfv2g  5424  fvco4  5459  fvmptd  5468  fvmpt2d  5473  mpteqb  5477  fvmptt  5478  fmptco  5552  fvunsng  5580  fvsng  5582  fsnunfv  5587  f1ocnvfv1  5644  f1ocnvfv2  5645  fcof1  5650  fcofo  5651  ofvalg  5957  offval2  5963  ofrfval2  5964  caofinvl  5970  tfrlemi1  6195  rdg0g  6251  freceq1  6255  oav  6316  omv  6317  oeiv  6318  mapxpen  6708  xpmapenlem  6709  exmidomni  6980  fseq1p1m1  9814  seqeq3  10163  seq3f1olemqsum  10213  seq3f1olemstep  10214  seq3f1olemp  10215  seq3id  10221  seq3z  10224  exp3val  10235  bcval5  10449  bcn2  10450  seq3coll  10525  shftcan1  10546  shftcan2  10547  shftvalg  10548  shftval4g  10549  climshft2  11015  sumeq2  11068  summodc  11092  zsumdc  11093  fsum3  11096  isumz  11098  fisumss  11101  fsum3cvg2  11103  isumsplit  11200  fvsetsid  11888  setsslid  11904  setsslnid  11905  ntrval  12174  clsval  12175  neival  12207  cnpval  12262  txmetcnp  12582  metcnpd  12584  limccl  12671  ellimc3apf  12672  cnplimclemr  12681  limccnp2cntop  12689  dvfvalap  12693  dvfre  12717  peano4nninf  13002
  Copyright terms: Public domain W3C validator