Theorem nfa1 2157

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 2185. (Revised by Wolf Lammen, 12-Oct-2021.)

Assertion

Ref	Expression
nfa1	⊢ Ⅎ𝑥∀𝑥𝜑

Proof of Theorem nfa1

Step	Hyp	Ref	Expression
1		alex 1828	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		nfe1 2156	. . 3 ⊢ Ⅎ𝑥∃𝑥 ¬ 𝜑
3	2	nfn 1859	. 2 ⊢ Ⅎ𝑥 ¬ ∃𝑥 ¬ 𝜑
4	1, 3	nfxfr 1855	1 ⊢ Ⅎ𝑥∀𝑥𝜑

Syntax hints:  ¬ wn 3  ∀wal 1540  ∃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 2147

This theorem depends on definitions:  df-bi 207  df-or 849  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfna1  2158  nfia1  2159  nfnf1  2160  nfs1v  2162  nfa2  2182  sbalexOLD  2251  sbf2  2279  equs5av  2284  nf5  2289  hba1  2300  axc4i  2328  19.12  2333  exsb  2364  equs5aALT  2371  equs5eALT  2372  cbv1h  2410  dral1  2444  nfald2  2450  equs5a  2462  equs5e  2463  equs5  2465  axc14  2468  nfsb4t  2504  sbcom3  2511  moexexlem  2627  2eu6  2658  axi12  2707  nfaba1  2907  nfaba1OLD  2908  nfaba1g  2909  nfra1  3262  ceqsalgALT  3479  elrab3t  3647  csbie2t  3889  rexdifi  4104  sbcnestgfw  4375  sbcnestgf  4380  dfnfc2  4887  mpteq12f  5185  axrep2  5229  axrep3  5230  axrep4OLD  5233  alxfr  5354  axprlem4OLD  5376  axprlem5OLD  5377  copsex2t  5448  mosubopt  5466  fv3  6860  fvmptt  6970  fnoprabg  7491  pssnn  9105  fiint  9239  aceq1  10039  zorn2lem4  10421  zfcndrep  10537  mreexexd  17583  dvelimalcased  35250  dvelimexcased  35252  fineqvrep  35289  dfon2lem7  36000  mh-setindnd  36686  bj-alalbial  36940  bj-exalbial  36941  bj-biexal1  36944  bj-bialal  36947  bj-cbv1hv  37038  ax11-pm  37074  bj-snsetex  37205  exlimim  37591  exellim  37593  difunieq  37623  fvineqsneq  37661  wl-nfimf1  37775  wl-nfae1  37776  wl-sb8t  37801  wl-sbnf1  37804  wl-2spsbbi  37814  wl-lem-moexsb  37817  wl-mo2tf  37820  wl-eutf  37822  wl-mo2t  37824  wl-mo3t  37825  wl-sb8eut  37827  sbali  38357  setindtr  43375  unielss  43569  ismnushort  44651  axc11next  44756  pm14.122b  44773  pm14.123b  44776  ax6e2ndeqVD  45258  e2ebindALT  45278  ax6e2ndeqALT  45280  modelaxreplem2  45329  modelaxreplem3  45330  permaxrep  45356  rexsb  47453  nfich1  47801  ichnfimlem  47817  ich2al  47821  pgind  50070