Theorem nf5i 2152

Description: Deduce that 𝑥 is not free in 𝜑 from the definition. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypothesis

Ref	Expression
nf5i.1	⊢ (𝜑 → ∀𝑥𝜑)

Assertion

Ref	Expression
nf5i	⊢ Ⅎ𝑥𝜑

Proof of Theorem nf5i

Step	Hyp	Ref	Expression
1		nf5-1 2151	. 2 ⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → Ⅎ𝑥𝜑)
2		nf5i.1	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3	1, 2	mpg 1799	1 ⊢ Ⅎ𝑥𝜑

Syntax hints:   → wi 4  ∀wal 1540  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-10 2147

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfnaew  2155  nfe1  2156  sbh  2280  nf5di  2292  19.9h  2293  19.21h  2294  19.23h  2295  exlimih  2296  exlimdh  2297  equsalhw  2298  equsexhv  2299  hban  2307  hb3an  2308  nfal  2329  hbex  2331  nfsbv  2336  cbv3hv  2345  dvelimhw  2350  cbv3h  2409  equsalh  2425  equsexh  2426  nfae  2438  axc16i  2441  dvelimh  2455  nfs1  2493  hbsb  2529  sb7h  2531  nfsab  2727  nfsabg  2728  cleqh  2866  nfcii  2888  nfralw  3285  bnj596  34908  bnj1146  34952  bnj1379  34991  bnj1464  35005  bnj1468  35007  bnj605  35068  bnj607  35077  bnj916  35094  bnj964  35104  bnj981  35111  bnj983  35112  bnj1014  35122  bnj1123  35147  bnj1373  35191  bnj1417  35202  bnj1445  35205  bnj1463  35216  bnj1497  35221  bj-cbv3hv2  37121  bj-equsalhv  37132  bj-nfs1v  37139  bj-nfsab1  37142  bj-gabima  37266  wl-nfalv  37867  nfequid-o  39373  nfa1-o  39378  nfalh  42670  2sb5ndVD  45357  2sb5ndALT  45379