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  2765  elrab3t  2892  mo2icl  2916  csbie2t  3105  sbcnestgf  3108  dfss4st  3368  dfnfc2  3827  mpteq12f  4083  copsex2t  4245  ssopab2  4275  alxfr  4461  eunex  4560  mosubopt  4691  fv3  5538  fvmptt  5607  fnoprabg  5975  fiintim  6927  bj-exlimmp  14491  bdsepnft  14609  setindft  14687  strcollnft  14706