Theorem nfi 1511

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

Syntax hints:   → wi 4  ∀wal 1396  Ⅎwnf 1509

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 1498

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

This theorem is referenced by:  nfth  1513  nfnth  1514  nfe1  1545  nfdh  1573  nfv  1577  nfa1  1590  nfan1  1613  nfim1  1620  nfor  1623  nfex  1686  nfae  1767  cbv3h  1791  nfs1  1857  nfs1v  1992  hbsb  2002  sbco2h  2017  hbsbd  2035  dvelimALT  2063  dvelimfv  2064  hbeu  2100  hbeud  2101  eu3h  2125  mo3h  2133  nfsab1  2221  nfsab  2223  nfcii  2366  nfcri  2369