Theorem nfa1 2191

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 2216. (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 2190	. . 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 2180

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

This theorem is used by:  nfna1  2192  nfia1  2193  nfnf1  2194  nfs1v  2196  nfa2  2213  sbf2  2309  equs5av  2314  nf5  2319  hba1  2330  axc4i  2356  19.12  2361  exsb  2391  equs5aALT  2398  equs5eALT  2399  cbv1h  2437  dral1  2471  nfald2  2477  equs5a  2489  equs5e  2490  equs5  2492  axc14  2495  nfsb4t  2531  sbcom3  2538  moexexlem  2654  2eu6  2684  axi12  2733  nfaba1  2934  nfaba1g  2935  nfra1  3290  ceqsalgALT  3490  elrab3t  3647  csbie2t  3889  rexdifi  4089  sbcnestgfw  4382  sbcnestgf  4387  dfnfc2  4892  mpteq12f  5194  axrep2  5239  axrep3  5240  alxfr  5374  copsex2t  5469  mosubopt  5487  mosubott  5489  fv3  6929  fvmptt  7040  fnoprabg  7569  pssnn  9215  fiint  9349  aceq1  10226  zorn2lem4  10607  zfcndrep  10729  mreexexd  17854  dvelimalcased  35788  dvelimexcased  35790  fineqvrep  35895  axsepg4  35924  onprcf1acwevdlem1  36058  srepdflem1  36098  srepdflem2  36099  srepdf  36100  dfon2lem7  36742  mh-setindnd  37516  bj-alalbial  37794  bj-exalbial  37795  bj-biexal1  37798  bj-bialal  37801  bj-cbv1hv  37899  ax11-pm  37935  bj-snsetex  38067  exlimim  38470  exellim  38472  difunieq  38502  fvineqsneq  38540  wl-nfimf1  38663  wl-nfae1  38664  wl-sb8t  38689  wl-sbnf1  38692  wl-2spsbbi  38702  wl-lem-moexsb  38705  wl-mo2tf  38708  wl-eutf  38710  wl-mo2t  38712  wl-mo3t  38713  wl-sb8eut  38715  sbali  39247  setindtr  44235  unielss  44423  ismnushort  45488  axc11next  45593  pm14.122b  45609  pm14.123b  45612  ax6e2ndeqVD  46093  e2ebindALT  46113  ax6e2ndeqALT  46115  modelaxreplem2  46175  modelaxreplem3  46176  permaxrep  46202  rexsb  48385  nfich1  48744  ichnfimlem  48760  ich2al  48764  pgind  51100