Theorem nfa1 2151

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 2177. (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 2150	. . 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 2141

This theorem depends on definitions:  df-bi 207  df-or 849  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfna1  2152  nfia1  2153  nfnf1  2154  nfs1v  2156  nfa2  2176  sbalexOLD  2243  sbf2  2272  equs5av  2277  nf5  2282  hba1  2293  axc4i  2322  19.12  2327  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  2913  nfaba1OLD  2914  nfaba1g  2915  nfra1  3284  nfra2wOLD  3300  ceqsalgALT  3518  elrab3t  3691  csbie2t  3937  rexdifi  4150  sbcnestgfw  4421  sbcnestgf  4426  dfnfc2  4929  mpteq12f  5230  axrep2  5282  axrep3  5283  axrep4OLD  5286  alxfr  5407  axprlem4OLD  5429  axprlem5OLD  5430  copsex2t  5497  mosubopt  5515  fv3  6924  fvmptt  7036  fnoprabg  7556  pssnn  9208  fiint  9366  fiintOLD  9367  aceq1  10157  zorn2lem4  10539  zfcndrep  10654  mreexexd  17691  dvelimalcased  35089  dvelimexcased  35091  fineqvrep  35109  dfon2lem7  35790  bj-alalbial  36702  bj-exalbial  36703  bj-biexal1  36706  bj-bialal  36709  bj-cbv1hv  36797  ax11-pm  36833  bj-snsetex  36964  exlimim  37343  exellim  37345  difunieq  37375  fvineqsneq  37413  wl-nfimf1  37527  wl-nfae1  37528  wl-sb8t  37553  wl-sbnf1  37556  wl-2spsbbi  37566  wl-lem-moexsb  37569  wl-mo2tf  37572  wl-eutf  37574  wl-mo2t  37576  wl-mo3t  37577  wl-sb8eut  37579  wl-ax11-lem3  37588  sbali  38119  setindtr  43036  unielss  43230  ismnushort  44320  axc11next  44425  pm14.122b  44442  pm14.123b  44445  eubiOLD  44455  ax6e2ndeqVD  44929  e2ebindALT  44949  ax6e2ndeqALT  44951  modelaxreplem2  44996  modelaxreplem3  44997  rexsb  47111  nfich1  47434  ichnfimlem  47450  ich2al  47454  pgind  49236