Theorem nfa1 1594

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

This proof depends on syntax axioms:  ∀wal 1400  Ⅎwnf 1513

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502  ax-ial 1587

This proof depends on definitions:  df-bi 117  df-nf 1514

This theorem is used by:  axc4i  1595  nfnf1  1597  nfa2  1632  nfia1  1633  alexdc  1672  nf2  1720  cbv1h  1799  sbf2  1831  sb4or  1886  nfsbxy  2002  nfsbxyt  2003  sbcomxyyz  2032  sbalyz  2059  dvelimALT  2070  hbe1a  2083  nfeu1  2097  moim  2151  euexex  2172  nfaba1  2398  nfabdw  2411  nfra1  2581  ceqsalg  2850  elrab3t  2981  mo2icl  3005  csbie2t  3196  sbcnestgf  3199  dfss4st  3464  dfnfc2  3953  mpteq12f  4211  copsex2t  4385  ssopab2  4418  alxfr  4607  eunex  4708  mosubopt  4840  fv3  5718  fvmptt  5797  fnoprabg  6189  fiintim  7238  bj-exlimmp  16809  bdsepnft  16925  setindft  17003  strcollnft  17022  dfalseu2  17189