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  2766  elrab3t  2893  mo2icl  2917  csbie2t  3106  sbcnestgf  3109  dfss4st  3369  dfnfc2  3828  mpteq12f  4084  copsex2t  4246  ssopab2  4276  alxfr  4462  eunex  4561  mosubopt  4692  fv3  5539  fvmptt  5608  fnoprabg  5976  fiintim  6928  bj-exlimmp  14524  bdsepnft  14642  setindft  14720  strcollnft  14739