Theorem nfa1 1541

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

Syntax hints:  ∀wal 1351  Ⅎwnf 1460

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 1449  ax-ial 1534

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

This theorem is referenced by:  axc4i  1542  nfnf1  1544  nfa2  1579  nfia1  1580  alexdc  1619  nf2  1668  cbv1h  1746  sbf2  1778  sb4or  1833  nfsbxy  1942  nfsbxyt  1943  sbcomxyyz  1972  sbalyz  1999  dvelimALT  2010  hbe1a  2023  nfeu1  2037  moim  2090  euexex  2111  nfaba1  2325  nfabdw  2338  nfra1  2508  ceqsalg  2767  elrab3t  2894  mo2icl  2918  csbie2t  3107  sbcnestgf  3110  dfss4st  3370  dfnfc2  3829  mpteq12f  4085  copsex2t  4247  ssopab2  4277  alxfr  4463  eunex  4562  mosubopt  4693  fv3  5540  fvmptt  5610  fnoprabg  5979  fiintim  6931  bj-exlimmp  14709  bdsepnft  14827  setindft  14905  strcollnft  14924