Theorem nf5i 2011

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

Syntax hints:   → wi 4  ∀wal 1473  Ⅎwnf 1699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-10 2006

This theorem depends on definitions:  df-bi 196  df-ex 1696  df-nf 1701

This theorem is referenced by:  nfe1  2014  nf5di  2105  19.9h  2106  19.21h  2107  19.23h  2108  hban  2113  hb3an  2114  exlimih  2133  exlimdh  2134  equsexhv  2135  nfal  2139  nfexOLD  2141  hbex  2142  nfa1OLD  2143  dvelimhw  2159  cbv3hv  2160  cbv3h  2254  equsalh  2280  equsexh  2283  nfae  2304  axc16i  2310  dvelimh  2324  nfs1  2353  sbh  2369  nfs1v  2425  hbsb  2429  sb7h  2442  nfsab1  2600  nfsab  2602  cleqh  2711  nfcii  2742  nfcri  2745  bnj596  30070  bnj1146  30116  bnj1379  30155  bnj1464  30168  bnj1468  30170  bnj605  30231  bnj607  30240  bnj916  30257  bnj964  30267  bnj981  30274  bnj983  30275  bnj1014  30284  bnj1123  30308  bnj1373  30352  bnj1417  30363  bnj1445  30366  bnj1463  30377  bnj1497  30382  bj-cbv3hv2  31915  bj-equsalhv  31932  bj-nfs1v  31947  bj-nfsab1  31960  bj-nfdiOLD  32019  bj-nfcri  32046  wl-nfalv  32491  nfequid-o  33213  nfa1-o  33218  2sb5ndVD  38168  2sb5ndALT  38190