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  35076  bnj1146  35120  bnj1379  35159  bnj1464  35173  bnj1468  35175  bnj605  35236  bnj607  35245  bnj916  35262  bnj964  35272  bnj981  35279  bnj983  35280  bnj1014  35290  bnj1123  35315  bnj1373  35359  bnj1417  35370  bnj1445  35373  bnj1463  35384  bnj1497  35389  bj-cbv3hv2  37315  bj-equsalhv  37326  bj-nfs1v  37333  bj-nfsab1  37336  bj-gabima  37460  wl-nfalv  38063  nfequid-o  39569  nfa1-o  39574  nfalh  42868  2sb5ndVD  45505  2sb5ndALT  45527