Theorem nf5i 2190

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

Syntax hints:   → wi 4  ∀wal 1635  Ⅎwnf 1863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-10 2185

This theorem depends on definitions:  df-bi 198  df-ex 1860  df-nf 1864

This theorem is referenced by:  nfe1  2194  nf5di  2294  19.9h  2295  19.21h  2296  19.23h  2297  equsalhw  2298  equsexhv  2300  hban  2304  hb3an  2305  exlimih  2325  exlimdh  2326  nfal  2329  nfexOLD  2331  hbex  2332  nfa1OLD  2333  cbv3hv  2347  dvelimhw  2350  cbv3h  2439  equsalh  2461  equsexh  2462  nfae  2480  axc16i  2484  dvelimh  2498  nfs1  2524  sbh  2540  nfs1vOLD  2590  hbsb  2603  sb7h  2614  nfsab1  2794  nfsab  2796  cleqh  2906  nfcii  2937  nfcri  2940  bnj596  31137  bnj1146  31183  bnj1379  31222  bnj1464  31235  bnj1468  31237  bnj605  31298  bnj607  31307  bnj916  31324  bnj964  31334  bnj981  31341  bnj983  31342  bnj1014  31351  bnj1123  31375  bnj1373  31419  bnj1417  31430  bnj1445  31433  bnj1463  31444  bnj1497  31449  bj-cbv3hv2  33040  bj-equsalhv  33056  bj-nfs1v  33071  bj-nfsab1  33084  wl-nfalv  33624  nfequid-o  34687  nfa1-o  34692  2sb5ndVD  39638  2sb5ndALT  39660