Theorem nfa1 1521

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

Syntax hints:  ∀wal 1329  Ⅎwnf 1436

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 1425  ax-ial 1514

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

This theorem is referenced by:  nfnf1  1523  nfa2  1558  nfia1  1559  alexdc  1598  nf2  1646  cbv1h  1723  sbf2  1751  sb4or  1805  nfsbxy  1913  nfsbxyt  1914  sbcomxyyz  1943  sbalyz  1972  dvelimALT  1983  nfeu1  2008  moim  2061  euexex  2082  nfaba1  2285  nfra1  2464  ceqsalg  2709  elrab3t  2834  mo2icl  2858  csbie2t  3043  sbcnestgf  3046  dfss4st  3304  dfnfc2  3749  mpteq12f  4003  copsex2t  4162  ssopab2  4192  alxfr  4377  eunex  4471  mosubopt  4599  fv3  5437  fvmptt  5505  fnoprabg  5865  fiintim  6810  bj-exlimmp  12965  bdsepnft  13074  setindft  13152  strcollnft  13171