Theorem nfi 1486

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

Hypothesis

Ref	Expression
nfi.1	⊢ (𝜑 → ∀𝑥𝜑)

Assertion

Ref	Expression
nfi	⊢ Ⅎ𝑥𝜑

Proof of Theorem nfi

Step	Hyp	Ref	Expression
1		df-nf 1485	. 2 ⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑))
2		nfi.1	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3	1, 2	mpgbir 1477	1 ⊢ Ⅎ𝑥𝜑

Syntax hints:   → wi 4  ∀wal 1371  Ⅎwnf 1484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1473

This theorem depends on definitions:  df-bi 117  df-nf 1485

This theorem is referenced by:  nfth  1488  nfnth  1489  nfe1  1520  nfdh  1548  nfv  1552  nfa1  1565  nfan1  1588  nfim1  1595  nfor  1598  nfex  1661  nfae  1743  cbv3h  1767  nfs1  1833  nfs1v  1968  hbsb  1978  sbco2h  1993  hbsbd  2011  dvelimALT  2039  dvelimfv  2040  hbeu  2076  hbeud  2077  eu3h  2101  mo3h  2109  nfsab1  2197  nfsab  2199  nfcii  2341  nfcri  2344