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 1537  Ⅎ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  2266  nf5di  2283  19.9h  2284  19.21h  2285  19.23h  2286  exlimih  2287  exlimdh  2288  equsalhw  2289  equsexhv  2290  hban  2298  hb3an  2299  nfal  2318  hbex  2320  nfsbv  2325  hbsbwOLD  2327  cbv3hv  2338  dvelimhw  2344  cbv3h  2405  equsalh  2421  equsexh  2422  nfae  2434  axc16i  2437  dvelimh  2451  nfs1  2493  hbsb  2530  sb7h  2532  nfsab  2729  nfsabg  2730  cleqh  2863  nfcii  2892  nfcriOLDOLDOLD  2902  nfralw  3152  bnj596  32735  bnj1146  32780  bnj1379  32819  bnj1464  32833  bnj1468  32835  bnj605  32896  bnj607  32905  bnj916  32922  bnj964  32932  bnj981  32939  bnj983  32940  bnj1014  32950  bnj1123  32975  bnj1373  33019  bnj1417  33030  bnj1445  33033  bnj1463  33044  bnj1497  33049  bj-cbv3hv2  34986  bj-equsalhv  34997  bj-nfs1v  35004  bj-nfsab1  35007  bj-gabima  35137  wl-nfalv  35693  nfequid-o  36931  nfa1-o  36936  2sb5ndVD  42537  2sb5ndALT  42559