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  2306  nf5di  2318  19.9h  2319  19.21h  2320  19.23h  2321  exlimih  2322  exlimdh  2323  equsalhw  2324  equsexhv  2325  hban  2333  hb3an  2334  nfal  2353  hbex  2355  nfsbv  2360  cbv3hv  2369  dvelimhw  2374  cbv3h  2433  equsalh  2449  equsexh  2450  nfae  2462  axc16i  2465  dvelimh  2479  nfs1  2517  hbsb  2553  sb7h  2555  nfsab  2750  nfsabg  2751  cleqh  2889  nfcii  2911  nfralw  3309  bnj596  35257  bnj1146  35301  bnj1379  35340  bnj1464  35354  bnj1468  35356  bnj605  35417  bnj607  35426  bnj916  35443  bnj964  35453  bnj981  35460  bnj983  35461  bnj1014  35471  bnj1123  35496  bnj1373  35540  bnj1417  35551  bnj1445  35554  bnj1463  35565  bnj1497  35570  bj-cbv3hv2  37539  bj-equsalhv  37550  bj-nfs1v  37557  bj-nfsab1  37560  bj-gabima  37685  wl-nfalv  38289  nfequid-o  39784  nfa1-o  39789  nfalh  43083  2sb5ndVD  45733  2sb5ndALT  45755