Theorem nf5i 2157

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

Syntax hints:   → wi 4  ∀wal 1545  Ⅎwnf 1790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-10 2152

This theorem depends on definitions:  df-bi 208  df-ex 1787  df-nf 1791

This theorem is referenced by:  nfnaew  2160  nfe1  2161  sbh  2284  nf5di  2296  19.9h  2297  19.21h  2298  19.23h  2299  exlimih  2300  exlimdh  2301  equsalhw  2302  equsexhv  2303  hban  2311  hb3an  2312  nfal  2332  hbex  2334  nfsbv  2339  cbv3hv  2348  dvelimhw  2353  cbv3h  2412  equsalh  2428  equsexh  2429  nfae  2441  axc16i  2444  dvelimh  2458  nfs1  2496  hbsb  2532  sb7h  2534  nfsab  2729  nfsabg  2730  cleqh  2868  nfcii  2890  nfralw  3286  bnj596  34929  bnj1146  34973  bnj1379  35012  bnj1464  35026  bnj1468  35028  bnj605  35089  bnj607  35098  bnj916  35115  bnj964  35125  bnj981  35132  bnj983  35133  bnj1014  35143  bnj1123  35168  bnj1373  35212  bnj1417  35223  bnj1445  35226  bnj1463  35237  bnj1497  35242  bj-cbv3hv2  37148  bj-equsalhv  37159  bj-nfs1v  37166  bj-nfsab1  37169  bj-gabima  37293  wl-nfalv  37896  nfequid-o  39402  nfa1-o  39407  nfalh  42699  2sb5ndVD  45353  2sb5ndALT  45375