Theorem nf5i 2024

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

Syntax hints:   → wi 4  ∀wal 1481  Ⅎwnf 1708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-10 2019

This theorem depends on definitions:  df-bi 197  df-ex 1705  df-nf 1710

This theorem is referenced by:  nfe1  2027  nf5di  2119  19.9h  2120  19.21h  2121  19.23h  2122  equsexhv  2124  hban  2128  hb3an  2129  exlimih  2148  exlimdh  2149  nfal  2153  nfexOLD  2155  hbex  2156  nfa1OLD  2157  dvelimhw  2173  cbv3hv  2174  cbv3h  2266  equsalh  2294  equsexh  2295  nfae  2316  axc16i  2322  dvelimh  2336  nfs1  2365  sbh  2381  nfs1v  2437  hbsb  2441  sb7h  2454  nfsab1  2612  nfsab  2614  cleqh  2724  nfcii  2755  nfcri  2758  bnj596  30816  bnj1146  30862  bnj1379  30901  bnj1464  30914  bnj1468  30916  bnj605  30977  bnj607  30986  bnj916  31003  bnj964  31013  bnj981  31020  bnj983  31021  bnj1014  31030  bnj1123  31054  bnj1373  31098  bnj1417  31109  bnj1445  31112  bnj1463  31123  bnj1497  31128  bj-cbv3hv2  32728  bj-equsalhv  32744  bj-nfs1v  32759  bj-nfsab1  32772  bj-nfcri  32852  wl-nfalv  33312  nfequid-o  34195  nfa1-o  34200  2sb5ndVD  39146  2sb5ndALT  39168