Theorem nf5i 2180

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

Syntax hints:   → wi 4  ∀wal 1558  Ⅎwnf 1803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-10 2175

This theorem depends on definitions:  df-bi 209  df-ex 1800  df-nf 1804

This theorem is referenced by:  nfnaew  2183  nfe1  2184  sbh  2307  nf5di  2319  19.9h  2320  19.21h  2321  19.23h  2322  exlimih  2323  exlimdh  2324  equsalhw  2325  equsexhv  2326  hban  2334  hb3an  2335  nfal  2355  hbex  2357  nfsbv  2362  cbv3hv  2371  dvelimhw  2376  cbv3h  2435  equsalh  2451  equsexh  2452  nfae  2464  axc16i  2467  dvelimh  2481  nfs1  2519  hbsb  2555  sb7h  2557  nfsab  2752  nfsabg  2753  cleqh  2891  nfcii  2913  nfralw  3309  bnj596  35042  bnj1146  35086  bnj1379  35125  bnj1464  35139  bnj1468  35141  bnj605  35202  bnj607  35211  bnj916  35228  bnj964  35238  bnj981  35245  bnj983  35246  bnj1014  35256  bnj1123  35281  bnj1373  35325  bnj1417  35336  bnj1445  35339  bnj1463  35350  bnj1497  35355  bj-cbv3hv2  37280  bj-equsalhv  37291  bj-nfs1v  37298  bj-nfsab1  37301  bj-gabima  37425  wl-nfalv  38028  nfequid-o  39534  nfa1-o  39539  nfalh  42831  2sb5ndVD  45485  2sb5ndALT  45507