Theorem nfa1 2186

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

Syntax hints:  ¬ wn 3  ∀wal 1568  ∃wex 1809  Ⅎwnf 1813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-10 2176

This theorem depends on definitions:  df-bi 210  df-or 861  df-ex 1810  df-nf 1814

This theorem is referenced by:  nfna1  2187  nfia1  2188  nfnf1  2189  nfs1v  2191  nfa2  2210  sbalexOLD  2279  sbf2  2307  equs5av  2312  nf5  2317  hba1  2328  axc4i  2355  19.12  2360  exsb  2391  equs5aALT  2398  equs5eALT  2399  cbv1h  2437  dral1  2471  nfald2  2477  equs5a  2489  equs5e  2490  equs5  2492  axc14  2495  nfsb4t  2531  sbcom3  2538  moexexlem  2654  2eu6  2684  axi12  2733  nfaba1  2933  nfaba1g  2934  nfra1  3289  ceqsalgALT  3491  elrab3t  3650  csbie2t  3892  rexdifi  4105  sbcnestgfw  4387  sbcnestgf  4392  dfnfc2  4895  mpteq12f  5197  axrep2  5242  axrep3  5243  axrep4OLD  5246  alxfr  5380  axprlem4OLD  5403  axprlem5OLD  5404  copsex2t  5477  mosubopt  5495  fv3  6901  fvmptt  7012  fnoprabg  7535  pssnn  9154  fiint  9287  aceq1  10102  zorn2lem4  10484  zfcndrep  10600  mreexexd  17705  dvelimalcased  35444  dvelimexcased  35446  fineqvrep  35508  axsepg4  35537  dfon2lem7  36260  mh-setindnd  37029  bj-alalbial  37307  bj-exalbial  37308  bj-biexal1  37311  bj-bialal  37314  bj-cbv1hv  37412  ax11-pm  37448  bj-snsetex  37580  exlimim  37969  exellim  37971  difunieq  38001  fvineqsneq  38039  wl-nfimf1  38162  wl-nfae1  38163  wl-sb8t  38188  wl-sbnf1  38191  wl-2spsbbi  38201  wl-lem-moexsb  38204  wl-mo2tf  38207  wl-eutf  38209  wl-mo2t  38211  wl-mo3t  38212  wl-sb8eut  38214  sbali  38742  setindtr  43734  unielss  43928  ismnushort  44994  axc11next  45099  pm14.122b  45116  pm14.123b  45119  ax6e2ndeqVD  45600  e2ebindALT  45620  ax6e2ndeqALT  45622  modelaxreplem2  45671  modelaxreplem3  45672  permaxrep  45698  rexsb  47819  nfich1  48179  ichnfimlem  48195  ich2al  48199  pgind  50478