Theorem nf5i 2186

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-10 2180

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817

This theorem is used by:  nfnaew  2189  nfe1  2190  sbh  2310  nf5diOLD  2322  19.9h  2323  19.21h  2324  19.23h  2325  exlimih  2326  exlimdh  2327  equsalhw  2328  equsexhv  2329  hbanOLD  2337  hb3anOLD  2338  nfal  2357  hbex  2359  nfsbv  2364  cbv3hv  2373  dvelimhw  2378  cbv3h  2436  equsalh  2452  equsexh  2453  nfae  2465  axc16i  2468  dvelimh  2482  nfs1  2520  hbsb  2556  sb7h  2558  nfsab  2753  nfsabg  2754  cleqh  2893  nfcii  2915  nfralw  3313  bnj596  35488  bnj1146  35532  bnj1379  35571  bnj1464  35585  bnj1468  35587  bnj605  35648  bnj607  35657  bnj916  35674  bnj964  35684  bnj981  35691  bnj983  35692  bnj1014  35702  bnj1123  35727  bnj1373  35771  bnj1417  35782  bnj1445  35785  bnj1463  35796  bnj1497  35801  bj-cbv3hv2  37922  bj-equsalhv  37933  bj-nfs1v  37940  bj-nfsab1  37943  bj-gabima  38068  wl-nfalv  38725  nfequid-o  40233  nfa1-o  40238  nfalh  43533  2sb5ndVD  46152  2sb5ndALT  46174