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

Theorem fveq2i 5392
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 5389 . 2 (𝐴 = 𝐵 → (𝐹𝐴) = (𝐹𝐵))
31, 2ax-mp 5 1 (𝐹𝐴) = (𝐹𝐵)
Colors of variables: wff set class
Syntax hints:   = wceq 1316  cfv 5093
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 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-3an 949  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-rex 2399  df-v 2662  df-un 3045  df-sn 3503  df-pr 3504  df-op 3506  df-uni 3707  df-br 3900  df-iota 5058  df-fv 5101
This theorem is referenced by:  fveq12i  5395  ot1stg  6018  ot2ndg  6019  ot3rdgg  6020  algrflem  6094  tfr2a  6186  tfr0dm  6187  tfr0  6188  infisoti  6887  1prl  7331  1pru  7332  ltexprlemell  7374  ltexprlemelu  7375  recexprlemell  7398  recexprlemelu  7399  cauappcvgprlemm  7421  cauappcvgprlemopl  7422  cauappcvgprlemlol  7423  cauappcvgprlemopu  7424  cauappcvgprlemupu  7425  cauappcvgprlemdisj  7427  cauappcvgprlemloc  7428  cauappcvgprlemladdfu  7430  cauappcvgprlemladdfl  7431  cauappcvgprlemladdru  7432  cauappcvgprlem2  7436  caucvgprlemm  7444  caucvgprlemopl  7445  caucvgprlemlol  7446  caucvgprlemopu  7447  caucvgprlemupu  7448  caucvgprlemdisj  7450  caucvgprlemloc  7451  caucvgprlemladdfu  7453  caucvgprlem2  7456  caucvgprprlemell  7461  caucvgprprlemelu  7462  caucvgprprlemml  7470  caucvgprprlemmu  7471  caucvgprprlemexbt  7482  caucvgprprlem2  7486  suplocexprlem2b  7490  suplocexprlemlub  7500  caucvgsr  7578  axcaucvg  7676  infrenegsupex  9357  fseq1p1m1  9842  rebtwn2zlemstep  9998  rebtwn2z  10000  fldiv4p1lem1div2  10046  frec2uzsucd  10142  frec2uzrdg  10150  frecuzrdgsuc  10155  frecuzrdgg  10157  frecuzrdgsuctlem  10164  frecfzennn  10167  0tonninf  10180  1tonninf  10181  seq3val  10199  seqvalcd  10200  facp1  10444  fac2  10445  fac3  10446  fac4  10447  4bc2eq6  10488  fihasheq0  10508  hashprg  10522  hashp1i  10524  pr0hash2ex  10529  hashfzo  10536  hashxp  10540  zfz1isolemsplit  10549  rei  10639  imi  10640  sqrt1  10786  sqrt4  10787  sqrt9  10788  abs0  10798  absi  10799  infxrnegsupex  11000  fsumabs  11202  fsumrelem  11208  hashrabrex  11218  hashuni  11219  isumnn0nn  11230  mertenslem2  11273  ege2le3  11304  efsep  11324  efgt1p2  11328  efgt1p  11329  sin0  11363  cos0  11364  ef01bndlem  11390  cos2bnd  11394  sin4lt0  11400  eucalg  11667  prmind2  11728  dfphi2  11823  phiprmpw  11825  phimullem  11828  ennnfonelemjn  11842  ennnfonelem1  11847  ennnfonelemhf1o  11853  sn0cld  12233  txval  12351  hmeontr  12409  comet  12595  cnmetdval  12625  sinhalfpilem  12799  cospi  12808  sincos4thpi  12848  sincos6thpi  12850  sincos3rdpi  12851  sinkpi  12855  ex-ceil  12865  ex-fac  12867  nninfsellemqall  13138  nninfomni  13142  nninffeq  13143  isomninnlem  13152
  Copyright terms: Public domain W3C validator