Theorem nf5i 2152

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

Syntax hints:   → wi 4  ∀wal 1540  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-10 2147

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

This theorem is referenced by:  nfnaew  2155  nfe1  2156  sbh  2280  nf5di  2292  19.9h  2293  19.21h  2294  19.23h  2295  exlimih  2296  exlimdh  2297  equsalhw  2298  equsexhv  2299  hban  2307  hb3an  2308  nfal  2328  hbex  2330  nfsbv  2335  cbv3hv  2344  dvelimhw  2349  cbv3h  2408  equsalh  2424  equsexh  2425  nfae  2437  axc16i  2440  dvelimh  2454  nfs1  2492  hbsb  2528  sb7h  2530  nfsab  2726  nfsabg  2727  cleqh  2865  nfcii  2887  nfralw  3284  bnj596  34889  bnj1146  34933  bnj1379  34972  bnj1464  34986  bnj1468  34988  bnj605  35049  bnj607  35058  bnj916  35075  bnj964  35085  bnj981  35092  bnj983  35093  bnj1014  35103  bnj1123  35128  bnj1373  35172  bnj1417  35183  bnj1445  35186  bnj1463  35197  bnj1497  35202  bj-cbv3hv2  37102  bj-equsalhv  37113  bj-nfs1v  37120  bj-nfsab1  37123  bj-gabima  37247  wl-nfalv  37850  nfequid-o  39356  nfa1-o  39361  nfalh  42653  2sb5ndVD  45336  2sb5ndALT  45358