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

Theorem fveq1i 5388
Description: Equality inference for function value. (Contributed by NM, 2-Sep-2003.)
Hypothesis
Ref Expression
fveq1i.1 𝐹 = 𝐺
Assertion
Ref Expression
fveq1i (𝐹𝐴) = (𝐺𝐴)

Proof of Theorem fveq1i
StepHypRef Expression
1 fveq1i.1 . 2 𝐹 = 𝐺
2 fveq1 5386 . 2 (𝐹 = 𝐺 → (𝐹𝐴) = (𝐺𝐴))
31, 2ax-mp 5 1 (𝐹𝐴) = (𝐺𝐴)
Colors of variables: wff set class
Syntax hints:   = 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:  fveq12i  5393  fvun2  5454  fvopab3ig  5461  fvsnun1  5583  fvsnun2  5584  fvpr1  5590  fvpr2  5591  fvpr1g  5592  fvpr2g  5593  fvtp1g  5594  fvtp2g  5595  fvtp3g  5596  fvtp2  5598  fvtp3  5599  ov  5856  ovigg  5857  ovg  5875  tfr2a  6184  tfrex  6231  frec0g  6260  freccllem  6265  frecsuclem  6269  caseinl  6942  caseinr  6943  ctssdccl  6962  addpiord  7088  mulpiord  7089  fseq1p1m1  9825  frec2uz0d  10123  frec2uzzd  10124  frec2uzsucd  10125  frecuzrdgrrn  10132  frec2uzrdg  10133  frecuzrdg0  10137  frecuzrdgsuc  10138  frecuzrdgg  10140  frecuzrdg0t  10146  frecuzrdgsuctlem  10147  0tonninf  10163  1tonninf  10164  inftonninf  10165  seq3val  10182  seqvalcd  10183  hashinfom  10475  hashennn  10477  hashfz1  10480  shftidt  10556  resqrexlemf1  10731  resqrexlemfp1  10732  cbvsum  11080  fisumss  11112  fsumadd  11126  isumclim3  11143  ialgr0  11632  algrp1  11634  ennnfonelem0  11824  ennnfonelemp1  11825  ennnfonelemom  11827  ctinfomlemom  11846  ndxarg  11888  strslfv2d  11907  upxp  12347  cnmetdval  12604  remetdval  12614
  Copyright terms: Public domain W3C validator