Theorem nfi 1515

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

Syntax hints:   → wi 4  ∀wal 1400  Ⅎwnf 1513

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 1502

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

This theorem is referenced by:  nfth  1517  nfnth  1518  nfe1  1549  nfdh  1577  nfv  1581  nfa1  1594  nfan1  1617  nfim1  1624  nfor  1627  nfex  1690  nfae  1771  cbv3h  1796  nfs1  1862  nfs1v  1999  hbsb  2009  sbco2h  2024  hbsbd  2042  dvelimALT  2070  dvelimfv  2071  hbeu  2107  hbeud  2108  eu3h  2132  mo3h  2140  nfsab1  2228  nfsab  2230  nfcii  2383  nfcri  2386