Theorem nfa1 2149

Description: The setvar 𝑥 is not free in ∀𝑥𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1787 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 1829	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		nfe1 2148	. . 3 ⊢ Ⅎ𝑥∃𝑥 ¬ 𝜑
3	2	nfn 1861	. 2 ⊢ Ⅎ𝑥 ¬ ∃𝑥 ¬ 𝜑
4	1, 3	nfxfr 1856	1 ⊢ Ⅎ𝑥∀𝑥𝜑

Syntax hints:  ¬ wn 3  ∀wal 1537  ∃wex 1782  Ⅎwnf 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-10 2138

This theorem depends on definitions:  df-bi 206  df-or 845  df-ex 1783  df-nf 1787

This theorem is referenced by:  nfna1  2150  nfia1  2151  nfnf1  2152  nfs1v  2154  nfa2  2171  sbalex  2236  sbf2  2265  equs5av  2272  nf5  2280  hba1  2291  axc4i  2317  19.12  2322  exsb  2358  equs5aALT  2365  equs5eALT  2366  dral1vOLD  2369  cbv1h  2406  dral1  2440  nfald2  2446  equs5a  2458  equs5e  2459  equs5  2461  axc14  2464  nfsb4t  2504  sbcom3  2511  nfmo1  2558  nfeu1  2589  moexexlem  2629  2eu6  2659  axi12  2708  nfaba1  2916  nfaba1g  2917  nfabdwOLD  2932  nfra1  3145  nfra2w  3155  nfra2wOLD  3156  ceqsalgALT  3466  elrab3t  3624  sbcbi2OLD  3780  csbie2t  3874  rexdifi  4081  sbcnestgfw  4353  sbcnestgf  4358  dfnfc2  4864  mpteq12f  5163  axrep2  5213  axrep3  5214  axrep4  5215  alxfr  5331  axprlem4  5350  axprlem5  5351  copsex2t  5407  mosubopt  5425  fv3  6801  fvmptt  6904  fnoprabg  7406  pssnn  8960  pssnnOLD  9049  fiint  9100  aceq1  9882  zorn2lem4  10264  zfcndrep  10379  mreexexd  17366  fineqvrep  33073  dfon2lem7  33774  bj-alalbial  34892  bj-exalbial  34893  bj-biexal1  34896  bj-bialal  34899  bj-cbv1hv  34987  ax11-pm  35024  bj-snsetex  35162  exlimim  35522  exellim  35524  difunieq  35554  fvineqsneq  35592  wl-nfimf1  35694  wl-nfae1  35695  wl-sb8t  35716  wl-sbnf1  35719  wl-2spsbbi  35729  wl-lem-moexsb  35732  wl-mo2tf  35735  wl-eutf  35737  wl-mo2t  35739  wl-mo3t  35740  wl-sb8eut  35741  wl-ax11-lem3  35747  sbali  36279  setindtr  40853  ismnushort  41926  axc11next  42031  pm14.122b  42048  pm14.123b  42051  eubiOLD  42061  ax6e2ndeqVD  42536  e2ebindALT  42556  ax6e2ndeqALT  42558  rexsb  44602  nfich1  44910  ichnfimlem  44926  ich2al  44930