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

Theorem hba1 1540
Description: 𝑥 is not free in 𝑥𝜑. Example in Appendix in [Megill] p. 450 (p. 19 of the preprint). Also Lemma 22 of [Monk2] p. 114. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
hba1 (∀𝑥𝜑 → ∀𝑥𝑥𝜑)

Proof of Theorem hba1
StepHypRef Expression
1 ax-ial 1534 1 (∀𝑥𝜑 → ∀𝑥𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1351
This theorem was proved from axioms:  ax-ial 1534
This theorem is referenced by:  nfa1  1541  a5i  1543  hba2  1551  hbia1  1552  19.21h  1557  19.21ht  1581  exim  1599  19.12  1665  19.38  1676  ax9o  1698  equveli  1759  nfald  1760  equs5a  1794  ax11v2  1820  equs5  1829  equs5or  1830  sb56  1885  hbsb4t  2013  hbeu1  2036  eupickbi  2108  moexexdc  2110  2eu4  2119  exists2  2123  hbra1  2507
  Copyright terms: Public domain W3C validator