Theorem nfa1 2154

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

Assertion

Ref	Expression
nfa1	⊢ Ⅎ𝑥∀𝑥𝜑

Proof of Theorem nfa1

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

Syntax hints:  ¬ wn 3  ∀wal 1539  ∃wex 1780  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-10 2144

This theorem depends on definitions:  df-bi 207  df-or 848  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfna1  2155  nfia1  2156  nfnf1  2157  nfs1v  2159  nfa2  2179  sbalexOLD  2246  sbf2  2274  equs5av  2279  nf5  2284  hba1  2295  axc4i  2323  19.12  2328  exsb  2359  equs5aALT  2366  equs5eALT  2367  cbv1h  2405  dral1  2439  nfald2  2445  equs5a  2457  equs5e  2458  equs5  2460  axc14  2463  nfsb4t  2499  sbcom3  2506  nfmo1  2552  nfeu1  2583  moexexlem  2621  2eu6  2652  axi12  2701  nfaba1  2902  nfaba1OLD  2903  nfaba1g  2904  nfra1  3256  ceqsalgALT  3473  elrab3t  3646  csbie2t  3888  rexdifi  4100  sbcnestgfw  4371  sbcnestgf  4376  dfnfc2  4881  mpteq12f  5176  axrep2  5220  axrep3  5221  axrep4OLD  5224  alxfr  5345  axprlem4OLD  5367  axprlem5OLD  5368  copsex2t  5432  mosubopt  5450  fv3  6840  fvmptt  6949  fnoprabg  7469  pssnn  9078  fiint  9211  aceq1  10005  zorn2lem4  10387  zfcndrep  10502  mreexexd  17551  dvelimalcased  35082  dvelimexcased  35084  fineqvrep  35125  dfon2lem7  35822  bj-alalbial  36734  bj-exalbial  36735  bj-biexal1  36738  bj-bialal  36741  bj-cbv1hv  36829  ax11-pm  36865  bj-snsetex  36996  exlimim  37375  exellim  37377  difunieq  37407  fvineqsneq  37445  wl-nfimf1  37559  wl-nfae1  37560  wl-sb8t  37585  wl-sbnf1  37588  wl-2spsbbi  37598  wl-lem-moexsb  37601  wl-mo2tf  37604  wl-eutf  37606  wl-mo2t  37608  wl-mo3t  37609  wl-sb8eut  37611  wl-ax11-lem3  37620  sbali  38151  setindtr  43056  unielss  43250  ismnushort  44333  axc11next  44438  pm14.122b  44455  pm14.123b  44458  ax6e2ndeqVD  44940  e2ebindALT  44960  ax6e2ndeqALT  44962  modelaxreplem2  45011  modelaxreplem3  45012  permaxrep  45038  rexsb  47129  nfich1  47477  ichnfimlem  47493  ich2al  47497  pgind  49748