Theorem nf5i 2151

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

Syntax hints:   → wi 4  ∀wal 1539  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-10 2146

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfnaew  2154  nfe1  2155  sbh  2277  nf5di  2289  19.9h  2290  19.21h  2291  19.23h  2292  exlimih  2293  exlimdh  2294  equsalhw  2295  equsexhv  2296  hban  2304  hb3an  2305  nfal  2326  hbex  2328  nfsbv  2333  cbv3hv  2342  dvelimhw  2347  cbv3h  2406  equsalh  2422  equsexh  2423  nfae  2435  axc16i  2438  dvelimh  2452  nfs1  2490  hbsb  2526  sb7h  2528  nfsab  2724  nfsabg  2725  cleqh  2863  nfcii  2885  nfralw  3281  bnj596  34851  bnj1146  34896  bnj1379  34935  bnj1464  34949  bnj1468  34951  bnj605  35012  bnj607  35021  bnj916  35038  bnj964  35048  bnj981  35055  bnj983  35056  bnj1014  35066  bnj1123  35091  bnj1373  35135  bnj1417  35146  bnj1445  35149  bnj1463  35160  bnj1497  35165  bj-cbv3hv2  36939  bj-equsalhv  36950  bj-nfs1v  36957  bj-nfsab1  36960  bj-gabima  37084  wl-nfalv  37669  nfequid-o  39109  nfa1-o  39114  nfalh  42408  2sb5ndVD  45092  2sb5ndALT  45114