Theorem hba1 1533

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

Step	Hyp	Ref	Expression
1		ax-ial 1527	1 ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑)

Syntax hints:   → wi 4  ∀wal 1346

This theorem was proved from axioms:  ax-ial 1527

This theorem is referenced by:  nfa1  1534  a5i  1536  hba2  1544  hbia1  1545  19.21h  1550  19.21ht  1574  exim  1592  19.12  1658  19.38  1669  ax9o  1691  equveli  1752  nfald  1753  equs5a  1787  ax11v2  1813  equs5  1822  equs5or  1823  sb56  1878  hbsb4t  2006  hbeu1  2029  eupickbi  2101  moexexdc  2103  2eu4  2112  exists2  2116  hbra1  2500