Theorem nfa1 1534

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

Syntax hints:  ∀wal 1346  Ⅎwnf 1453

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 1442  ax-ial 1527

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

This theorem is referenced by:  axc4i  1535  nfnf1  1537  nfa2  1572  nfia1  1573  alexdc  1612  nf2  1661  cbv1h  1739  sbf2  1771  sb4or  1826  nfsbxy  1935  nfsbxyt  1936  sbcomxyyz  1965  sbalyz  1992  dvelimALT  2003  hbe1a  2016  nfeu1  2030  moim  2083  euexex  2104  nfaba1  2318  nfabdw  2331  nfra1  2501  ceqsalg  2758  elrab3t  2885  mo2icl  2909  csbie2t  3097  sbcnestgf  3100  dfss4st  3360  dfnfc2  3814  mpteq12f  4069  copsex2t  4230  ssopab2  4260  alxfr  4446  eunex  4545  mosubopt  4676  fv3  5519  fvmptt  5587  fnoprabg  5954  fiintim  6906  bj-exlimmp  13804  bdsepnft  13922  setindft  14000  strcollnft  14019