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  3467  elrab3t  3634  csbie2t  3876  rexdifi  4091  sbcnestgfw  4362  sbcnestgf  4367  dfnfc2  4873  mpteq12f  5171  axrep2  5215  axrep3  5216  axrep4OLD  5219  alxfr  5344  axprlem4OLD  5367  axprlem5OLD  5368  copsex2t  5440  mosubopt  5458  fv3  6852  fvmptt  6962  fnoprabg  7483  pssnn  9096  fiint  9230  aceq1  10030  zorn2lem4  10412  zfcndrep  10528  mreexexd  17605  dvelimalcased  35233  dvelimexcased  35235  fineqvrep  35274  dfon2lem7  35985  mh-setindnd  36735  bj-alalbial  37014  bj-exalbial  37015  bj-biexal1  37018  bj-bialal  37021  bj-cbv1hv  37119  ax11-pm  37155  bj-snsetex  37286  exlimim  37672  exellim  37674  difunieq  37704  fvineqsneq  37742  wl-nfimf1  37865  wl-nfae1  37866  wl-sb8t  37891  wl-sbnf1  37894  wl-2spsbbi  37904  wl-lem-moexsb  37907  wl-mo2tf  37910  wl-eutf  37912  wl-mo2t  37914  wl-mo3t  37915  wl-sb8eut  37917  sbali  38447  setindtr  43470  unielss  43664  ismnushort  44746  axc11next  44851  pm14.122b  44868  pm14.123b  44871  ax6e2ndeqVD  45353  e2ebindALT  45373  ax6e2ndeqALT  45375  modelaxreplem2  45424  modelaxreplem3  45425  permaxrep  45451  rexsb  47559  nfich1  47919  ichnfimlem  47935  ich2al  47939  pgind  50204