Theorem nfi 1551

Description: Deduce that x is not free in φ from the definition. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypothesis

Ref	Expression
nfi.1	⊢ (φ → ∀xφ)

Assertion

Ref	Expression
nfi	⊢ Ⅎxφ

Proof of Theorem nfi

Step	Hyp	Ref	Expression
1		df-nf 1545	. 2 ⊢ (Ⅎxφ ↔ ∀x(φ → ∀xφ))
2		nfi.1	. 2 ⊢ (φ → ∀xφ)
3	1, 2	mpgbir 1550	1 ⊢ Ⅎxφ

Syntax hints:   → wi 4  ∀wal 1540  Ⅎwnf 1544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546

This theorem depends on definitions:  df-bi 177  df-nf 1545

This theorem is referenced by:  nfth  1553  nfnth  1556  nfv  1619  nfe1  1732  nfdh  1767  19.9h  1780  nfa1  1788  19.21h  1797  19.23h  1802  exlimih  1804  exlimdh  1807  nfim1  1811  nfim1OLD  1812  hban  1828  hb3an  1830  nfal  1842  nfex  1843  nfan1  1881  nfae  1954  equsalh  1961  equsexh  1963  sbh  2027  nfs1  2044  ax16i  2046  nfs1v  2106  hbsb  2110  sb7h  2121  nfequid-o  2161  nfa1-o  2166  nfsab1  2343  nfsab  2345  nfcii  2481  nfcri  2484