Theorem nf5i 2183

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 2182	. 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 2178

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

This theorem is used by:  nfnaew  2186  nfe1  2187  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  2354  hbex  2356  nfsbv  2361  cbv3hv  2370  dvelimhw  2375  cbv3h  2434  equsalh  2450  equsexh  2451  nfae  2463  axc16i  2466  dvelimh  2480  nfs1  2518  hbsb  2554  sb7h  2556  nfsab  2751  nfsabg  2752  cleqh  2890  nfcii  2912  nfralw  3310  bnj596  35377  bnj1146  35421  bnj1379  35460  bnj1464  35474  bnj1468  35476  bnj605  35537  bnj607  35546  bnj916  35563  bnj964  35573  bnj981  35580  bnj983  35581  bnj1014  35591  bnj1123  35616  bnj1373  35660  bnj1417  35671  bnj1445  35674  bnj1463  35685  bnj1497  35690  bj-cbv3hv2  37707  bj-equsalhv  37718  bj-nfs1v  37725  bj-nfsab1  37728  bj-gabima  37853  wl-nfalv  38457  nfequid-o  39967  nfa1-o  39972  nfalh  43266  2sb5ndVD  45891  2sb5ndALT  45913