Theorem nf5i 2146

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

Syntax hints:   → wi 4  ∀wal 1538  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-10 2141

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfnaew  2149  nfe1  2150  sbh  2273  nf5di  2285  19.9h  2286  19.21h  2287  19.23h  2288  exlimih  2289  exlimdh  2290  equsalhw  2291  equsexhv  2292  hban  2300  hb3an  2301  nfal  2323  hbex  2325  nfsbv  2330  cbv3hv  2341  dvelimhw  2346  cbv3h  2408  equsalh  2424  equsexh  2425  nfae  2437  axc16i  2440  dvelimh  2454  nfs1  2492  hbsb  2528  sb7h  2530  nfsab  2725  nfsabg  2726  cleqh  2864  nfcii  2887  nfralw  3291  bnj596  34777  bnj1146  34822  bnj1379  34861  bnj1464  34875  bnj1468  34877  bnj605  34938  bnj607  34947  bnj916  34964  bnj964  34974  bnj981  34981  bnj983  34982  bnj1014  34992  bnj1123  35017  bnj1373  35061  bnj1417  35072  bnj1445  35075  bnj1463  35086  bnj1497  35091  bj-cbv3hv2  36813  bj-equsalhv  36824  bj-nfs1v  36831  bj-nfsab1  36834  bj-gabima  36958  wl-nfalv  37543  nfequid-o  38928  nfa1-o  38933  2sb5ndVD  44934  2sb5ndALT  44956