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  33746  bnj1146  33791  bnj1379  33830  bnj1464  33844  bnj1468  33846  bnj605  33907  bnj607  33916  bnj916  33933  bnj964  33943  bnj981  33950  bnj983  33951  bnj1014  33961  bnj1123  33986  bnj1373  34030  bnj1417  34041  bnj1445  34044  bnj1463  34055  bnj1497  34060  bj-cbv3hv2  35662  bj-equsalhv  35673  bj-nfs1v  35680  bj-nfsab1  35683  bj-gabima  35809  wl-nfalv  36383  nfequid-o  37769  nfa1-o  37774  2sb5ndVD  43657  2sb5ndALT  43679