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

Theorem hba1 1449
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 1443 1 (∀𝑥𝜑 → ∀𝑥𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1257
This theorem was proved from axioms:  ax-ial 1443
This theorem is referenced by:  nfa1  1450  a5i  1451  hba2  1459  hbia1  1460  19.21h  1465  19.21ht  1489  exim  1506  19.12  1571  19.38  1582  ax9o  1604  equveli  1658  nfald  1659  equs5a  1691  ax11v2  1717  equs5  1726  equs5or  1727  sb56  1781  hbsb4t  1905  hbeu1  1926  eupickbi  1998  moexexdc  2000  2eu4  2009  exists2  2013  hbra1  2371
  Copyright terms: Public domain W3C validator