Theorem nfa1 2152

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

Assertion

Ref	Expression
nfa1	⊢ Ⅎ𝑥∀𝑥𝜑

Proof of Theorem nfa1

Step	Hyp	Ref	Expression
1		alex 1826	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		nfe1 2151	. . 3 ⊢ Ⅎ𝑥∃𝑥 ¬ 𝜑
3	2	nfn 1857	. 2 ⊢ Ⅎ𝑥 ¬ ∃𝑥 ¬ 𝜑
4	1, 3	nfxfr 1853	1 ⊢ Ⅎ𝑥∀𝑥𝜑

Syntax hints:  ¬ wn 3  ∀wal 1538  ∃wex 1779  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-10 2142

This theorem depends on definitions:  df-bi 207  df-or 848  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfna1  2153  nfia1  2154  nfnf1  2155  nfs1v  2157  nfa2  2177  sbalexOLD  2244  sbf2  2272  equs5av  2277  nf5  2282  hba1  2293  axc4i  2321  19.12  2326  exsb  2357  equs5aALT  2364  equs5eALT  2365  cbv1h  2403  dral1  2437  nfald2  2443  equs5a  2455  equs5e  2456  equs5  2458  axc14  2461  nfsb4t  2497  sbcom3  2504  nfmo1  2550  nfeu1  2581  moexexlem  2619  2eu6  2650  axi12  2699  nfaba1  2899  nfaba1OLD  2900  nfaba1g  2901  nfra1  3253  ceqsalgALT  3475  elrab3t  3649  csbie2t  3891  rexdifi  4103  sbcnestgfw  4374  sbcnestgf  4379  dfnfc2  4883  mpteq12f  5180  axrep2  5224  axrep3  5225  axrep4OLD  5228  alxfr  5349  axprlem4OLD  5371  axprlem5OLD  5372  copsex2t  5439  mosubopt  5457  fv3  6844  fvmptt  6954  fnoprabg  7476  pssnn  9092  fiint  9235  fiintOLD  9236  aceq1  10030  zorn2lem4  10412  zfcndrep  10527  mreexexd  17572  dvelimalcased  35041  dvelimexcased  35043  fineqvrep  35069  dfon2lem7  35762  bj-alalbial  36674  bj-exalbial  36675  bj-biexal1  36678  bj-bialal  36681  bj-cbv1hv  36769  ax11-pm  36805  bj-snsetex  36936  exlimim  37315  exellim  37317  difunieq  37347  fvineqsneq  37385  wl-nfimf1  37499  wl-nfae1  37500  wl-sb8t  37525  wl-sbnf1  37528  wl-2spsbbi  37538  wl-lem-moexsb  37541  wl-mo2tf  37544  wl-eutf  37546  wl-mo2t  37548  wl-mo3t  37549  wl-sb8eut  37551  wl-ax11-lem3  37560  sbali  38091  setindtr  42997  unielss  43191  ismnushort  44274  axc11next  44379  pm14.122b  44396  pm14.123b  44399  eubiOLD  44409  ax6e2ndeqVD  44882  e2ebindALT  44902  ax6e2ndeqALT  44904  modelaxreplem2  44953  modelaxreplem3  44954  permaxrep  44980  rexsb  47084  nfich1  47432  ichnfimlem  47448  ich2al  47452  pgind  49703