Theorem nf5i 2146

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

Syntax hints:   → wi 4  ∀wal 1535  Ⅎwnf 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-10 2141

This theorem depends on definitions:  df-bi 207  df-ex 1778  df-nf 1782

This theorem is referenced by:  nfnaew  2149  nfnaewOLD  2150  nfe1  2151  sbh  2274  nf5di  2289  19.9h  2290  19.21h  2291  19.23h  2292  exlimih  2293  exlimdh  2294  equsalhw  2295  equsexhv  2296  hban  2304  hb3an  2305  nfal  2327  hbex  2329  nfsbv  2334  cbv3hv  2346  dvelimhw  2351  cbv3h  2412  equsalh  2428  equsexh  2429  nfae  2441  axc16i  2444  dvelimh  2458  nfs1  2496  hbsb  2532  sb7h  2534  nfsab  2730  nfsabg  2731  cleqh  2874  nfcii  2897  nfralw  3317  bnj596  34722  bnj1146  34767  bnj1379  34806  bnj1464  34820  bnj1468  34822  bnj605  34883  bnj607  34892  bnj916  34909  bnj964  34919  bnj981  34926  bnj983  34927  bnj1014  34937  bnj1123  34962  bnj1373  35006  bnj1417  35017  bnj1445  35020  bnj1463  35031  bnj1497  35036  bj-cbv3hv2  36761  bj-equsalhv  36772  bj-nfs1v  36779  bj-nfsab1  36782  bj-gabima  36906  wl-nfalv  37479  nfequid-o  38866  nfa1-o  38871  2sb5ndVD  44881  2sb5ndALT  44903