Theorem nfa1 1565

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

Syntax hints:  ∀wal 1371  Ⅎwnf 1484

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 1473  ax-ial 1558

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

This theorem is referenced by:  axc4i  1566  nfnf1  1568  nfa2  1603  nfia1  1604  alexdc  1643  nf2  1692  cbv1h  1770  sbf2  1802  sb4or  1857  nfsbxy  1971  nfsbxyt  1972  sbcomxyyz  2001  sbalyz  2028  dvelimALT  2039  hbe1a  2052  nfeu1  2066  moim  2119  euexex  2140  nfaba1  2355  nfabdw  2368  nfra1  2538  ceqsalg  2802  elrab3t  2930  mo2icl  2954  csbie2t  3144  sbcnestgf  3147  dfss4st  3408  dfnfc2  3871  mpteq12f  4129  copsex2t  4294  ssopab2  4327  alxfr  4513  eunex  4614  mosubopt  4745  fv3  5609  fvmptt  5681  fnoprabg  6056  fiintim  7040  bj-exlimmp  15819  bdsepnft  15937  setindft  16015  strcollnft  16034