Theorem nf5i 2084

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

Syntax hints:   → wi 4  ∀wal 1505  Ⅎwnf 1746

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-10 2079

This theorem depends on definitions:  df-bi 199  df-ex 1743  df-nf 1747

This theorem is referenced by:  nfe1  2087  sbh  2201  nf5di  2219  19.9h  2220  19.21h  2221  19.23h  2222  exlimih  2223  exlimdh  2224  equsalhw  2225  equsexhv  2226  hban  2234  hb3an  2235  nfal  2263  hbex  2265  cbv3hv  2276  dvelimhw  2279  cbv3h  2337  equsalh  2355  equsexh  2356  nfae  2369  axc16i  2372  dvelimh  2386  nfs1  2448  hbsb  2489  sb7h  2492  nfsab1OLD  2768  nfsab  2770  cleqh  2889  nfcii  2920  nfcri  2926  bnj596  31671  bnj1146  31717  bnj1379  31756  bnj1464  31769  bnj1468  31771  bnj605  31832  bnj607  31841  bnj916  31858  bnj964  31868  bnj981  31875  bnj983  31876  bnj1014  31885  bnj1123  31909  bnj1373  31953  bnj1417  31964  bnj1445  31967  bnj1463  31978  bnj1497  31983  bj-cbv3hv2  33581  bj-equsalhv  33595  bj-nfs1v  33605  bj-nfsab1  33610  wl-nfalv  34214  nfequid-o  35497  nfa1-o  35502  2sb5ndVD  40669  2sb5ndALT  40691