Theorem nfi 1351

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

Syntax hints:   → wi 4  ∀wal 1241  Ⅎwnf 1349

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1338

This theorem depends on definitions:  df-bi 110  df-nf 1350

This theorem is referenced by:  nfth  1353  nfnth  1354  nfe1  1385  nfdh  1417  nfv  1421  nfa1  1434  nfan1  1456  nfim1  1463  nfor  1466  nfal  1468  nfex  1528  nfae  1607  cbv3h  1631  nfs1  1690  nfs1v  1815  hbsb  1823  sbco2h  1838  hbsbd  1858  dvelimALT  1886  dvelimfv  1887  hbeu  1921  hbeud  1922  eu3h  1945  mo3h  1953  nfsab1  2030  nfsab  2032  nfcii  2169  nfcri  2172