Theorem nfi 1348

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 1347	. 2 ⊢ (Ⅎxφ ↔ ∀x(φ → ∀xφ))
2		nfi.1	. 2 ⊢ (φ → ∀xφ)
3	1, 2	mpgbir 1339	1 ⊢ Ⅎxφ

Syntax hints:   → wi 4  ∀wal 1240  Ⅎwnf 1346

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1335

This theorem depends on definitions:  df-bi 110  df-nf 1347

This theorem is referenced by:  nfth  1350  nfnth  1351  nfe1  1382  nfdh  1414  nfv  1418  nfa1  1431  nfan1  1453  nfim1  1460  nfor  1463  nfal  1465  nfex  1525  nfae  1604  cbv3h  1628  nfs1  1687  nfs1v  1812  hbsb  1820  sbco2h  1835  hbsbd  1855  dvelimALT  1883  dvelimfv  1884  hbeu  1918  hbeud  1919  eu3h  1942  mo3h  1950  nfsab1  2027  nfsab  2029  nfcii  2166  nfcri  2169