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  1795  sbf2  1827  sb4or  1882  nfsbxy  1996  nfsbxyt  1997  sbcomxyyz  2026  sbalyz  2053  dvelimALT  2064  hbe1a  2077  nfeu1  2091  moim  2145  euexex  2166  nfaba1  2390  nfabdw  2403  nfra1  2573  ceqsalg  2841  elrab3t  2971  mo2icl  2995  csbie2t  3186  sbcnestgf  3189  dfss4st  3453  dfnfc2  3931  mpteq12f  4189  copsex2t  4360  ssopab2  4393  alxfr  4581  eunex  4682  mosubopt  4814  fv3  5692  fvmptt  5768  fnoprabg  6153  fiintim  7190  bj-exlimmp  16533  bdsepnft  16649  setindft  16727  strcollnft  16746