Theorem nfa1 1555

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

Syntax hints:  ∀wal 1362  Ⅎwnf 1474

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 1463  ax-ial 1548

This theorem depends on definitions:  df-bi 117  df-nf 1475

This theorem is referenced by:  axc4i  1556  nfnf1  1558  nfa2  1593  nfia1  1594  alexdc  1633  nf2  1682  cbv1h  1760  sbf2  1792  sb4or  1847  nfsbxy  1961  nfsbxyt  1962  sbcomxyyz  1991  sbalyz  2018  dvelimALT  2029  hbe1a  2042  nfeu1  2056  moim  2109  euexex  2130  nfaba1  2345  nfabdw  2358  nfra1  2528  ceqsalg  2791  elrab3t  2919  mo2icl  2943  csbie2t  3133  sbcnestgf  3136  dfss4st  3397  dfnfc2  3858  mpteq12f  4114  copsex2t  4279  ssopab2  4311  alxfr  4497  eunex  4598  mosubopt  4729  fv3  5584  fvmptt  5656  fnoprabg  6027  fiintim  7001  bj-exlimmp  15499  bdsepnft  15617  setindft  15695  strcollnft  15714