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

Theorem fveq12d 5501
Description: Equality deduction for function value. (Contributed by FL, 22-Dec-2008.)
Hypotheses
Ref Expression
fveq12d.1  |-  ( ph  ->  F  =  G )
fveq12d.2  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
fveq12d  |-  ( ph  ->  ( F `  A
)  =  ( G `
 B ) )

Proof of Theorem fveq12d
StepHypRef Expression
1 fveq12d.1 . . 3  |-  ( ph  ->  F  =  G )
21fveq1d 5496 . 2  |-  ( ph  ->  ( F `  A
)  =  ( G `
 A ) )
3 fveq12d.2 . . 3  |-  ( ph  ->  A  =  B )
43fveq2d 5498 . 2  |-  ( ph  ->  ( G `  A
)  =  ( G `
 B ) )
52, 4eqtrd 2203 1  |-  ( ph  ->  ( F `  A
)  =  ( G `
 B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1348   ` cfv 5196
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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rex 2454  df-v 2732  df-un 3125  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-br 3988  df-iota 5158  df-fv 5204
This theorem is referenced by:  nffvd  5506  fvsng  5690  tfrlem3ag  6286  tfrlem3a  6287  tfrlemi1  6309  tfr1onlem3ag  6314  omp1eomlem  7068  seq3shft  10791  climshft2  11258  fsum3  11339  ctiunctlemfo  12383  reldvg  13403  dvfvalap  13405  lgsval  13660  lgsneg  13680
  Copyright terms: Public domain W3C validator