Theorem nfa1 2149

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 2175. (Revised by Wolf Lammen, 12-Oct-2021.)

Assertion

Ref	Expression
nfa1	⊢ Ⅎ𝑥∀𝑥𝜑

Proof of Theorem nfa1

Step	Hyp	Ref	Expression
1		alex 1823	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		nfe1 2148	. . 3 ⊢ Ⅎ𝑥∃𝑥 ¬ 𝜑
3	2	nfn 1855	. 2 ⊢ Ⅎ𝑥 ¬ ∃𝑥 ¬ 𝜑
4	1, 3	nfxfr 1850	1 ⊢ Ⅎ𝑥∀𝑥𝜑

Syntax hints:  ¬ wn 3  ∀wal 1535  ∃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 2139

This theorem depends on definitions:  df-bi 207  df-or 848  df-ex 1777  df-nf 1781

This theorem is referenced by:  nfna1  2150  nfia1  2151  nfnf1  2152  nfs1v  2154  nfa2  2174  sbalexOLD  2241  sbf2  2270  equs5av  2275  nf5  2281  hba1  2292  axc4i  2321  19.12  2326  exsb  2360  equs5aALT  2367  equs5eALT  2368  dral1vOLD  2371  cbv1h  2408  dral1  2442  nfald2  2448  equs5a  2460  equs5e  2461  equs5  2463  axc14  2466  nfsb4t  2502  sbcom3  2509  nfmo1  2555  nfeu1  2586  moexexlem  2624  2eu6  2655  axi12  2704  nfaba1  2911  nfaba1OLD  2912  nfaba1g  2913  nfra1  3282  nfra2wOLD  3298  ceqsalgALT  3516  elrab3t  3694  csbie2t  3949  rexdifi  4160  sbcnestgfw  4427  sbcnestgf  4432  dfnfc2  4934  mpteq12f  5236  axrep2  5288  axrep3  5289  axrep4OLD  5292  alxfr  5413  axprlem4OLD  5435  axprlem5OLD  5436  copsex2t  5503  mosubopt  5520  fv3  6925  fvmptt  7036  fnoprabg  7556  pssnn  9207  fiint  9364  fiintOLD  9365  aceq1  10155  zorn2lem4  10537  zfcndrep  10652  mreexexd  17693  dvelimalcased  35068  dvelimexcased  35070  fineqvrep  35088  dfon2lem7  35771  bj-alalbial  36684  bj-exalbial  36685  bj-biexal1  36688  bj-bialal  36691  bj-cbv1hv  36779  ax11-pm  36815  bj-snsetex  36946  exlimim  37325  exellim  37327  difunieq  37357  fvineqsneq  37395  wl-nfimf1  37507  wl-nfae1  37508  wl-sb8t  37533  wl-sbnf1  37536  wl-2spsbbi  37546  wl-lem-moexsb  37549  wl-mo2tf  37552  wl-eutf  37554  wl-mo2t  37556  wl-mo3t  37557  wl-sb8eut  37559  wl-ax11-lem3  37568  sbali  38099  setindtr  43013  unielss  43207  ismnushort  44297  axc11next  44402  pm14.122b  44419  pm14.123b  44422  eubiOLD  44432  ax6e2ndeqVD  44907  e2ebindALT  44927  ax6e2ndeqALT  44929  modelaxreplem2  44944  modelaxreplem3  44945  rexsb  47049  nfich1  47372  ichnfimlem  47388  ich2al  47392  pgind  48948