Theorem nfi 1327

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

Syntax hints:   → wi 4  ∀wal 1224  Ⅎwnf 1325

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 1314

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

This theorem is referenced by:  nfth  1329  nfnth  1330  nfe1  1362  nfdh  1394  nfv  1398  nfa1  1412  nfan1  1434  nfim1  1441  nfor  1444  nfal  1446  nfex  1506  nfae  1585  cbv3h  1609  nfs1  1668  nfs1v  1793  hbsb  1801  sbco2h  1816  hbsbd  1836  dvelimALT  1864  dvelimfv  1865  hbeu  1899  hbeud  1900  eu3h  1923  mo3h  1931  nfsab1  2008  nfsab  2010  nfcii  2147  nfcri  2150