Theorem nf5i 2181

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

Syntax hints:   → wi 4  ∀wal 1568  Ⅎwnf 1813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-10 2176

This theorem depends on definitions:  df-bi 210  df-ex 1810  df-nf 1814

This theorem is referenced by:  nfnaew  2184  nfe1  2185  sbh  2308  nf5di  2320  19.9h  2321  19.21h  2322  19.23h  2323  exlimih  2324  exlimdh  2325  equsalhw  2326  equsexhv  2327  hban  2335  hb3an  2336  nfal  2356  hbex  2358  nfsbv  2363  cbv3hv  2372  dvelimhw  2377  cbv3h  2436  equsalh  2452  equsexh  2453  nfae  2465  axc16i  2468  dvelimh  2482  nfs1  2520  hbsb  2556  sb7h  2558  nfsab  2753  nfsabg  2754  cleqh  2892  nfcii  2914  nfralw  3312  bnj596  35135  bnj1146  35179  bnj1379  35218  bnj1464  35232  bnj1468  35234  bnj605  35295  bnj607  35304  bnj916  35321  bnj964  35331  bnj981  35338  bnj983  35339  bnj1014  35349  bnj1123  35374  bnj1373  35418  bnj1417  35429  bnj1445  35432  bnj1463  35443  bnj1497  35448  bj-cbv3hv2  37450  bj-equsalhv  37461  bj-nfs1v  37468  bj-nfsab1  37471  bj-gabima  37596  wl-nfalv  38200  nfequid-o  39704  nfa1-o  39709  nfalh  43003  2sb5ndVD  45638  2sb5ndALT  45660