Theorem nfa1 2141

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

Assertion

Ref	Expression
nfa1	⊢ Ⅎ𝑥∀𝑥𝜑

Proof of Theorem nfa1

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

Syntax hints:  ¬ wn 3  ∀wal 1532  ∃wex 1774  Ⅎwnf 1778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-10 2130

This theorem depends on definitions:  df-bi 206  df-or 846  df-ex 1775  df-nf 1779

This theorem is referenced by:  nfna1  2142  nfia1  2143  nfnf1  2144  nfs1v  2146  nfa2  2166  sbalex  2231  sbf2  2259  equs5av  2266  nf5  2272  hba1  2283  axc4i  2311  19.12  2316  exsb  2350  equs5aALT  2358  equs5eALT  2359  dral1vOLD  2362  cbv1h  2399  dral1  2433  nfald2  2439  equs5a  2451  equs5e  2452  equs5  2454  axc14  2457  nfsb4t  2493  sbcom3  2500  nfmo1  2546  nfeu1  2577  moexexlem  2615  2eu6  2646  axi12  2695  nfaba1  2900  nfaba1OLD  2901  nfaba1g  2902  nfabdwOLD  2917  nfra1  3272  nfra2wOLD  3288  ceqsalgALT  3499  elrab3t  3680  csbie2t  3933  rexdifi  4145  sbcnestgfw  4423  sbcnestgf  4428  dfnfc2  4937  mpteq12f  5241  axrep2  5293  axrep3  5294  axrep4  5295  alxfr  5411  axprlem4  5430  axprlem5  5431  copsex2t  5498  mosubopt  5516  fv3  6919  fvmptt  7029  fnoprabg  7548  pssnn  9206  pssnnOLD  9299  fiint  9368  fiintOLD  9369  aceq1  10160  zorn2lem4  10542  zfcndrep  10657  mreexexd  17661  fineqvrep  34931  dfon2lem7  35613  bj-alalbial  36406  bj-exalbial  36407  bj-biexal1  36410  bj-bialal  36413  bj-cbv1hv  36501  ax11-pm  36537  bj-snsetex  36670  exlimim  37049  exellim  37051  difunieq  37081  fvineqsneq  37119  wl-nfimf1  37221  wl-nfae1  37222  wl-sb8t  37247  wl-sbnf1  37250  wl-2spsbbi  37260  wl-lem-moexsb  37263  wl-mo2tf  37266  wl-eutf  37268  wl-mo2t  37270  wl-mo3t  37271  wl-sb8eut  37273  wl-ax11-lem3  37282  sbali  37813  setindtr  42682  unielss  42883  ismnushort  43975  axc11next  44080  pm14.122b  44097  pm14.123b  44100  eubiOLD  44110  ax6e2ndeqVD  44585  e2ebindALT  44605  ax6e2ndeqALT  44607  rexsb  46712  nfich1  47019  ichnfimlem  47035  ich2al  47039  pgind  48463