Theorem nf5i 2143

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-10 2138

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787

This theorem is referenced by:  nfnaew  2146  nfnaewOLD  2147  nfe1  2148  sbh  2265  nf5di  2282  19.9h  2283  19.21h  2284  19.23h  2285  exlimih  2286  exlimdh  2287  equsalhw  2288  equsexhv  2289  hban  2297  hb3an  2298  nfal  2317  hbex  2319  nfsbv  2324  hbsbwOLD  2326  cbv3hv  2337  dvelimhw  2342  cbv3h  2404  equsalh  2420  equsexh  2421  nfae  2433  axc16i  2436  dvelimh  2450  nfs1  2488  hbsb  2524  sb7h  2526  nfsab  2723  nfsabg  2724  cleqh  2864  nfcii  2888  nfcriOLDOLDOLD  2898  nfralw  3309  bnj596  33757  bnj1146  33802  bnj1379  33841  bnj1464  33855  bnj1468  33857  bnj605  33918  bnj607  33927  bnj916  33944  bnj964  33954  bnj981  33961  bnj983  33962  bnj1014  33972  bnj1123  33997  bnj1373  34041  bnj1417  34052  bnj1445  34055  bnj1463  34066  bnj1497  34071  bj-cbv3hv2  35673  bj-equsalhv  35684  bj-nfs1v  35691  bj-nfsab1  35694  bj-gabima  35820  wl-nfalv  36394  nfequid-o  37780  nfa1-o  37785  2sb5ndVD  43671  2sb5ndALT  43693