Theorem nf5i 2182

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1567  Ⅎwnf 1815

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-10 2177

This proof depends on definitions:  df-bi 210  df-ex 1812  df-nf 1816

This theorem is used by:  nfnaew  2185  nfe1  2186  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  35427  bnj1146  35471  bnj1379  35510  bnj1464  35524  bnj1468  35526  bnj605  35587  bnj607  35596  bnj916  35613  bnj964  35623  bnj981  35630  bnj983  35631  bnj1014  35641  bnj1123  35666  bnj1373  35710  bnj1417  35721  bnj1445  35724  bnj1463  35735  bnj1497  35740  bj-cbv3hv2  37831  bj-equsalhv  37842  bj-nfs1v  37849  bj-nfsab1  37852  bj-gabima  37977  wl-nfalv  38594  nfequid-o  40104  nfa1-o  40109  nfalh  43403  2sb5ndVD  46028  2sb5ndALT  46050