Theorem nfa1 2156

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 2184. (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 2155	. . 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 2146

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

This theorem is referenced by:  nfna1  2157  nfia1  2158  nfnf1  2159  nfs1v  2161  nfa2  2181  sbalexOLD  2250  sbf2  2278  equs5av  2283  nf5  2288  hba1  2299  axc4i  2327  19.12  2332  exsb  2363  equs5aALT  2370  equs5eALT  2371  cbv1h  2409  dral1  2443  nfald2  2449  equs5a  2461  equs5e  2462  equs5  2464  axc14  2467  nfsb4t  2503  sbcom3  2510  moexexlem  2626  2eu6  2657  axi12  2706  nfaba1  2906  nfaba1OLD  2907  nfaba1g  2908  nfra1  3260  ceqsalgALT  3477  elrab3t  3645  csbie2t  3887  rexdifi  4102  sbcnestgfw  4373  sbcnestgf  4378  dfnfc2  4885  mpteq12f  5183  axrep2  5227  axrep3  5228  axrep4OLD  5231  alxfr  5352  axprlem4OLD  5374  axprlem5OLD  5375  copsex2t  5440  mosubopt  5458  fv3  6852  fvmptt  6961  fnoprabg  7481  pssnn  9093  fiint  9227  aceq1  10027  zorn2lem4  10409  zfcndrep  10525  mreexexd  17571  dvelimalcased  35231  dvelimexcased  35233  fineqvrep  35270  dfon2lem7  35981  mh-setindnd  36667  bj-alalbial  36902  bj-exalbial  36903  bj-biexal1  36906  bj-bialal  36909  bj-cbv1hv  36997  ax11-pm  37033  bj-snsetex  37164  exlimim  37543  exellim  37545  difunieq  37575  fvineqsneq  37613  wl-nfimf1  37727  wl-nfae1  37728  wl-sb8t  37753  wl-sbnf1  37756  wl-2spsbbi  37766  wl-lem-moexsb  37769  wl-mo2tf  37772  wl-eutf  37774  wl-mo2t  37776  wl-mo3t  37777  wl-sb8eut  37779  sbali  38309  setindtr  43262  unielss  43456  ismnushort  44538  axc11next  44643  pm14.122b  44660  pm14.123b  44663  ax6e2ndeqVD  45145  e2ebindALT  45165  ax6e2ndeqALT  45167  modelaxreplem2  45216  modelaxreplem3  45217  permaxrep  45243  rexsb  47341  nfich1  47689  ichnfimlem  47705  ich2al  47709  pgind  49958