Theorem nfa1 1587

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

Syntax hints:  ∀wal 1393  Ⅎwnf 1506

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 1495  ax-ial 1580

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

This theorem is referenced by:  axc4i  1588  nfnf1  1590  nfa2  1625  nfia1  1626  alexdc  1665  nf2  1714  cbv1h  1792  sbf2  1824  sb4or  1879  nfsbxy  1993  nfsbxyt  1994  sbcomxyyz  2023  sbalyz  2050  dvelimALT  2061  hbe1a  2074  nfeu1  2088  moim  2142  euexex  2163  nfaba1  2378  nfabdw  2391  nfra1  2561  ceqsalg  2828  elrab3t  2958  mo2icl  2982  csbie2t  3173  sbcnestgf  3176  dfss4st  3437  dfnfc2  3906  mpteq12f  4164  copsex2t  4332  ssopab2  4365  alxfr  4553  eunex  4654  mosubopt  4786  fv3  5655  fvmptt  5731  fnoprabg  6114  fiintim  7109  bj-exlimmp  16242  bdsepnft  16359  setindft  16437  strcollnft  16456