Theorem nfa1 2151

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

Assertion

Ref	Expression
nfa1	⊢ Ⅎ𝑥∀𝑥𝜑

Proof of Theorem nfa1

Step	Hyp	Ref	Expression
1		alex 1822	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		nfe1 2150	. . 3 ⊢ Ⅎ𝑥∃𝑥 ¬ 𝜑
3	2	nfn 1853	. 2 ⊢ Ⅎ𝑥 ¬ ∃𝑥 ¬ 𝜑
4	1, 3	nfxfr 1849	1 ⊢ Ⅎ𝑥∀𝑥𝜑

Syntax hints:  ¬ wn 3  ∀wal 1531  ∃wex 1776  Ⅎwnf 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-10 2141

This theorem depends on definitions:  df-bi 209  df-or 844  df-ex 1777  df-nf 1781

This theorem is referenced by:  nfna1  2152  nfia1  2153  nfnf1  2154  nfa2  2171  sbf2  2267  nfs1v  2269  sb56OLD  2274  equs5av  2275  nf5  2286  hba1  2297  spsbimvOLD  2324  axc4i  2337  19.12  2342  exsb  2374  equs5aALT  2380  equs5eALT  2381  dral1v  2383  cbv1h  2421  dral1  2457  nfald2  2463  equs5a  2476  equs5e  2477  equs5  2479  axc14  2482  nfsb4t  2535  sbcom3  2544  nfsb4tALT  2600  nfmo1  2637  nfeu1  2670  moexexlem  2707  2eu6  2740  axi12  2789  nfaba1  2986  nfaba1g  2987  nfabdw  3000  nfra1  3219  ceqsalgALT  3531  elrab3t  3679  sbcbi2  3831  csbie2t  3921  rexdifi  4122  sbcnestgfw  4370  sbcnestgf  4375  dfnfc2  4850  mpteq12f  5142  axrep2  5186  axrep3  5187  axrep4  5188  alxfr  5300  axprlem4  5319  axprlem5  5320  copsex2t  5376  mosubopt  5393  fv3  6683  fvmptt  6783  fnoprabg  7269  pssnn  8730  fiint  8789  aceq1  9537  zorn2lem4  9915  zfcndrep  10030  mreexexd  16913  dfon2lem7  33029  bj-alalbial  34030  bj-exalbial  34031  bj-biexal1  34034  bj-bialal  34037  bj-cbv1hv  34113  ax11-pm  34150  bj-snsetex  34270  exlimim  34617  exellim  34619  difunieq  34649  fvineqsneq  34687  wl-nfimf1  34760  wl-nfae1  34761  wl-sb8t  34782  wl-sbnf1  34785  wl-2spsbbi  34795  wl-lem-moexsb  34798  wl-mo2tf  34801  wl-eutf  34803  wl-mo2t  34805  wl-mo3t  34806  wl-sb8eut  34807  wl-ax11-lem3  34813  sbali  35384  setindtr  39614  axc11next  40731  pm14.122b  40748  pm14.123b  40751  eubiOLD  40761  ax6e2ndeqVD  41236  e2ebindALT  41256  ax6e2ndeqALT  41258  rexsb  43290  nfich1  43600  dfich2bi  43608  ichnfimlem2  43615  ich2al  43621