NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  hbth GIF version

Theorem hbth 1552
Description: No variable is (effectively) free in a theorem.

This and later "hypothesis-building" lemmas, with labels starting "hb...", allow us to construct proofs of formulas of the form (φxφ) from smaller formulas of this form. These are useful for constructing hypotheses that state "x is (effectively) not free in φ." (Contributed by NM, 5-Aug-1993.)

Hypothesis
Ref Expression
hbth.1 φ
Assertion
Ref Expression
hbth (φxφ)

Proof of Theorem hbth
StepHypRef Expression
1 hbth.1 . . 3 φ
21ax-gen 1546 . 2 xφ
32a1i 10 1 (φxφ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-gen 1546
This theorem is referenced by:  nfth  1553  spfalw  1672  spimehOLD  1821
  Copyright terms: Public domain W3C validator