Theorem nf5i 2179

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

Syntax hints:   → wi 4  ∀wal 1629  Ⅎwnf 1856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-10 2174

This theorem depends on definitions:  df-bi 197  df-ex 1853  df-nf 1858

This theorem is referenced by:  nfe1  2183  nf5di  2282  19.9h  2283  19.21h  2284  19.23h  2285  equsalhw  2286  equsexhv  2288  hban  2292  hb3an  2293  exlimih  2313  exlimdh  2314  nfal  2317  nfexOLD  2319  hbex  2320  nfa1OLD  2321  cbv3hv  2335  dvelimhw  2338  cbv3h  2427  equsalh  2449  equsexh  2450  nfae  2468  axc16i  2472  dvelimh  2486  nfs1  2512  sbh  2528  nfs1vOLD  2578  hbsb  2591  sb7h  2602  nfsab1  2761  nfsab  2763  cleqh  2873  nfcii  2904  nfcri  2907  bnj596  31154  bnj1146  31200  bnj1379  31239  bnj1464  31252  bnj1468  31254  bnj605  31315  bnj607  31324  bnj916  31341  bnj964  31351  bnj981  31358  bnj983  31359  bnj1014  31368  bnj1123  31392  bnj1373  31436  bnj1417  31447  bnj1445  31450  bnj1463  31461  bnj1497  31466  bj-cbv3hv2  33063  bj-equsalhv  33079  bj-nfs1v  33094  bj-nfsab1  33107  wl-nfalv  33646  nfequid-o  34716  nfa1-o  34721  2sb5ndVD  39666  2sb5ndALT  39688