Theorem nfi 1438

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

Syntax hints:   → wi 4  ∀wal 1329  Ⅎwnf 1436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1425

This theorem depends on definitions:  df-bi 116  df-nf 1437

This theorem is referenced by:  nfth  1440  nfnth  1441  nfe1  1472  nfdh  1504  nfv  1508  nfa1  1521  nfan1  1543  nfim1  1550  nfor  1553  nfal  1555  nfex  1616  nfae  1697  cbv3h  1721  nfs1  1781  nfs1v  1912  hbsb  1922  sbco2h  1937  hbsbd  1957  dvelimALT  1985  dvelimfv  1986  hbeu  2020  hbeud  2021  eu3h  2044  mo3h  2052  nfsab1  2129  nfsab  2131  nfcii  2272  nfcri  2275