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  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  3261  ceqsalgALT  3466  elrab3t  3633  csbie2t  3875  rexdifi  4090  sbcnestgfw  4361  sbcnestgf  4366  dfnfc2  4872  mpteq12f  5170  axrep2  5215  axrep3  5216  axrep4OLD  5219  alxfr  5349  axprlem4OLD  5372  axprlem5OLD  5373  copsex2t  5446  mosubopt  5464  fv3  6858  fvmptt  6968  fnoprabg  7490  pssnn  9103  fiint  9237  aceq1  10039  zorn2lem4  10421  zfcndrep  10537  mreexexd  17614  dvelimalcased  35217  dvelimexcased  35219  fineqvrep  35258  dfon2lem7  35969  mh-setindnd  36719  bj-alalbial  36998  bj-exalbial  36999  bj-biexal1  37002  bj-bialal  37005  bj-cbv1hv  37103  ax11-pm  37139  bj-snsetex  37270  exlimim  37658  exellim  37660  difunieq  37690  fvineqsneq  37728  wl-nfimf1  37851  wl-nfae1  37852  wl-sb8t  37877  wl-sbnf1  37880  wl-2spsbbi  37890  wl-lem-moexsb  37893  wl-mo2tf  37896  wl-eutf  37898  wl-mo2t  37900  wl-mo3t  37901  wl-sb8eut  37903  sbali  38433  setindtr  43452  unielss  43646  ismnushort  44728  axc11next  44833  pm14.122b  44850  pm14.123b  44853  ax6e2ndeqVD  45335  e2ebindALT  45355  ax6e2ndeqALT  45357  modelaxreplem2  45406  modelaxreplem3  45407  permaxrep  45433  rexsb  47547  nfich1  47907  ichnfimlem  47923  ich2al  47927  pgind  50192