Theorem nf5i 2184

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-10 2179

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817

This theorem is used by:  nfnaew  2187  nfe1  2188  sbh  2310  nf5di  2322  19.9h  2323  19.21h  2324  19.23h  2325  exlimih  2326  exlimdh  2327  equsalhw  2328  equsexhv  2329  hban  2337  hb3an  2338  nfal  2358  hbex  2360  nfsbv  2365  cbv3hv  2374  dvelimhw  2379  cbv3h  2438  equsalh  2454  equsexh  2455  nfae  2467  axc16i  2470  dvelimh  2484  nfs1  2522  hbsb  2558  sb7h  2560  nfsab  2755  nfsabg  2756  cleqh  2894  nfcii  2916  nfralw  3314  bnj596  35202  bnj1146  35246  bnj1379  35285  bnj1464  35299  bnj1468  35301  bnj605  35362  bnj607  35371  bnj916  35388  bnj964  35398  bnj981  35405  bnj983  35406  bnj1014  35416  bnj1123  35441  bnj1373  35485  bnj1417  35496  bnj1445  35499  bnj1463  35510  bnj1497  35515  bj-cbv3hv2  37489  bj-equsalhv  37500  bj-nfs1v  37507  bj-nfsab1  37510  bj-gabima  37635  wl-nfalv  38239  nfequid-o  39744  nfa1-o  39749  nfalh  43043  2sb5ndVD  45678  2sb5ndALT  45700