Theorem nfa1 2187

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

Assertion

Ref	Expression
nfa1	⊢ Ⅎ𝑥∀𝑥𝜑

Proof of Theorem nfa1

Step	Hyp	Ref	Expression
1		alex 1858	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		nfe1 2186	. . 3 ⊢ Ⅎ𝑥∃𝑥 ¬ 𝜑
3	2	nfn 1889	. 2 ⊢ Ⅎ𝑥 ¬ ∃𝑥 ¬ 𝜑
4	1, 3	nfxfr 1885	1 ⊢ Ⅎ𝑥∀𝑥𝜑

This proof depends on syntax axioms:  ¬ wn 3  ∀wal 1567  ∃wex 1811  Ⅎwnf 1815

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-10 2177

This proof depends on definitions:  df-bi 210  df-or 862  df-ex 1812  df-nf 1816

This theorem is used by:  nfna1  2188  nfia1  2189  nfnf1  2190  nfs1v  2192  nfa2  2209  sbf2  2305  equs5av  2310  nf5  2315  hba1  2326  axc4i  2352  19.12  2357  exsb  2388  equs5aALT  2395  equs5eALT  2396  cbv1h  2434  dral1  2468  nfald2  2474  equs5a  2486  equs5e  2487  equs5  2489  axc14  2492  nfsb4t  2528  sbcom3  2535  moexexlem  2651  2eu6  2681  axi12  2730  nfaba1  2930  nfaba1g  2931  nfra1  3286  ceqsalgALT  3486  elrab3t  3643  csbie2t  3884  rexdifi  4086  sbcnestgfw  4378  sbcnestgf  4383  dfnfc2  4888  mpteq12f  5189  axrep2  5234  axrep3  5235  alxfr  5368  copsex2t  5463  mosubopt  5481  mosubott  5483  fv3  6904  fvmptt  7015  fnoprabg  7544  pssnn  9188  fiint  9322  aceq1  10200  zorn2lem4  10581  zfcndrep  10703  mreexexd  17828  dvelimalcased  35752  dvelimexcased  35754  fineqvrep  35839  axsepg4  35868  onprcf1acwevdlem1  35965  srepdflem1  36005  srepdflem2  36006  srepdf  36007  dfon2lem7  36644  mh-setindnd  37418  bj-alalbial  37696  bj-exalbial  37697  bj-biexal1  37700  bj-bialal  37703  bj-cbv1hv  37801  ax11-pm  37837  bj-snsetex  37969  exlimim  38359  exellim  38361  difunieq  38391  fvineqsneq  38429  wl-nfimf1  38552  wl-nfae1  38553  wl-sb8t  38578  wl-sbnf1  38581  wl-2spsbbi  38591  wl-lem-moexsb  38594  wl-mo2tf  38597  wl-eutf  38599  wl-mo2t  38601  wl-mo3t  38602  wl-sb8eut  38604  sbali  39138  setindtr  44125  unielss  44314  ismnushort  45379  axc11next  45484  pm14.122b  45501  pm14.123b  45504  ax6e2ndeqVD  45985  e2ebindALT  46005  ax6e2ndeqALT  46007  modelaxreplem2  46063  modelaxreplem3  46064  permaxrep  46090  rexsb  48263  nfich1  48623  ichnfimlem  48639  ich2al  48643  pgind  50979