Theorem nfa1 2152

Description: The setvar 𝑥 is not free in ∀𝑥𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1786 changed. (Revised by Wolf Lammen, 11-Sep-2021.) Remove dependency on ax-12 2175. (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 2151	. . 3 ⊢ Ⅎ𝑥∃𝑥 ¬ 𝜑
3	2	nfn 1858	. 2 ⊢ Ⅎ𝑥 ¬ ∃𝑥 ¬ 𝜑
4	1, 3	nfxfr 1854	1 ⊢ Ⅎ𝑥∀𝑥𝜑

Syntax hints:  ¬ wn 3  ∀wal 1536  ∃wex 1781  Ⅎwnf 1785

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

This theorem depends on definitions:  df-bi 210  df-or 845  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfna1  2153  nfia1  2154  nfnf1  2155  nfs1v  2157  nfa2  2174  sbf2  2269  sb56OLD  2275  equs5av  2276  nf5  2286  hba1  2297  axc4i  2330  19.12  2335  exsb  2367  equs5aALT  2373  equs5eALT  2374  dral1v  2376  cbv1h  2414  dral1  2450  nfald2  2456  equs5a  2469  equs5e  2470  equs5  2472  axc14  2475  nfsb4t  2517  sbcom3  2525  nfsb4tALT  2580  nfmo1  2616  nfeu1  2649  moexexlem  2688  2eu6  2719  axi12  2768  nfaba1  2963  nfaba1g  2964  nfabdw  2976  nfra1  3183  ceqsalgALT  3477  elrab3t  3627  sbcbi2OLD  3779  csbie2t  3866  rexdifi  4073  sbcnestgfw  4326  sbcnestgf  4331  dfnfc2  4822  mpteq12f  5113  axrep2  5157  axrep3  5158  axrep4  5159  alxfr  5273  axprlem4  5292  axprlem5  5293  copsex2t  5348  mosubopt  5365  fv3  6663  fvmptt  6765  fnoprabg  7254  pssnn  8720  fiint  8779  aceq1  9528  zorn2lem4  9910  zfcndrep  10025  mreexexd  16911  dfon2lem7  33147  bj-alalbial  34148  bj-exalbial  34149  bj-biexal1  34152  bj-bialal  34155  bj-cbv1hv  34233  ax11-pm  34270  bj-snsetex  34399  exlimim  34759  exellim  34761  difunieq  34791  fvineqsneq  34829  wl-nfimf1  34931  wl-nfae1  34932  wl-sb8t  34953  wl-sbnf1  34956  wl-2spsbbi  34966  wl-lem-moexsb  34969  wl-mo2tf  34972  wl-eutf  34974  wl-mo2t  34976  wl-mo3t  34977  wl-sb8eut  34978  wl-ax11-lem3  34984  sbali  35550  setindtr  39965  axc11next  41110  pm14.122b  41127  pm14.123b  41130  eubiOLD  41140  ax6e2ndeqVD  41615  e2ebindALT  41635  ax6e2ndeqALT  41637  rexsb  43654  nfich1  43964  ichnfimlem  43980  ich2al  43984