Theorem nfa1 1522

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

Syntax hints:  ∀wal 1330  Ⅎwnf 1437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1426  ax-ial 1515

This theorem depends on definitions:  df-bi 116  df-nf 1438

This theorem is referenced by:  nfnf1  1524  nfa2  1559  nfia1  1560  alexdc  1599  nf2  1647  cbv1h  1724  sbf2  1752  sb4or  1806  nfsbxy  1916  nfsbxyt  1917  sbcomxyyz  1946  sbalyz  1975  dvelimALT  1986  nfeu1  2011  moim  2064  euexex  2085  nfaba1  2288  nfra1  2469  ceqsalg  2717  elrab3t  2843  mo2icl  2867  csbie2t  3053  sbcnestgf  3056  dfss4st  3314  dfnfc2  3762  mpteq12f  4016  copsex2t  4175  ssopab2  4205  alxfr  4390  eunex  4484  mosubopt  4612  fv3  5452  fvmptt  5520  fnoprabg  5880  fiintim  6825  bj-exlimmp  13147  bdsepnft  13256  setindft  13334  strcollnft  13353