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 1793	1 ⊢ Ⅎ𝑥𝜑

Syntax hints:   → wi 4  ∀wal 1534  Ⅎwnf 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-10 2138

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

This theorem is referenced by:  nfnaew  2146  nfe1  2147  sbh  2270  nf5di  2283  19.9h  2284  19.21h  2285  19.23h  2286  exlimih  2287  exlimdh  2288  equsalhw  2289  equsexhv  2290  hban  2298  hb3an  2299  nfal  2321  hbex  2323  nfsbv  2328  cbv3hv  2340  dvelimhw  2345  cbv3h  2406  equsalh  2422  equsexh  2423  nfae  2435  axc16i  2438  dvelimh  2452  nfs1  2490  hbsb  2526  sb7h  2528  nfsab  2724  nfsabg  2725  cleqh  2868  nfcii  2891  nfralw  3308  bnj596  34738  bnj1146  34783  bnj1379  34822  bnj1464  34836  bnj1468  34838  bnj605  34899  bnj607  34908  bnj916  34925  bnj964  34935  bnj981  34942  bnj983  34943  bnj1014  34953  bnj1123  34978  bnj1373  35022  bnj1417  35033  bnj1445  35036  bnj1463  35047  bnj1497  35052  bj-cbv3hv2  36777  bj-equsalhv  36788  bj-nfs1v  36795  bj-nfsab1  36798  bj-gabima  36922  wl-nfalv  37505  nfequid-o  38891  nfa1-o  38896  2sb5ndVD  44907  2sb5ndALT  44929