Theorem nfa1 2189

Description: The setvar 𝑥 is not free in ∀𝑥𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1817 changed. (Revised by Wolf Lammen, 11-Sep-2021.) Remove dependency on ax-12 2216. (Revised by Wolf Lammen, 12-Oct-2021.)

Assertion

Ref	Expression
nfa1	⊢ Ⅎ𝑥∀𝑥𝜑

Proof of Theorem nfa1

Step	Hyp	Ref	Expression
1		alex 1859	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		nfe1 2188	. . 3 ⊢ Ⅎ𝑥∃𝑥 ¬ 𝜑
3	2	nfn 1890	. 2 ⊢ Ⅎ𝑥 ¬ ∃𝑥 ¬ 𝜑
4	1, 3	nfxfr 1886	1 ⊢ Ⅎ𝑥∀𝑥𝜑

This proof depends on syntax axioms:  ¬ wn 3  ∀wal 1568  ∃wex 1812  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-10 2179

This proof depends on definitions:  df-bi 210  df-or 862  df-ex 1813  df-nf 1817

This theorem is used by:  nfna1  2190  nfia1  2191  nfnf1  2192  nfs1v  2194  nfa2  2213  sbalexOLD  2282  sbf2  2310  equs5av  2315  nf5  2320  hba1  2331  axc4i  2358  19.12  2363  exsb  2394  equs5aALT  2401  equs5eALT  2402  cbv1h  2440  dral1  2474  nfald2  2480  equs5a  2492  equs5e  2493  equs5  2495  axc14  2498  nfsb4t  2534  sbcom3  2541  moexexlem  2657  2eu6  2687  axi12  2736  nfaba1  2936  nfaba1g  2937  nfra1  3292  ceqsalgALT  3494  elrab3t  3652  csbie2t  3894  rexdifi  4107  sbcnestgfw  4389  sbcnestgf  4394  dfnfc2  4899  mpteq12f  5201  axrep2  5246  axrep3  5247  axrep4OLD  5250  alxfr  5383  axprlem4OLD  5406  axprlem5OLD  5407  copsex2t  5480  mosubopt  5498  fv3  6906  fvmptt  7017  fnoprabg  7546  pssnn  9163  fiint  9296  aceq1  10120  zorn2lem4  10501  zfcndrep  10617  mreexexd  17729  dvelimalcased  35495  dvelimexcased  35497  fineqvrep  35551  axsepg4  35580  dfon2lem7  36300  mh-setindnd  37089  bj-alalbial  37367  bj-exalbial  37368  bj-biexal1  37371  bj-bialal  37374  bj-cbv1hv  37472  ax11-pm  37508  bj-snsetex  37640  exlimim  38029  exellim  38031  difunieq  38061  fvineqsneq  38099  wl-nfimf1  38222  wl-nfae1  38223  wl-sb8t  38248  wl-sbnf1  38251  wl-2spsbbi  38261  wl-lem-moexsb  38264  wl-mo2tf  38267  wl-eutf  38269  wl-mo2t  38271  wl-mo3t  38272  wl-sb8eut  38274  sbali  38802  setindtr  43792  unielss  43986  ismnushort  45052  axc11next  45157  pm14.122b  45174  pm14.123b  45177  ax6e2ndeqVD  45658  e2ebindALT  45678  ax6e2ndeqALT  45680  modelaxreplem2  45729  modelaxreplem3  45730  permaxrep  45756  rexsb  47877  nfich1  48237  ichnfimlem  48253  ich2al  48257  pgind  50536