Theorem nfa1 2188

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

This proof depends on syntax axioms:  ¬ wn 3  ∀wal 1568  ∃wex 1812  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-10 2178

This proof depends on definitions:  df-bi 210  df-or 862  df-ex 1813  df-nf 1817

This theorem is used by:  nfna1  2189  nfia1  2190  nfnf1  2191  nfs1v  2193  nfa2  2212  sbf2  2307  equs5av  2312  nf5  2317  hba1  2328  axc4i  2354  19.12  2359  exsb  2390  equs5aALT  2397  equs5eALT  2398  cbv1h  2436  dral1  2470  nfald2  2476  equs5a  2488  equs5e  2489  equs5  2491  axc14  2494  nfsb4t  2530  sbcom3  2537  moexexlem  2653  2eu6  2683  axi12  2732  nfaba1  2932  nfaba1g  2933  nfra1  3288  ceqsalgALT  3489  elrab3t  3647  csbie2t  3888  rexdifi  4100  sbcnestgfw  4382  sbcnestgf  4387  dfnfc2  4892  mpteq12f  5194  axrep2  5239  axrep3  5240  axrep4OLD  5243  alxfr  5376  axprlem4OLD  5399  axprlem5OLD  5400  copsex2t  5473  mosubopt  5491  fv3  6900  fvmptt  7011  fnoprabg  7540  pssnn  9167  fiint  9300  aceq1  10124  zorn2lem4  10505  zfcndrep  10627  mreexexd  17742  dvelimalcased  35592  dvelimexcased  35594  fineqvrep  35648  axsepg4  35677  dfon2lem7  36374  mh-setindnd  37164  bj-alalbial  37442  bj-exalbial  37443  bj-biexal1  37446  bj-bialal  37449  bj-cbv1hv  37547  ax11-pm  37583  bj-snsetex  37715  exlimim  38104  exellim  38106  difunieq  38136  fvineqsneq  38174  wl-nfimf1  38297  wl-nfae1  38298  wl-sb8t  38323  wl-sbnf1  38326  wl-2spsbbi  38336  wl-lem-moexsb  38339  wl-mo2tf  38342  wl-eutf  38344  wl-mo2t  38346  wl-mo3t  38347  wl-sb8eut  38349  sbali  38868  setindtr  43873  unielss  44067  ismnushort  45133  axc11next  45238  pm14.122b  45255  pm14.123b  45258  ax6e2ndeqVD  45739  e2ebindALT  45759  ax6e2ndeqALT  45761  modelaxreplem2  45810  modelaxreplem3  45811  permaxrep  45837  rexsb  47995  nfich1  48355  ichnfimlem  48371  ich2al  48375  pgind  50651