Theorem nf5i 2149

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

Syntax hints:   → wi 4  ∀wal 1539  Ⅎ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 2144

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

This theorem is referenced by:  nfnaew  2152  nfe1  2153  sbh  2275  nf5di  2287  19.9h  2288  19.21h  2289  19.23h  2290  exlimih  2291  exlimdh  2292  equsalhw  2293  equsexhv  2294  hban  2302  hb3an  2303  nfal  2324  hbex  2326  nfsbv  2331  cbv3hv  2340  dvelimhw  2345  cbv3h  2404  equsalh  2420  equsexh  2421  nfae  2433  axc16i  2436  dvelimh  2450  nfs1  2488  hbsb  2524  sb7h  2526  nfsab  2721  nfsabg  2722  cleqh  2860  nfcii  2883  nfralw  3279  bnj596  34758  bnj1146  34803  bnj1379  34842  bnj1464  34856  bnj1468  34858  bnj605  34919  bnj607  34928  bnj916  34945  bnj964  34955  bnj981  34962  bnj983  34963  bnj1014  34973  bnj1123  34998  bnj1373  35042  bnj1417  35053  bnj1445  35056  bnj1463  35067  bnj1497  35072  bj-cbv3hv2  36839  bj-equsalhv  36850  bj-nfs1v  36857  bj-nfsab1  36860  bj-gabima  36984  wl-nfalv  37569  nfequid-o  39019  nfa1-o  39024  2sb5ndVD  45012  2sb5ndALT  45034