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 ⊢ Ⅎ𝑥∀𝑥𝜑

Syntax hints:  ∀wal 1400  Ⅎwnf 1513

This theorem was proved from 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 theorem depends on definitions:  df-bi 117  df-nf 1514

This theorem is referenced 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  3951  mpteq12f  4209  copsex2t  4383  ssopab2  4416  alxfr  4605  eunex  4706  mosubopt  4838  fv3  5716  fvmptt  5794  fnoprabg  6183  fiintim  7232  bj-exlimmp  16780  bdsepnft  16896  setindft  16974  strcollnft  16993  dfalseu2  17151