Theorem nfa1 2152

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

Assertion

Ref	Expression
nfa1	⊢ Ⅎ𝑥∀𝑥𝜑

Proof of Theorem nfa1

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-10 2141

This theorem depends on definitions:  df-bi 206  df-or 845  df-ex 1787  df-nf 1791

This theorem is referenced by:  nfna1  2153  nfia1  2154  nfnf1  2155  nfs1v  2157  nfa2  2174  sbalex  2239  sbf2  2268  equs5av  2275  nf5  2283  hba1  2294  axc4i  2320  19.12  2325  exsb  2359  equs5aALT  2366  equs5eALT  2367  dral1vOLD  2370  cbv1h  2407  dral1  2441  nfald2  2447  equs5a  2459  equs5e  2460  equs5  2462  axc14  2465  nfsb4t  2505  sbcom3  2512  nfmo1  2559  nfeu1  2590  moexexlem  2630  2eu6  2660  axi12  2709  nfaba1  2917  nfaba1g  2918  nfabdwOLD  2933  nfra1  3145  nfra2w  3154  nfra2wOLD  3155  ceqsalgALT  3464  elrab3t  3625  sbcbi2OLD  3784  csbie2t  3878  rexdifi  4085  sbcnestgfw  4358  sbcnestgf  4363  dfnfc2  4869  mpteq12f  5167  axrep2  5217  axrep3  5218  axrep4  5219  alxfr  5334  axprlem4  5353  axprlem5  5354  copsex2t  5410  mosubopt  5428  fv3  6789  fvmptt  6892  fnoprabg  7392  pssnn  8942  pssnnOLD  9028  fiint  9079  aceq1  9884  zorn2lem4  10266  zfcndrep  10381  mreexexd  17368  fineqvrep  33073  dfon2lem7  33774  bj-alalbial  34892  bj-exalbial  34893  bj-biexal1  34896  bj-bialal  34899  bj-cbv1hv  34987  ax11-pm  35024  bj-snsetex  35162  exlimim  35522  exellim  35524  difunieq  35554  fvineqsneq  35592  wl-nfimf1  35694  wl-nfae1  35695  wl-sb8t  35716  wl-sbnf1  35719  wl-2spsbbi  35729  wl-lem-moexsb  35732  wl-mo2tf  35735  wl-eutf  35737  wl-mo2t  35739  wl-mo3t  35740  wl-sb8eut  35741  wl-ax11-lem3  35747  sbali  36279  setindtr  40855  ismnushort  41901  axc11next  42006  pm14.122b  42023  pm14.123b  42026  eubiOLD  42036  ax6e2ndeqVD  42511  e2ebindALT  42531  ax6e2ndeqALT  42533  rexsb  44570  nfich1  44878  ichnfimlem  44894  ich2al  44898