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 1797	1 ⊢ Ⅎ𝑥𝜑

Syntax hints:   → wi 4  ∀wal 1538  Ⅎwnf 1783

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

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfnaew  2149  nfe1  2150  sbh  2273  nf5di  2285  19.9h  2286  19.21h  2287  19.23h  2288  exlimih  2289  exlimdh  2290  equsalhw  2291  equsexhv  2292  hban  2300  hb3an  2301  nfal  2323  hbex  2325  nfsbv  2330  cbv3hv  2342  dvelimhw  2347  cbv3h  2409  equsalh  2425  equsexh  2426  nfae  2438  axc16i  2441  dvelimh  2455  nfs1  2493  hbsb  2529  sb7h  2531  nfsab  2727  nfsabg  2728  cleqh  2871  nfcii  2894  nfralw  3311  bnj596  34760  bnj1146  34805  bnj1379  34844  bnj1464  34858  bnj1468  34860  bnj605  34921  bnj607  34930  bnj916  34947  bnj964  34957  bnj981  34964  bnj983  34965  bnj1014  34975  bnj1123  35000  bnj1373  35044  bnj1417  35055  bnj1445  35058  bnj1463  35069  bnj1497  35074  bj-cbv3hv2  36796  bj-equsalhv  36807  bj-nfs1v  36814  bj-nfsab1  36817  bj-gabima  36941  wl-nfalv  37526  nfequid-o  38911  nfa1-o  38916  2sb5ndVD  44930  2sb5ndALT  44952