Theorem nfi 1450

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

Syntax hints:   → wi 4  ∀wal 1341  Ⅎwnf 1448

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 1437

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

This theorem is referenced by:  nfth  1452  nfnth  1453  nfe1  1484  nfdh  1512  nfv  1516  nfa1  1529  nfan1  1552  nfim1  1559  nfor  1562  nfex  1625  nfae  1707  cbv3h  1731  nfs1  1797  nfs1v  1927  hbsb  1937  sbco2h  1952  hbsbd  1970  dvelimALT  1998  dvelimfv  1999  hbeu  2035  hbeud  2036  eu3h  2059  mo3h  2067  nfsab1  2155  nfsab  2157  nfcii  2299  nfcri  2302