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  2279  nf5di  2291  19.9h  2292  19.21h  2293  19.23h  2294  exlimih  2295  exlimdh  2296  equsalhw  2297  equsexhv  2298  hban  2306  hb3an  2307  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  3283  bnj596  34902  bnj1146  34947  bnj1379  34986  bnj1464  35000  bnj1468  35002  bnj605  35063  bnj607  35072  bnj916  35089  bnj964  35099  bnj981  35106  bnj983  35107  bnj1014  35117  bnj1123  35142  bnj1373  35186  bnj1417  35197  bnj1445  35200  bnj1463  35211  bnj1497  35216  bj-cbv3hv2  36996  bj-equsalhv  37007  bj-nfs1v  37014  bj-nfsab1  37017  bj-gabima  37141  wl-nfalv  37730  nfequid-o  39170  nfa1-o  39175  nfalh  42468  2sb5ndVD  45150  2sb5ndALT  45172