Theorem nf5i 2150

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

Syntax hints:   → wi 4  ∀wal 1535  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-10 2145

This theorem depends on definitions:  df-bi 209  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfnaew  2153  nfe1  2154  sbh  2273  nf5di  2293  19.9h  2294  19.21h  2295  19.23h  2296  exlimih  2297  exlimdh  2298  equsalhw  2299  equsexhv  2300  hban  2308  hb3an  2309  nfal  2342  hbex  2344  hbsbw  2351  cbv3hv  2360  dvelimhw  2366  cbv3h  2424  equsalh  2442  equsexh  2443  nfae  2455  axc16i  2458  dvelimh  2472  nfs1  2527  hbsb  2567  sb7h  2569  nfsab1OLD  2811  nfsab  2814  nfsabg  2815  cleqh  2938  nfcii  2967  nfcri  2973  bnj596  32019  bnj1146  32065  bnj1379  32104  bnj1464  32118  bnj1468  32120  bnj605  32181  bnj607  32190  bnj916  32207  bnj964  32217  bnj981  32224  bnj983  32225  bnj1014  32235  bnj1123  32260  bnj1373  32304  bnj1417  32315  bnj1445  32318  bnj1463  32329  bnj1497  32334  bj-cbv3hv2  34119  bj-equsalhv  34130  bj-nfs1v  34137  bj-nfsab1  34140  wl-nfalv  34767  nfequid-o  36048  nfa1-o  36053  2sb5ndVD  41251  2sb5ndALT  41273