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

Theorem fveq2i 5181
Description: Equality inference for function value. (Contributed by NM, 28-Jul-1999.)
Hypothesis
Ref Expression
fveq2i.1 𝐴 = 𝐵
Assertion
Ref Expression
fveq2i (𝐹𝐴) = (𝐹𝐵)

Proof of Theorem fveq2i
StepHypRef Expression
1 fveq2i.1 . 2 𝐴 = 𝐵
2 fveq2 5178 . 2 (𝐴 = 𝐵 → (𝐹𝐴) = (𝐹𝐵))
31, 2ax-mp 7 1 (𝐹𝐴) = (𝐹𝐵)
Colors of variables: wff set class
Syntax hints:   = wceq 1243  cfv 4902
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 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-rex 2312  df-v 2559  df-un 2922  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-br 3765  df-iota 4867  df-fv 4910
This theorem is referenced by:  fveq12i  5183  ot1stg  5779  ot2ndg  5780  ot3rdgg  5781  algrflem  5850  tfr2a  5936  tfr0  5937  1prl  6653  1pru  6654  ltexprlemell  6696  ltexprlemelu  6697  recexprlemell  6720  recexprlemelu  6721  cauappcvgprlemm  6743  cauappcvgprlemopl  6744  cauappcvgprlemlol  6745  cauappcvgprlemopu  6746  cauappcvgprlemupu  6747  cauappcvgprlemdisj  6749  cauappcvgprlemloc  6750  cauappcvgprlemladdfu  6752  cauappcvgprlemladdfl  6753  cauappcvgprlemladdru  6754  cauappcvgprlem2  6758  caucvgprlemm  6766  caucvgprlemopl  6767  caucvgprlemlol  6768  caucvgprlemopu  6769  caucvgprlemupu  6770  caucvgprlemdisj  6772  caucvgprlemloc  6773  caucvgprlemladdfu  6775  caucvgprlem2  6778  caucvgprprlemell  6783  caucvgprprlemelu  6784  caucvgprprlemml  6792  caucvgprprlemmu  6793  caucvgprprlemexbt  6804  caucvgprprlem2  6808  caucvgsr  6886  axcaucvg  6974  fseq1p1m1  8956  rebtwn2zlemstep  9107  rebtwn2z  9109  fldiv4p1lem1div2  9147  frec2uzzd  9186  frec2uzsucd  9187  frec2uzrdg  9195  frecuzrdgsuc  9201  frecfzennn  9203  rei  9499  imi  9500  sqrt1  9644  sqrt4  9645  sqrt9  9646  abs0  9656  absi  9657  ialgrp1  9885  ex-ceil  9896
  Copyright terms: Public domain W3C validator