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  34923  bnj1146  34967  bnj1379  35006  bnj1464  35020  bnj1468  35022  bnj605  35083  bnj607  35092  bnj916  35109  bnj964  35119  bnj981  35126  bnj983  35127  bnj1014  35137  bnj1123  35162  bnj1373  35206  bnj1417  35217  bnj1445  35220  bnj1463  35231  bnj1497  35236  bj-cbv3hv2  37043  bj-equsalhv  37054  bj-nfs1v  37061  bj-nfsab1  37064  bj-gabima  37188  wl-nfalv  37780  nfequid-o  39286  nfa1-o  39291  nfalh  42584  2sb5ndVD  45265  2sb5ndALT  45287