Theorem nfi 1485

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

Syntax hints:   → wi 4  ∀wal 1371  Ⅎwnf 1483

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 1472

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

This theorem is referenced by:  nfth  1487  nfnth  1488  nfe1  1519  nfdh  1547  nfv  1551  nfa1  1564  nfan1  1587  nfim1  1594  nfor  1597  nfex  1660  nfae  1742  cbv3h  1766  nfs1  1832  nfs1v  1967  hbsb  1977  sbco2h  1992  hbsbd  2010  dvelimALT  2038  dvelimfv  2039  hbeu  2075  hbeud  2076  eu3h  2099  mo3h  2107  nfsab1  2195  nfsab  2197  nfcii  2339  nfcri  2342