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  3261  ceqsalgALT  3484  elrab3t  3658  csbie2t  3900  rexdifi  4113  sbcnestgfw  4384  sbcnestgf  4389  dfnfc2  4893  mpteq12f  5192  axrep2  5237  axrep3  5238  axrep4OLD  5241  alxfr  5362  axprlem4OLD  5384  axprlem5OLD  5385  copsex2t  5452  mosubopt  5470  fv3  6876  fvmptt  6988  fnoprabg  7512  pssnn  9132  fiint  9277  fiintOLD  9278  aceq1  10070  zorn2lem4  10452  zfcndrep  10567  mreexexd  17609  dvelimalcased  35065  dvelimexcased  35067  fineqvrep  35085  dfon2lem7  35777  bj-alalbial  36689  bj-exalbial  36690  bj-biexal1  36693  bj-bialal  36696  bj-cbv1hv  36784  ax11-pm  36820  bj-snsetex  36951  exlimim  37330  exellim  37332  difunieq  37362  fvineqsneq  37400  wl-nfimf1  37514  wl-nfae1  37515  wl-sb8t  37540  wl-sbnf1  37543  wl-2spsbbi  37553  wl-lem-moexsb  37556  wl-mo2tf  37559  wl-eutf  37561  wl-mo2t  37563  wl-mo3t  37564  wl-sb8eut  37566  wl-ax11-lem3  37575  sbali  38106  setindtr  43013  unielss  43207  ismnushort  44290  axc11next  44395  pm14.122b  44412  pm14.123b  44415  eubiOLD  44425  ax6e2ndeqVD  44898  e2ebindALT  44918  ax6e2ndeqALT  44920  modelaxreplem2  44969  modelaxreplem3  44970  permaxrep  44996  rexsb  47097  nfich1  47445  ichnfimlem  47461  ich2al  47465  pgind  49703