Theorem nfi 1455

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 1454	. 2 ⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑))
2		nfi.1	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3	1, 2	mpgbir 1446	1 ⊢ Ⅎ𝑥𝜑

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

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

This theorem depends on definitions:  df-bi 116  df-nf 1454

This theorem is referenced by:  nfth  1457  nfnth  1458  nfe1  1489  nfdh  1517  nfv  1521  nfa1  1534  nfan1  1557  nfim1  1564  nfor  1567  nfex  1630  nfae  1712  cbv3h  1736  nfs1  1802  nfs1v  1932  hbsb  1942  sbco2h  1957  hbsbd  1975  dvelimALT  2003  dvelimfv  2004  hbeu  2040  hbeud  2041  eu3h  2064  mo3h  2072  nfsab1  2160  nfsab  2162  nfcii  2303  nfcri  2306