Theorem nfa1 2152

Description: The setvar 𝑥 is not free in ∀𝑥𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1782 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 1824	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		nfe1 2151	. . 3 ⊢ Ⅎ𝑥∃𝑥 ¬ 𝜑
3	2	nfn 1856	. 2 ⊢ Ⅎ𝑥 ¬ ∃𝑥 ¬ 𝜑
4	1, 3	nfxfr 1851	1 ⊢ Ⅎ𝑥∀𝑥𝜑

Syntax hints:  ¬ wn 3  ∀wal 1535  ∃wex 1777  Ⅎwnf 1781

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

This theorem depends on definitions:  df-bi 207  df-or 847  df-ex 1778  df-nf 1782

This theorem is referenced by:  nfna1  2153  nfia1  2154  nfnf1  2155  nfs1v  2157  nfa2  2177  sbalexOLD  2244  sbf2  2273  equs5av  2280  nf5  2286  hba1  2297  axc4i  2326  19.12  2331  exsb  2365  equs5aALT  2372  equs5eALT  2373  dral1vOLD  2376  cbv1h  2413  dral1  2447  nfald2  2453  equs5a  2465  equs5e  2466  equs5  2468  axc14  2471  nfsb4t  2507  sbcom3  2514  nfmo1  2560  nfeu1  2591  moexexlem  2629  2eu6  2660  axi12  2709  nfaba1  2916  nfaba1OLD  2917  nfaba1g  2918  nfabdwOLD  2933  nfra1  3290  nfra2wOLD  3306  ceqsalgALT  3526  elrab3t  3707  csbie2t  3962  rexdifi  4173  sbcnestgfw  4444  sbcnestgf  4449  dfnfc2  4953  mpteq12f  5254  axrep2  5306  axrep3  5307  axrep4  5308  alxfr  5425  axprlem4  5444  axprlem5  5445  copsex2t  5512  mosubopt  5529  fv3  6938  fvmptt  7049  fnoprabg  7573  pssnn  9234  fiint  9394  fiintOLD  9395  aceq1  10186  zorn2lem4  10568  zfcndrep  10683  mreexexd  17706  dvelimalcased  35051  dvelimexcased  35053  fineqvrep  35071  dfon2lem7  35753  bj-alalbial  36667  bj-exalbial  36668  bj-biexal1  36671  bj-bialal  36674  bj-cbv1hv  36762  ax11-pm  36798  bj-snsetex  36929  exlimim  37308  exellim  37310  difunieq  37340  fvineqsneq  37378  wl-nfimf1  37480  wl-nfae1  37481  wl-sb8t  37506  wl-sbnf1  37509  wl-2spsbbi  37519  wl-lem-moexsb  37522  wl-mo2tf  37525  wl-eutf  37527  wl-mo2t  37529  wl-mo3t  37530  wl-sb8eut  37532  wl-ax11-lem3  37541  sbali  38072  setindtr  42981  unielss  43179  ismnushort  44270  axc11next  44375  pm14.122b  44392  pm14.123b  44395  eubiOLD  44405  ax6e2ndeqVD  44880  e2ebindALT  44900  ax6e2ndeqALT  44902  rexsb  47014  nfich1  47321  ichnfimlem  47337  ich2al  47341  pgind  48809