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  2273  equs5av  2278  nf5  2283  hba1  2294  axc4i  2323  19.12  2328  exsb  2362  equs5aALT  2369  equs5eALT  2370  dral1vOLD  2373  cbv1h  2410  dral1  2444  nfald2  2450  equs5a  2462  equs5e  2463  equs5  2465  axc14  2468  nfsb4t  2504  sbcom3  2511  nfmo1  2557  nfeu1  2588  moexexlem  2626  2eu6  2657  axi12  2706  nfaba1  2907  nfaba1OLD  2908  nfaba1g  2909  nfra1  3270  ceqsalgALT  3502  elrab3t  3675  csbie2t  3917  rexdifi  4130  sbcnestgfw  4401  sbcnestgf  4406  dfnfc2  4910  mpteq12f  5210  axrep2  5257  axrep3  5258  axrep4OLD  5261  alxfr  5382  axprlem4OLD  5404  axprlem5OLD  5405  copsex2t  5472  mosubopt  5490  fv3  6899  fvmptt  7011  fnoprabg  7535  pssnn  9187  fiint  9343  fiintOLD  9344  aceq1  10136  zorn2lem4  10518  zfcndrep  10633  mreexexd  17665  dvelimalcased  35111  dvelimexcased  35113  fineqvrep  35131  dfon2lem7  35812  bj-alalbial  36724  bj-exalbial  36725  bj-biexal1  36728  bj-bialal  36731  bj-cbv1hv  36819  ax11-pm  36855  bj-snsetex  36986  exlimim  37365  exellim  37367  difunieq  37397  fvineqsneq  37435  wl-nfimf1  37549  wl-nfae1  37550  wl-sb8t  37575  wl-sbnf1  37578  wl-2spsbbi  37588  wl-lem-moexsb  37591  wl-mo2tf  37594  wl-eutf  37596  wl-mo2t  37598  wl-mo3t  37599  wl-sb8eut  37601  wl-ax11-lem3  37610  sbali  38141  setindtr  43015  unielss  43209  ismnushort  44292  axc11next  44397  pm14.122b  44414  pm14.123b  44417  eubiOLD  44427  ax6e2ndeqVD  44900  e2ebindALT  44920  ax6e2ndeqALT  44922  modelaxreplem2  44971  modelaxreplem3  44972  permaxrep  44998  rexsb  47095  nfich1  47428  ichnfimlem  47444  ich2al  47448  pgind  49548