Theorem nfi 1396

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

Syntax hints:   → wi 4  ∀wal 1287  Ⅎwnf 1394

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

This theorem depends on definitions:  df-bi 115  df-nf 1395

This theorem is referenced by:  nfth  1398  nfnth  1399  nfe1  1430  nfdh  1462  nfv  1466  nfa1  1479  nfan1  1501  nfim1  1508  nfor  1511  nfal  1513  nfex  1573  nfae  1654  cbv3h  1678  nfs1  1737  nfs1v  1863  hbsb  1871  sbco2h  1886  hbsbd  1906  dvelimALT  1934  dvelimfv  1935  hbeu  1969  hbeud  1970  eu3h  1993  mo3h  2001  nfsab1  2078  nfsab  2080  nfcii  2219  nfcri  2222