Theorem nfa1 2184

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

Assertion

Ref	Expression
nfa1	⊢ Ⅎ𝑥∀𝑥𝜑

Proof of Theorem nfa1

Step	Hyp	Ref	Expression
1		alex 1845	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		nfe1 2183	. . 3 ⊢ Ⅎ𝑥∃𝑥 ¬ 𝜑
3	2	nfn 1876	. 2 ⊢ Ⅎ𝑥 ¬ ∃𝑥 ¬ 𝜑
4	1, 3	nfxfr 1872	1 ⊢ Ⅎ𝑥∀𝑥𝜑

Syntax hints:  ¬ wn 3  ∀wal 1557  ∃wex 1798  Ⅎwnf 1802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-10 2174

This theorem depends on definitions:  df-bi 209  df-or 859  df-ex 1799  df-nf 1803

This theorem is referenced by:  nfna1  2185  nfia1  2186  nfnf1  2187  nfs1v  2189  nfa2  2208  sbalexOLD  2277  sbf2  2305  equs5av  2310  nf5  2315  hba1  2326  axc4i  2353  19.12  2358  exsb  2389  equs5aALT  2396  equs5eALT  2397  cbv1h  2435  dral1  2469  nfald2  2475  equs5a  2487  equs5e  2488  equs5  2490  axc14  2493  nfsb4t  2529  sbcom3  2536  moexexlem  2652  2eu6  2682  axi12  2731  nfaba1  2931  nfaba1g  2932  nfra1  3285  ceqsalgALT  3489  elrab3t  3649  csbie2t  3890  rexdifi  4103  sbcnestgfw  4374  sbcnestgf  4379  dfnfc2  4886  mpteq12f  5184  axrep2  5229  axrep3  5230  axrep4OLD  5233  alxfr  5363  axprlem4OLD  5386  axprlem5OLD  5387  copsex2t  5460  mosubopt  5478  fv3  6881  fvmptt  6992  fnoprabg  7515  pssnn  9133  fiint  9267  aceq1  10070  zorn2lem4  10453  zfcndrep  10569  mreexexd  17663  dvelimalcased  35334  dvelimexcased  35336  fineqvrep  35374  axsepg4  35403  dfon2lem7  36101  mh-setindnd  36861  bj-alalbial  37140  bj-exalbial  37141  bj-biexal1  37144  bj-bialal  37147  bj-cbv1hv  37245  ax11-pm  37281  bj-snsetex  37412  exlimim  37800  exellim  37802  difunieq  37832  fvineqsneq  37870  wl-nfimf1  37993  wl-nfae1  37994  wl-sb8t  38019  wl-sbnf1  38022  wl-2spsbbi  38032  wl-lem-moexsb  38035  wl-mo2tf  38038  wl-eutf  38040  wl-mo2t  38042  wl-mo3t  38043  wl-sb8eut  38045  sbali  38575  setindtr  43565  unielss  43759  ismnushort  44841  axc11next  44946  pm14.122b  44963  pm14.123b  44966  ax6e2ndeqVD  45448  e2ebindALT  45468  ax6e2ndeqALT  45470  modelaxreplem2  45519  modelaxreplem3  45520  permaxrep  45546  rexsb  47657  nfich1  48017  ichnfimlem  48033  ich2al  48037  pgind  50302