Theorem nfa1 2164

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

Assertion

Ref	Expression
nfa1	⊢ Ⅎ𝑥∀𝑥𝜑

Proof of Theorem nfa1

Step	Hyp	Ref	Expression
1		alex 1834	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		nfe1 2163	. . 3 ⊢ Ⅎ𝑥∃𝑥 ¬ 𝜑
3	2	nfn 1865	. 2 ⊢ Ⅎ𝑥 ¬ ∃𝑥 ¬ 𝜑
4	1, 3	nfxfr 1861	1 ⊢ Ⅎ𝑥∀𝑥𝜑

Syntax hints:  ¬ wn 3  ∀wal 1546  ∃wex 1787  Ⅎwnf 1791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-10 2154

This theorem depends on definitions:  df-bi 209  df-or 855  df-ex 1788  df-nf 1792

This theorem is referenced by:  nfna1  2165  nfia1  2166  nfnf1  2167  nfs1v  2169  nfa2  2188  sbalexOLD  2257  sbf2  2285  equs5av  2290  nf5  2295  hba1  2306  axc4i  2333  19.12  2338  exsb  2369  equs5aALT  2376  equs5eALT  2377  cbv1h  2415  dral1  2449  nfald2  2455  equs5a  2467  equs5e  2468  equs5  2470  axc14  2473  nfsb4t  2509  sbcom3  2516  moexexlem  2632  2eu6  2662  axi12  2711  nfaba1  2911  nfaba1g  2912  nfra1  3265  ceqsalgALT  3469  elrab3t  3629  csbie2t  3870  rexdifi  4082  sbcnestgfw  4351  sbcnestgf  4356  dfnfc2  4862  mpteq12f  5159  axrep2  5204  axrep3  5205  axrep4OLD  5208  alxfr  5338  axprlem4OLD  5361  axprlem5OLD  5362  copsex2t  5435  mosubopt  5453  fv3  6848  fvmptt  6959  fnoprabg  7482  pssnn  9097  fiint  9231  aceq1  10034  zorn2lem4  10417  zfcndrep  10533  mreexexd  17609  dvelimalcased  35270  dvelimexcased  35272  fineqvrep  35308  axsepg4  35337  dfon2lem7  36028  mh-setindnd  36778  bj-alalbial  37057  bj-exalbial  37058  bj-biexal1  37061  bj-bialal  37064  bj-cbv1hv  37162  ax11-pm  37198  bj-snsetex  37329  exlimim  37717  exellim  37719  difunieq  37749  fvineqsneq  37787  wl-nfimf1  37910  wl-nfae1  37911  wl-sb8t  37936  wl-sbnf1  37939  wl-2spsbbi  37949  wl-lem-moexsb  37952  wl-mo2tf  37955  wl-eutf  37957  wl-mo2t  37959  wl-mo3t  37960  wl-sb8eut  37962  sbali  38492  setindtr  43482  unielss  43676  ismnushort  44758  axc11next  44863  pm14.122b  44880  pm14.123b  44883  ax6e2ndeqVD  45365  e2ebindALT  45385  ax6e2ndeqALT  45387  modelaxreplem2  45436  modelaxreplem3  45437  permaxrep  45463  rexsb  47574  nfich1  47934  ichnfimlem  47950  ich2al  47954  pgind  50219