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

Theorem fveq2i 5292
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 5289 . 2 (𝐴 = 𝐵 → (𝐹𝐴) = (𝐹𝐵))
31, 2ax-mp 7 1 (𝐹𝐴) = (𝐹𝐵)
Colors of variables: wff set class
Syntax hints:   = wceq 1289  cfv 5002
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 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-rex 2365  df-v 2621  df-un 3001  df-sn 3447  df-pr 3448  df-op 3450  df-uni 3649  df-br 3838  df-iota 4967  df-fv 5010
This theorem is referenced by:  fveq12i  5295  ot1stg  5905  ot2ndg  5906  ot3rdgg  5907  algrflem  5976  tfr2a  6068  tfr0dm  6069  tfr0  6070  infisoti  6706  1prl  7093  1pru  7094  ltexprlemell  7136  ltexprlemelu  7137  recexprlemell  7160  recexprlemelu  7161  cauappcvgprlemm  7183  cauappcvgprlemopl  7184  cauappcvgprlemlol  7185  cauappcvgprlemopu  7186  cauappcvgprlemupu  7187  cauappcvgprlemdisj  7189  cauappcvgprlemloc  7190  cauappcvgprlemladdfu  7192  cauappcvgprlemladdfl  7193  cauappcvgprlemladdru  7194  cauappcvgprlem2  7198  caucvgprlemm  7206  caucvgprlemopl  7207  caucvgprlemlol  7208  caucvgprlemopu  7209  caucvgprlemupu  7210  caucvgprlemdisj  7212  caucvgprlemloc  7213  caucvgprlemladdfu  7215  caucvgprlem2  7218  caucvgprprlemell  7223  caucvgprprlemelu  7224  caucvgprprlemml  7232  caucvgprprlemmu  7233  caucvgprprlemexbt  7244  caucvgprprlem2  7248  caucvgsr  7326  axcaucvg  7414  infrenegsupex  9051  fseq1p1m1  9475  rebtwn2zlemstep  9629  rebtwn2z  9631  fldiv4p1lem1div2  9677  frec2uzsucd  9773  frec2uzrdg  9781  frecuzrdgsuc  9786  frecuzrdgg  9788  frecuzrdgsuctlem  9795  frecfzennn  9798  0tonninf  9810  1tonninf  9811  iseqvalt  9838  seq3val  9839  facp1  10103  fac2  10104  fac3  10105  fac4  10106  4bc2eq6  10147  fihasheq0  10167  hashprg  10181  hashp1i  10183  pr0hash2ex  10188  hashfzo  10195  hashxp  10199  zfz1isolemsplit  10208  rei  10298  imi  10299  sqrt1  10444  sqrt4  10445  sqrt9  10446  abs0  10456  absi  10457  fsumabs  10822  fsumrelem  10828  hashrabrex  10837  hashuni  10838  isumnn0nn  10849  ialgrp1  11121  eucialg  11134  prmind2  11195  dfphi2  11289  phiprmpw  11291  phimullem  11294  ex-ceil  11310  ex-fac  11312  nninfsellemqall  11564  nninfomni  11568
  Copyright terms: Public domain W3C validator