Theorem nfa1 1434

Description: 𝑥 is not free in ∀𝑥𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

Ref	Expression
nfa1	⊢ Ⅎ𝑥∀𝑥𝜑

Proof of Theorem nfa1

Step	Hyp	Ref	Expression
1		hba1 1433	. 2 ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑)
2	1	nfi 1351	1 ⊢ Ⅎ𝑥∀𝑥𝜑

Syntax hints:  ∀wal 1241  Ⅎwnf 1349

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1338  ax-ial 1427

This theorem depends on definitions:  df-bi 110  df-nf 1350

This theorem is referenced by:  nfnf1  1436  nfa2  1471  nfia1  1472  alexdc  1510  nf2  1558  cbv1h  1633  sbf2  1661  sb4or  1714  nfsbxy  1818  nfsbxyt  1819  sbcomxyyz  1846  sbalyz  1875  dvelimALT  1886  nfeu1  1911  moim  1964  euexex  1985  nfaba1  2183  nfra1  2355  ceqsalg  2582  elrab3t  2697  mo2icl  2720  csbie2t  2894  sbcnestgf  2897  dfnfc2  3598  mpteq12f  3837  copsex2t  3982  ssopab2  4012  alxfr  4193  eunex  4285  mosubopt  4405  fv3  5197  fvmptt  5262  fnoprabg  5602  bj-exlimmp  9909  bdsepnft  10007  setindft  10090  strcollnft  10109