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  1792  nfs1  1858  nfs1v  1993  hbsb  2003  sbco2h  2018  hbsbd  2036  dvelimALT  2064  dvelimfv  2065  hbeu  2101  hbeud  2102  eu3h  2126  mo3h  2134  nfsab1  2222  nfsab  2224  nfcii  2375  nfcri  2378