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  4889  mpteq12f  5189  axrep2  5234  axrep3  5235  axrep4OLD  5238  alxfr  5368  axprlem4OLD  5391  axprlem5OLD  5392  copsex2t  5465  mosubopt  5483  fv3  6889  fvmptt  7000  fnoprabg  7523  pssnn  9141  fiint  9274  aceq1  10089  zorn2lem4  10471  zfcndrep  10587  mreexexd  17692  dvelimalcased  35375  dvelimexcased  35377  fineqvrep  35417  axsepg4  35446  dfon2lem7  36145  mh-setindnd  36905  bj-alalbial  37183  bj-exalbial  37184  bj-biexal1  37187  bj-bialal  37190  bj-cbv1hv  37288  ax11-pm  37324  bj-snsetex  37455  exlimim  37843  exellim  37845  difunieq  37875  fvineqsneq  37913  wl-nfimf1  38036  wl-nfae1  38037  wl-sb8t  38062  wl-sbnf1  38065  wl-2spsbbi  38075  wl-lem-moexsb  38078  wl-mo2tf  38081  wl-eutf  38083  wl-mo2t  38085  wl-mo3t  38086  wl-sb8eut  38088  sbali  38618  setindtr  43608  unielss  43802  ismnushort  44870  axc11next  44975  pm14.122b  44992  pm14.123b  44995  ax6e2ndeqVD  45476  e2ebindALT  45496  ax6e2ndeqALT  45498  modelaxreplem2  45547  modelaxreplem3  45548  permaxrep  45574  rexsb  47692  nfich1  48052  ichnfimlem  48068  ich2al  48072  pgind  50347