Theorem nfa1 2150

Description: The setvar 𝑥 is not free in ∀𝑥𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1788 changed. (Revised by Wolf Lammen, 11-Sep-2021.) Remove dependency on ax-12 2173. (Revised by Wolf Lammen, 12-Oct-2021.)

Assertion

Ref	Expression
nfa1	⊢ Ⅎ𝑥∀𝑥𝜑

Proof of Theorem nfa1

Step	Hyp	Ref	Expression
1		alex 1829	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		nfe1 2149	. . 3 ⊢ Ⅎ𝑥∃𝑥 ¬ 𝜑
3	2	nfn 1861	. 2 ⊢ Ⅎ𝑥 ¬ ∃𝑥 ¬ 𝜑
4	1, 3	nfxfr 1856	1 ⊢ Ⅎ𝑥∀𝑥𝜑

Syntax hints:  ¬ wn 3  ∀wal 1537  ∃wex 1783  Ⅎwnf 1787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-10 2139

This theorem depends on definitions:  df-bi 206  df-or 844  df-ex 1784  df-nf 1788

This theorem is referenced by:  nfna1  2151  nfia1  2152  nfnf1  2153  nfs1v  2155  nfa2  2172  sbalex  2238  sbf2  2267  equs5av  2274  nf5  2282  hba1  2293  axc4i  2320  19.12  2325  exsb  2357  equs5aALT  2364  equs5eALT  2365  dral1vOLD  2368  cbv1h  2405  dral1  2439  nfald2  2445  equs5a  2457  equs5e  2458  equs5  2460  axc14  2463  nfsb4t  2503  sbcom3  2510  nfmo1  2557  nfeu1  2588  moexexlem  2628  2eu6  2658  axi12  2707  nfaba1  2914  nfaba1g  2915  nfabdwOLD  2930  nfra1  3142  nfra2w  3151  nfra2wOLD  3152  ceqsalgALT  3455  elrab3t  3616  sbcbi2OLD  3775  csbie2t  3869  rexdifi  4076  sbcnestgfw  4349  sbcnestgf  4354  dfnfc2  4860  mpteq12f  5158  axrep2  5208  axrep3  5209  axrep4  5210  alxfr  5325  axprlem4  5344  axprlem5  5345  copsex2t  5400  mosubopt  5418  fv3  6774  fvmptt  6877  fnoprabg  7375  pssnn  8913  pssnnOLD  8969  fiint  9021  aceq1  9804  zorn2lem4  10186  zfcndrep  10301  mreexexd  17274  fineqvrep  32964  dfon2lem7  33671  bj-alalbial  34810  bj-exalbial  34811  bj-biexal1  34814  bj-bialal  34817  bj-cbv1hv  34905  ax11-pm  34942  bj-snsetex  35080  exlimim  35440  exellim  35442  difunieq  35472  fvineqsneq  35510  wl-nfimf1  35612  wl-nfae1  35613  wl-sb8t  35634  wl-sbnf1  35637  wl-2spsbbi  35647  wl-lem-moexsb  35650  wl-mo2tf  35653  wl-eutf  35655  wl-mo2t  35657  wl-mo3t  35658  wl-sb8eut  35659  wl-ax11-lem3  35665  sbali  36197  setindtr  40762  ismnushort  41808  axc11next  41913  pm14.122b  41930  pm14.123b  41933  eubiOLD  41943  ax6e2ndeqVD  42418  e2ebindALT  42438  ax6e2ndeqALT  42440  rexsb  44478  nfich1  44787  ichnfimlem  44803  ich2al  44807