Theorem nfa1 1590

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

Syntax hints:  ∀wal 1396  Ⅎwnf 1509

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 1498  ax-ial 1583

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

This theorem is referenced by:  axc4i  1591  nfnf1  1593  nfa2  1628  nfia1  1629  alexdc  1668  nf2  1716  cbv1h  1794  sbf2  1826  sb4or  1881  nfsbxy  1995  nfsbxyt  1996  sbcomxyyz  2025  sbalyz  2052  dvelimALT  2063  hbe1a  2076  nfeu1  2090  moim  2144  euexex  2165  nfaba1  2381  nfabdw  2394  nfra1  2564  ceqsalg  2832  elrab3t  2962  mo2icl  2986  csbie2t  3177  sbcnestgf  3180  dfss4st  3442  dfnfc2  3916  mpteq12f  4174  copsex2t  4343  ssopab2  4376  alxfr  4564  eunex  4665  mosubopt  4797  fv3  5671  fvmptt  5747  fnoprabg  6132  fiintim  7166  bj-exlimmp  16467  bdsepnft  16583  setindft  16661  strcollnft  16680