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

Theorem fveq2i 5212
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 5209 . 2 (𝐴 = 𝐵 → (𝐹𝐴) = (𝐹𝐵))
31, 2ax-mp 7 1 (𝐹𝐴) = (𝐹𝐵)
Colors of variables: wff set class
Syntax hints:   = wceq 1285  cfv 4932
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-rex 2355  df-v 2604  df-un 2978  df-sn 3412  df-pr 3413  df-op 3415  df-uni 3610  df-br 3794  df-iota 4897  df-fv 4940
This theorem is referenced by:  fveq12i  5214  ot1stg  5810  ot2ndg  5811  ot3rdgg  5812  algrflem  5881  tfr2a  5970  tfr0dm  5971  tfr0  5972  infisoti  6504  1prl  6807  1pru  6808  ltexprlemell  6850  ltexprlemelu  6851  recexprlemell  6874  recexprlemelu  6875  cauappcvgprlemm  6897  cauappcvgprlemopl  6898  cauappcvgprlemlol  6899  cauappcvgprlemopu  6900  cauappcvgprlemupu  6901  cauappcvgprlemdisj  6903  cauappcvgprlemloc  6904  cauappcvgprlemladdfu  6906  cauappcvgprlemladdfl  6907  cauappcvgprlemladdru  6908  cauappcvgprlem2  6912  caucvgprlemm  6920  caucvgprlemopl  6921  caucvgprlemlol  6922  caucvgprlemopu  6923  caucvgprlemupu  6924  caucvgprlemdisj  6926  caucvgprlemloc  6927  caucvgprlemladdfu  6929  caucvgprlem2  6932  caucvgprprlemell  6937  caucvgprprlemelu  6938  caucvgprprlemml  6946  caucvgprprlemmu  6947  caucvgprprlemexbt  6958  caucvgprprlem2  6962  caucvgsr  7040  axcaucvg  7128  infrenegsupex  8763  fseq1p1m1  9187  rebtwn2zlemstep  9339  rebtwn2z  9341  fldiv4p1lem1div2  9387  frec2uzsucd  9483  frec2uzrdg  9491  frecuzrdgsuc  9496  frecuzrdgg  9498  frecuzrdgsuctlem  9505  frecfzennn  9508  iseqvalt  9532  facp1  9754  fac2  9755  fac3  9756  fac4  9757  4bc2eq6  9798  sizeeq0  9818  sizeprg  9832  sizep1i  9834  pr0size2ex  9839  rei  9924  imi  9925  sqrt1  10070  sqrt4  10071  sqrt9  10072  abs0  10082  absi  10083  ialgrp1  10572  eucialg  10585  prmind2  10646  ex-ceil  10742  ex-fac  10743
  Copyright terms: Public domain W3C validator