Theorem nfa1 1529

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

Syntax hints:  ∀wal 1341  Ⅎwnf 1448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1437  ax-ial 1522

This theorem depends on definitions:  df-bi 116  df-nf 1449

This theorem is referenced by:  axc4i  1530  nfnf1  1532  nfa2  1567  nfia1  1568  alexdc  1607  nf2  1656  cbv1h  1734  sbf2  1766  sb4or  1821  nfsbxy  1930  nfsbxyt  1931  sbcomxyyz  1960  sbalyz  1987  dvelimALT  1998  hbe1a  2011  nfeu1  2025  moim  2078  euexex  2099  nfaba1  2314  nfabdw  2327  nfra1  2497  ceqsalg  2754  elrab3t  2881  mo2icl  2905  csbie2t  3093  sbcnestgf  3096  dfss4st  3355  dfnfc2  3807  mpteq12f  4062  copsex2t  4223  ssopab2  4253  alxfr  4439  eunex  4538  mosubopt  4669  fv3  5509  fvmptt  5577  fnoprabg  5943  fiintim  6894  bj-exlimmp  13650  bdsepnft  13769  setindft  13847  strcollnft  13866