Theorem nf5i 2148

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

Syntax hints:   → wi 4  ∀wal 1541  Ⅎwnf 1791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-10 2143

This theorem depends on definitions:  df-bi 210  df-ex 1788  df-nf 1792

This theorem is referenced by:  nfnaew  2151  nfnaewOLD  2152  nfe1  2153  sbh  2271  nf5di  2288  19.9h  2289  19.21h  2290  19.23h  2291  exlimih  2292  exlimdh  2293  equsalhw  2294  equsexhv  2295  hban  2303  hb3an  2304  nfal  2324  hbex  2326  hbsbwOLD  2332  cbv3hv  2341  dvelimhw  2347  cbv3h  2403  equsalh  2419  equsexh  2420  nfae  2432  axc16i  2435  dvelimh  2449  nfs1  2491  hbsb  2528  sb7h  2530  nfsab  2726  nfsabg  2727  cleqh  2854  nfcii  2881  nfcriOLDOLDOLD  2891  bnj596  32392  bnj1146  32438  bnj1379  32477  bnj1464  32491  bnj1468  32493  bnj605  32554  bnj607  32563  bnj916  32580  bnj964  32590  bnj981  32597  bnj983  32598  bnj1014  32608  bnj1123  32633  bnj1373  32677  bnj1417  32688  bnj1445  32691  bnj1463  32702  bnj1497  32707  bj-cbv3hv2  34663  bj-equsalhv  34674  bj-nfs1v  34681  bj-nfsab1  34684  bj-gabima  34814  wl-nfalv  35370  nfequid-o  36610  nfa1-o  36615  2sb5ndVD  42144  2sb5ndALT  42166