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  1998  nfsbxyt  1999  sbcomxyyz  2028  sbalyz  2055  dvelimALT  2066  hbe1a  2079  nfeu1  2093  moim  2147  euexex  2168  nfaba1  2392  nfabdw  2405  nfra1  2575  ceqsalg  2844  elrab3t  2975  mo2icl  2999  csbie2t  3190  sbcnestgf  3193  dfss4st  3458  dfnfc2  3937  mpteq12f  4195  copsex2t  4366  ssopab2  4399  alxfr  4587  eunex  4688  mosubopt  4820  fv3  5698  fvmptt  5774  fnoprabg  6162  fiintim  7204  bj-exlimmp  16653  bdsepnft  16769  setindft  16847  strcollnft  16866