Theorem nfa1 2149

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

Assertion

Ref	Expression
nfa1	⊢ Ⅎ𝑥∀𝑥𝜑

Proof of Theorem nfa1

Step	Hyp	Ref	Expression
1		alex 1829	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		nfe1 2148	. . 3 ⊢ Ⅎ𝑥∃𝑥 ¬ 𝜑
3	2	nfn 1861	. 2 ⊢ Ⅎ𝑥 ¬ ∃𝑥 ¬ 𝜑
4	1, 3	nfxfr 1856	1 ⊢ Ⅎ𝑥∀𝑥𝜑

Syntax hints:  ¬ wn 3  ∀wal 1540  ∃wex 1782  Ⅎwnf 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-10 2138

This theorem depends on definitions:  df-bi 206  df-or 847  df-ex 1783  df-nf 1787

This theorem is referenced by:  nfna1  2150  nfia1  2151  nfnf1  2152  nfs1v  2154  nfa2  2171  sbalex  2236  sbf2  2264  equs5av  2271  nf5  2279  hba1  2290  axc4i  2316  19.12  2321  exsb  2356  equs5aALT  2364  equs5eALT  2365  dral1vOLD  2368  cbv1h  2405  dral1  2439  nfald2  2445  equs5a  2457  equs5e  2458  equs5  2460  axc14  2463  nfsb4t  2499  sbcom3  2506  nfmo1  2552  nfeu1  2583  moexexlem  2623  2eu6  2653  axi12  2702  nfaba1  2912  nfaba1g  2913  nfabdwOLD  2928  nfra1  3282  nfra2wOLD  3298  ceqsalgALT  3509  elrab3t  3683  sbcbi2OLD  3841  csbie2t  3935  rexdifi  4146  sbcnestgfw  4419  sbcnestgf  4424  dfnfc2  4934  mpteq12f  5237  axrep2  5289  axrep3  5290  axrep4  5291  alxfr  5406  axprlem4  5425  axprlem5  5426  copsex2t  5493  mosubopt  5511  fv3  6910  fvmptt  7019  fnoprabg  7531  pssnn  9168  pssnnOLD  9265  fiint  9324  aceq1  10112  zorn2lem4  10494  zfcndrep  10609  mreexexd  17592  fineqvrep  34095  dfon2lem7  34761  bj-alalbial  35579  bj-exalbial  35580  bj-biexal1  35583  bj-bialal  35586  bj-cbv1hv  35674  ax11-pm  35710  bj-snsetex  35844  exlimim  36223  exellim  36225  difunieq  36255  fvineqsneq  36293  wl-nfimf1  36395  wl-nfae1  36396  wl-sb8t  36417  wl-sbnf1  36420  wl-2spsbbi  36430  wl-lem-moexsb  36433  wl-mo2tf  36436  wl-eutf  36438  wl-mo2t  36440  wl-mo3t  36441  wl-sb8eut  36442  wl-ax11-lem3  36449  sbali  36980  setindtr  41763  unielss  41967  ismnushort  43060  axc11next  43165  pm14.122b  43182  pm14.123b  43185  eubiOLD  43195  ax6e2ndeqVD  43670  e2ebindALT  43690  ax6e2ndeqALT  43692  rexsb  45807  nfich1  46115  ichnfimlem  46131  ich2al  46135  pgind  47762