Theorem nfa1 2188

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

Assertion

Ref	Expression
nfa1	⊢ Ⅎ𝑥∀𝑥𝜑

Proof of Theorem nfa1

Step	Hyp	Ref	Expression
1		alex 1849	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		nfe1 2187	. . 3 ⊢ Ⅎ𝑥∃𝑥 ¬ 𝜑
3	2	nfn 1880	. 2 ⊢ Ⅎ𝑥 ¬ ∃𝑥 ¬ 𝜑
4	1, 3	nfxfr 1876	1 ⊢ Ⅎ𝑥∀𝑥𝜑

Syntax hints:  ¬ wn 3  ∀wal 1561  ∃wex 1802  Ⅎwnf 1806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-10 2178

This theorem depends on definitions:  df-bi 210  df-or 861  df-ex 1803  df-nf 1807

This theorem is referenced by:  nfna1  2189  nfia1  2190  nfnf1  2191  nfs1v  2193  nfa2  2212  sbalexOLD  2281  sbf2  2309  equs5av  2314  nf5  2319  hba1  2330  axc4i  2357  19.12  2362  exsb  2393  equs5aALT  2400  equs5eALT  2401  cbv1h  2439  dral1  2473  nfald2  2479  equs5a  2491  equs5e  2492  equs5  2494  axc14  2497  nfsb4t  2533  sbcom3  2540  moexexlem  2656  2eu6  2686  axi12  2735  nfaba1  2935  nfaba1g  2936  nfra1  3289  ceqsalgALT  3493  elrab3t  3652  csbie2t  3893  rexdifi  4106  sbcnestgfw  4378  sbcnestgf  4383  dfnfc2  4890  mpteq12f  5190  axrep2  5235  axrep3  5236  axrep4OLD  5239  alxfr  5369  axprlem4OLD  5392  axprlem5OLD  5393  copsex2t  5466  mosubopt  5484  fv3  6889  fvmptt  7000  fnoprabg  7523  pssnn  9141  fiint  9274  aceq1  10089  zorn2lem4  10471  zfcndrep  10587  mreexexd  17694  dvelimalcased  35380  dvelimexcased  35382  fineqvrep  35422  axsepg4  35451  dfon2lem7  36150  mh-setindnd  36910  bj-alalbial  37188  bj-exalbial  37189  bj-biexal1  37192  bj-bialal  37195  bj-cbv1hv  37293  ax11-pm  37329  bj-snsetex  37460  exlimim  37848  exellim  37850  difunieq  37880  fvineqsneq  37918  wl-nfimf1  38041  wl-nfae1  38042  wl-sb8t  38067  wl-sbnf1  38070  wl-2spsbbi  38080  wl-lem-moexsb  38083  wl-mo2tf  38086  wl-eutf  38088  wl-mo2t  38090  wl-mo3t  38091  wl-sb8eut  38093  sbali  38623  setindtr  43613  unielss  43807  ismnushort  44875  axc11next  44980  pm14.122b  44997  pm14.123b  45000  ax6e2ndeqVD  45482  e2ebindALT  45502  ax6e2ndeqALT  45504  modelaxreplem2  45553  modelaxreplem3  45554  permaxrep  45580  rexsb  47691  nfich1  48051  ichnfimlem  48067  ich2al  48071  pgind  50346