@MISC{SUBSTUT1.MIZ,
  AUTHOR = {Braselmann, Patrick and Koepke, Peter},
  TITLE = {Substitution in First-Order Formulas: Elementary Properties},
  NOTE = {This research was carried out within the project ``Wissensformate'' and was
             financially supported by the Mathematical Institute
             of the University of Bonn (http://www.\-wissensformate.uni-bonn.de). 
	     Preparation of the Mizar
             code was part of the first author's graduate work
             under the supervision of the second author.
The authors thank Jip Veldman for his work on the final version 
of this article.},
  SECTION1 = {Preliminaries},
  SECTION2 = {Definition and Properties of the Formula -- Substitution -- Construction},
  SECTION3 = {Definition and Properties of Substitution},
  DAY = {25},
  MONTH = {September},
  YEAR = {2004},
  ADDRESS1 = {University of Bonn},
  ADDRESS2 = {University of Bonn},
  SUMMARY = {This article is part of a series of Mizar articles
              which constitute a formal proof (of a basic version)
              of Kurt G{\"o}del's famous completeness theorem
              (K. G{\"o}del, ``Die Vollst{\"a}ndigkeit der
              Axiome des logischen Funktionenkalk{\"u}ls'',
              Monatshefte f\"ur Mathematik und Physik 37 (1930),
              349-360). The completeness theorem provides the
              theoretical basis for a uniform formalization of
              mathematics as in the Mizar project. We formalize
              first-order logic up to the completeness theorem as
              in H. D. Ebbinghaus, J. Flum, and W. Thomas,
              Mathematical Logic, 1984, Springer Verlag New York
              Inc. The present article introduces the basic
              concepts of substitution of a variable for a
              variable in a first-order formula. The contents of
              this article correspond to Chapter III par. 8,
              Definition 8.1, 8.2 of Ebbinghaus, Flum, Thomas.}}

