Theorem nf5i 2187

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 2186	. 2 ⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → Ⅎ𝑥𝜑)
2		nf5i.1	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3	1, 2	mpg 1824	1 ⊢ Ⅎ𝑥𝜑

Syntax hints:   → wi 4  ∀wal 1565  Ⅎwnf 1810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-10 2182

This theorem depends on definitions:  df-bi 210  df-ex 1807  df-nf 1811

This theorem is referenced by:  nfnaew  2190  nfe1  2191  sbh  2314  nf5di  2326  19.9h  2327  19.21h  2328  19.23h  2329  exlimih  2330  exlimdh  2331  equsalhw  2332  equsexhv  2333  hban  2341  hb3an  2342  nfal  2362  hbex  2364  nfsbv  2369  cbv3hv  2378  dvelimhw  2383  cbv3h  2442  equsalh  2458  equsexh  2459  nfae  2471  axc16i  2474  dvelimh  2488  nfs1  2526  hbsb  2562  sb7h  2564  nfsab  2759  nfsabg  2760  cleqh  2898  nfcii  2920  nfralw  3318  bnj596  35080  bnj1146  35124  bnj1379  35163  bnj1464  35177  bnj1468  35179  bnj605  35240  bnj607  35249  bnj916  35266  bnj964  35276  bnj981  35283  bnj983  35284  bnj1014  35294  bnj1123  35319  bnj1373  35363  bnj1417  35374  bnj1445  35377  bnj1463  35388  bnj1497  35393  bj-cbv3hv2  37319  bj-equsalhv  37330  bj-nfs1v  37337  bj-nfsab1  37340  bj-gabima  37464  wl-nfalv  38068  nfequid-o  39574  nfa1-o  39579  nfalh  42873  2sb5ndVD  45510  2sb5ndALT  45532