Theorem nfi 1510

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

Syntax hints:   → wi 4  ∀wal 1395  Ⅎwnf 1508

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 1497

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

This theorem is referenced by:  nfth  1512  nfnth  1513  nfe1  1544  nfdh  1572  nfv  1576  nfa1  1589  nfan1  1612  nfim1  1619  nfor  1622  nfex  1685  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  2365  nfcri  2368