Theorem nf5i 2147

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

Syntax hints:   → wi 4  ∀wal 1538  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-10 2142

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfnaew  2150  nfe1  2151  sbh  2273  nf5di  2285  19.9h  2286  19.21h  2287  19.23h  2288  exlimih  2289  exlimdh  2290  equsalhw  2291  equsexhv  2292  hban  2300  hb3an  2301  nfal  2322  hbex  2324  nfsbv  2329  cbv3hv  2338  dvelimhw  2343  cbv3h  2402  equsalh  2418  equsexh  2419  nfae  2431  axc16i  2434  dvelimh  2448  nfs1  2486  hbsb  2522  sb7h  2524  nfsab  2719  nfsabg  2720  cleqh  2857  nfcii  2880  nfralw  3285  bnj596  34736  bnj1146  34781  bnj1379  34820  bnj1464  34834  bnj1468  34836  bnj605  34897  bnj607  34906  bnj916  34923  bnj964  34933  bnj981  34940  bnj983  34941  bnj1014  34951  bnj1123  34976  bnj1373  35020  bnj1417  35031  bnj1445  35034  bnj1463  35045  bnj1497  35050  bj-cbv3hv2  36783  bj-equsalhv  36794  bj-nfs1v  36801  bj-nfsab1  36804  bj-gabima  36928  wl-nfalv  37513  nfequid-o  38903  nfa1-o  38908  2sb5ndVD  44899  2sb5ndALT  44921