Theorem nfa1 2162

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

Assertion

Ref	Expression
nfa1	⊢ Ⅎ𝑥∀𝑥𝜑

Proof of Theorem nfa1

Step	Hyp	Ref	Expression
1		alex 1833	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		nfe1 2161	. . 3 ⊢ Ⅎ𝑥∃𝑥 ¬ 𝜑
3	2	nfn 1864	. 2 ⊢ Ⅎ𝑥 ¬ ∃𝑥 ¬ 𝜑
4	1, 3	nfxfr 1860	1 ⊢ Ⅎ𝑥∀𝑥𝜑

Syntax hints:  ¬ wn 3  ∀wal 1545  ∃wex 1786  Ⅎwnf 1790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-10 2152

This theorem depends on definitions:  df-bi 208  df-or 854  df-ex 1787  df-nf 1791

This theorem is referenced by:  nfna1  2163  nfia1  2164  nfnf1  2165  nfs1v  2167  nfa2  2186  sbalexOLD  2255  sbf2  2283  equs5av  2288  nf5  2293  hba1  2304  axc4i  2331  19.12  2336  exsb  2367  equs5aALT  2374  equs5eALT  2375  cbv1h  2413  dral1  2447  nfald2  2453  equs5a  2465  equs5e  2466  equs5  2468  axc14  2471  nfsb4t  2507  sbcom3  2514  moexexlem  2630  2eu6  2661  axi12  2710  nfaba1  2910  nfaba1g  2911  nfra1  3264  ceqsalgALT  3469  elrab3t  3635  csbie2t  3876  rexdifi  4087  sbcnestgfw  4356  sbcnestgf  4361  dfnfc2  4867  mpteq12f  5164  axrep2  5209  axrep3  5210  axrep4OLD  5213  alxfr  5343  axprlem4OLD  5366  axprlem5OLD  5367  copsex2t  5440  mosubopt  5458  fv3  6852  fvmptt  6963  fnoprabg  7486  pssnn  9100  fiint  9234  aceq1  10037  zorn2lem4  10419  zfcndrep  10535  mreexexd  17612  dvelimalcased  35264  dvelimexcased  35266  fineqvrep  35302  axsepg4  35331  dfon2lem7  36022  mh-setindnd  36772  bj-alalbial  37051  bj-exalbial  37052  bj-biexal1  37055  bj-bialal  37058  bj-cbv1hv  37156  ax11-pm  37192  bj-snsetex  37323  exlimim  37711  exellim  37713  difunieq  37743  fvineqsneq  37781  wl-nfimf1  37904  wl-nfae1  37905  wl-sb8t  37930  wl-sbnf1  37933  wl-2spsbbi  37943  wl-lem-moexsb  37946  wl-mo2tf  37949  wl-eutf  37951  wl-mo2t  37953  wl-mo3t  37954  wl-sb8eut  37956  sbali  38486  setindtr  43476  unielss  43670  ismnushort  44752  axc11next  44857  pm14.122b  44874  pm14.123b  44877  ax6e2ndeqVD  45359  e2ebindALT  45379  ax6e2ndeqALT  45381  modelaxreplem2  45430  modelaxreplem3  45431  permaxrep  45457  rexsb  47569  nfich1  47929  ichnfimlem  47945  ich2al  47949  pgind  50214