Theorem nfa1 2152

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

Assertion

Ref	Expression
nfa1	⊢ Ⅎ𝑥∀𝑥𝜑

Proof of Theorem nfa1

Step	Hyp	Ref	Expression
1		alex 1826	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		nfe1 2151	. . 3 ⊢ Ⅎ𝑥∃𝑥 ¬ 𝜑
3	2	nfn 1857	. 2 ⊢ Ⅎ𝑥 ¬ ∃𝑥 ¬ 𝜑
4	1, 3	nfxfr 1853	1 ⊢ Ⅎ𝑥∀𝑥𝜑

Syntax hints:  ¬ wn 3  ∀wal 1538  ∃wex 1779  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-10 2142

This theorem depends on definitions:  df-bi 207  df-or 848  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfna1  2153  nfia1  2154  nfnf1  2155  nfs1v  2157  nfa2  2177  sbalexOLD  2244  sbf2  2272  equs5av  2277  nf5  2282  hba1  2293  axc4i  2321  19.12  2326  exsb  2357  equs5aALT  2364  equs5eALT  2365  cbv1h  2403  dral1  2437  nfald2  2443  equs5a  2455  equs5e  2456  equs5  2458  axc14  2461  nfsb4t  2497  sbcom3  2504  nfmo1  2550  nfeu1  2581  moexexlem  2619  2eu6  2650  axi12  2699  nfaba1  2899  nfaba1OLD  2900  nfaba1g  2901  nfra1  3253  ceqsalgALT  3473  elrab3t  3647  csbie2t  3889  rexdifi  4101  sbcnestgfw  4372  sbcnestgf  4377  dfnfc2  4880  mpteq12f  5177  axrep2  5221  axrep3  5222  axrep4OLD  5225  alxfr  5346  axprlem4OLD  5368  axprlem5OLD  5369  copsex2t  5435  mosubopt  5453  fv3  6840  fvmptt  6950  fnoprabg  7472  pssnn  9082  fiint  9216  fiintOLD  9217  aceq1  10011  zorn2lem4  10393  zfcndrep  10508  mreexexd  17554  dvelimalcased  35048  dvelimexcased  35050  fineqvrep  35076  dfon2lem7  35773  bj-alalbial  36685  bj-exalbial  36686  bj-biexal1  36689  bj-bialal  36692  bj-cbv1hv  36780  ax11-pm  36816  bj-snsetex  36947  exlimim  37326  exellim  37328  difunieq  37358  fvineqsneq  37396  wl-nfimf1  37510  wl-nfae1  37511  wl-sb8t  37536  wl-sbnf1  37539  wl-2spsbbi  37549  wl-lem-moexsb  37552  wl-mo2tf  37555  wl-eutf  37557  wl-mo2t  37559  wl-mo3t  37560  wl-sb8eut  37562  wl-ax11-lem3  37571  sbali  38102  setindtr  43007  unielss  43201  ismnushort  44284  axc11next  44389  pm14.122b  44406  pm14.123b  44409  eubiOLD  44419  ax6e2ndeqVD  44892  e2ebindALT  44912  ax6e2ndeqALT  44914  modelaxreplem2  44963  modelaxreplem3  44964  permaxrep  44990  rexsb  47093  nfich1  47441  ichnfimlem  47457  ich2al  47461  pgind  49712