Theorem nfa1 2188

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

Assertion

Ref	Expression
nfa1	⊢ Ⅎ𝑥∀𝑥𝜑

Proof of Theorem nfa1

Step	Hyp	Ref	Expression
1		alex 1859	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		nfe1 2187	. . 3 ⊢ Ⅎ𝑥∃𝑥 ¬ 𝜑
3	2	nfn 1890	. 2 ⊢ Ⅎ𝑥 ¬ ∃𝑥 ¬ 𝜑
4	1, 3	nfxfr 1886	1 ⊢ Ⅎ𝑥∀𝑥𝜑

This proof depends on syntax axioms:  ¬ wn 3  ∀wal 1568  ∃wex 1812  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-10 2178

This proof depends on definitions:  df-bi 210  df-or 862  df-ex 1813  df-nf 1817

This theorem is used by:  nfna1  2189  nfia1  2190  nfnf1  2191  nfs1v  2193  nfa2  2210  sbf2  2306  equs5av  2311  nf5  2316  hba1  2327  axc4i  2353  19.12  2358  exsb  2389  equs5aALT  2396  equs5eALT  2397  cbv1h  2435  dral1  2469  nfald2  2475  equs5a  2487  equs5e  2488  equs5  2490  axc14  2493  nfsb4t  2529  sbcom3  2536  moexexlem  2652  2eu6  2682  axi12  2731  nfaba1  2931  nfaba1g  2932  nfra1  3287  ceqsalgALT  3487  elrab3t  3644  csbie2t  3885  rexdifi  4097  sbcnestgfw  4379  sbcnestgf  4384  dfnfc2  4889  mpteq12f  5190  axrep2  5235  axrep3  5236  alxfr  5369  copsex2t  5464  mosubopt  5482  mosubott  5484  fv3  6895  fvmptt  7006  fnoprabg  7535  pssnn  9168  fiint  9302  aceq1  10177  zorn2lem4  10558  zfcndrep  10680  mreexexd  17802  dvelimalcased  35688  dvelimexcased  35690  fineqvrep  35755  axsepg4  35784  dfon2lem7  36521  mh-setindnd  37295  bj-alalbial  37573  bj-exalbial  37574  bj-biexal1  37577  bj-bialal  37580  bj-cbv1hv  37678  ax11-pm  37714  bj-snsetex  37846  exlimim  38233  exellim  38235  difunieq  38265  fvineqsneq  38303  wl-nfimf1  38426  wl-nfae1  38427  wl-sb8t  38452  wl-sbnf1  38455  wl-2spsbbi  38465  wl-lem-moexsb  38468  wl-mo2tf  38471  wl-eutf  38473  wl-mo2t  38475  wl-mo3t  38476  wl-sb8eut  38478  sbali  39012  setindtr  43984  unielss  44178  ismnushort  45244  axc11next  45349  pm14.122b  45366  pm14.123b  45369  ax6e2ndeqVD  45850  e2ebindALT  45870  ax6e2ndeqALT  45872  modelaxreplem2  45921  modelaxreplem3  45922  permaxrep  45948  rexsb  48113  nfich1  48473  ichnfimlem  48489  ich2al  48493  pgind  50754