Theorem nf5i 2144

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

Syntax hints:   → wi 4  ∀wal 1537  Ⅎwnf 1787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-10 2139

This theorem depends on definitions:  df-bi 206  df-ex 1784  df-nf 1788

This theorem is referenced by:  nfnaew  2147  nfnaewOLD  2148  nfe1  2149  sbh  2268  nf5di  2285  19.9h  2286  19.21h  2287  19.23h  2288  exlimih  2289  exlimdh  2290  equsalhw  2291  equsexhv  2292  hban  2300  hb3an  2301  nfal  2321  hbex  2323  nfsbv  2328  hbsbwOLD  2330  cbv3hv  2339  dvelimhw  2345  cbv3h  2404  equsalh  2420  equsexh  2421  nfae  2433  axc16i  2436  dvelimh  2450  nfs1  2492  hbsb  2529  sb7h  2531  nfsab  2728  nfsabg  2729  cleqh  2862  nfcii  2890  nfcriOLDOLDOLD  2900  bnj596  32626  bnj1146  32671  bnj1379  32710  bnj1464  32724  bnj1468  32726  bnj605  32787  bnj607  32796  bnj916  32813  bnj964  32823  bnj981  32830  bnj983  32831  bnj1014  32841  bnj1123  32866  bnj1373  32910  bnj1417  32921  bnj1445  32924  bnj1463  32935  bnj1497  32940  bj-cbv3hv2  34904  bj-equsalhv  34915  bj-nfs1v  34922  bj-nfsab1  34925  bj-gabima  35055  wl-nfalv  35611  nfequid-o  36851  nfa1-o  36856  2sb5ndVD  42419  2sb5ndALT  42441