Theorem nf5i 2135

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

Syntax hints:   → wi 4  ∀wal 1532  Ⅎwnf 1778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-10 2130

This theorem depends on definitions:  df-bi 206  df-ex 1775  df-nf 1779

This theorem is referenced by:  nfnaew  2138  nfnaewOLD  2139  nfe1  2140  sbh  2260  nf5di  2275  19.9h  2276  19.21h  2277  19.23h  2278  exlimih  2279  exlimdh  2280  equsalhw  2281  equsexhv  2282  hban  2290  hb3an  2291  nfal  2312  hbex  2314  nfsbv  2319  cbv3hv  2331  dvelimhw  2336  cbv3h  2398  equsalh  2414  equsexh  2415  nfae  2427  axc16i  2430  dvelimh  2444  nfs1  2482  hbsb  2518  sb7h  2520  nfsab  2716  nfsabg  2717  cleqh  2856  nfcii  2880  nfralw  3299  bnj596  34602  bnj1146  34647  bnj1379  34686  bnj1464  34700  bnj1468  34702  bnj605  34763  bnj607  34772  bnj916  34789  bnj964  34799  bnj981  34806  bnj983  34807  bnj1014  34817  bnj1123  34842  bnj1373  34886  bnj1417  34897  bnj1445  34900  bnj1463  34911  bnj1497  34916  bj-cbv3hv2  36511  bj-equsalhv  36522  bj-nfs1v  36529  bj-nfsab1  36532  bj-gabima  36657  wl-nfalv  37231  nfequid-o  38619  nfa1-o  38624  2sb5ndVD  44621  2sb5ndALT  44643