Theorem nfa1 1552

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

Syntax hints:  ∀wal 1362  Ⅎwnf 1471

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 1460  ax-ial 1545

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

This theorem is referenced by:  axc4i  1553  nfnf1  1555  nfa2  1590  nfia1  1591  alexdc  1630  nf2  1679  cbv1h  1757  sbf2  1789  sb4or  1844  nfsbxy  1958  nfsbxyt  1959  sbcomxyyz  1988  sbalyz  2015  dvelimALT  2026  hbe1a  2039  nfeu1  2053  moim  2106  euexex  2127  nfaba1  2342  nfabdw  2355  nfra1  2525  ceqsalg  2788  elrab3t  2915  mo2icl  2939  csbie2t  3129  sbcnestgf  3132  dfss4st  3392  dfnfc2  3853  mpteq12f  4109  copsex2t  4274  ssopab2  4306  alxfr  4492  eunex  4593  mosubopt  4724  fv3  5577  fvmptt  5649  fnoprabg  6019  fiintim  6985  bj-exlimmp  15261  bdsepnft  15379  setindft  15457  strcollnft  15476