Theorem nfa1 1474

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 1473	. 2 ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑)
2	1	nfi 1391	1 ⊢ Ⅎ𝑥∀𝑥𝜑

Syntax hints:  ∀wal 1282  Ⅎwnf 1389

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1378  ax-ial 1467

This theorem depends on definitions:  df-bi 115  df-nf 1390

This theorem is referenced by:  nfnf1  1476  nfa2  1511  nfia1  1512  alexdc  1550  nf2  1598  cbv1h  1673  sbf2  1701  sb4or  1754  nfsbxy  1859  nfsbxyt  1860  sbcomxyyz  1887  sbalyz  1916  dvelimALT  1927  nfeu1  1952  moim  2005  euexex  2026  nfaba1  2224  nfra1  2397  ceqsalg  2627  elrab3t  2748  mo2icl  2771  csbie2t  2950  sbcnestgf  2953  dfnfc2  3619  mpteq12f  3858  copsex2t  4000  ssopab2  4030  alxfr  4211  eunex  4304  mosubopt  4423  fv3  5218  fvmptt  5283  fnoprabg  5622  bj-exlimmp  10580  bdsepnft  10678  setindft  10760  strcollnft  10779