Theorem nfa1 2156

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

Assertion

Ref	Expression
nfa1	⊢ Ⅎ𝑥∀𝑥𝜑

Proof of Theorem nfa1

Step	Hyp	Ref	Expression
1		alex 1827	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		nfe1 2155	. . 3 ⊢ Ⅎ𝑥∃𝑥 ¬ 𝜑
3	2	nfn 1858	. 2 ⊢ Ⅎ𝑥 ¬ ∃𝑥 ¬ 𝜑
4	1, 3	nfxfr 1854	1 ⊢ Ⅎ𝑥∀𝑥𝜑

Syntax hints:  ¬ wn 3  ∀wal 1539  ∃wex 1780  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-10 2146

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

This theorem is referenced by:  nfna1  2157  nfia1  2158  nfnf1  2159  nfs1v  2161  nfa2  2181  sbalexOLD  2248  sbf2  2276  equs5av  2281  nf5  2286  hba1  2297  axc4i  2325  19.12  2330  exsb  2361  equs5aALT  2368  equs5eALT  2369  cbv1h  2407  dral1  2441  nfald2  2447  equs5a  2459  equs5e  2460  equs5  2462  axc14  2465  nfsb4t  2501  sbcom3  2508  nfmo1  2554  nfeu1  2585  moexexlem  2623  2eu6  2654  axi12  2703  nfaba1  2903  nfaba1OLD  2904  nfaba1g  2905  nfra1  3257  ceqsalgALT  3474  elrab3t  3642  csbie2t  3884  rexdifi  4099  sbcnestgfw  4370  sbcnestgf  4375  dfnfc2  4880  mpteq12f  5178  axrep2  5222  axrep3  5223  axrep4OLD  5226  alxfr  5347  axprlem4OLD  5369  axprlem5OLD  5370  copsex2t  5435  mosubopt  5453  fv3  6846  fvmptt  6955  fnoprabg  7475  pssnn  9085  fiint  9218  aceq1  10015  zorn2lem4  10397  zfcndrep  10512  mreexexd  17556  dvelimalcased  35108  dvelimexcased  35110  fineqvrep  35158  dfon2lem7  35852  bj-alalbial  36766  bj-exalbial  36767  bj-biexal1  36770  bj-bialal  36773  bj-cbv1hv  36861  ax11-pm  36897  bj-snsetex  37028  exlimim  37407  exellim  37409  difunieq  37439  fvineqsneq  37477  wl-nfimf1  37591  wl-nfae1  37592  wl-sb8t  37617  wl-sbnf1  37620  wl-2spsbbi  37630  wl-lem-moexsb  37633  wl-mo2tf  37636  wl-eutf  37638  wl-mo2t  37640  wl-mo3t  37641  wl-sb8eut  37643  sbali  38172  setindtr  43141  unielss  43335  ismnushort  44418  axc11next  44523  pm14.122b  44540  pm14.123b  44543  ax6e2ndeqVD  45025  e2ebindALT  45045  ax6e2ndeqALT  45047  modelaxreplem2  45096  modelaxreplem3  45097  permaxrep  45123  rexsb  47223  nfich1  47571  ichnfimlem  47587  ich2al  47591  pgind  49842