Theorem nfa1 2148

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

Assertion

Ref	Expression
nfa1	⊢ Ⅎ𝑥∀𝑥𝜑

Proof of Theorem nfa1

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

Syntax hints:  ¬ wn 3  ∀wal 1539  ∃wex 1781  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-10 2137

This theorem depends on definitions:  df-bi 206  df-or 846  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfna1  2149  nfia1  2150  nfnf1  2151  nfs1v  2153  nfa2  2170  sbalex  2235  sbf2  2263  equs5av  2270  nf5  2278  hba1  2289  axc4i  2315  19.12  2320  exsb  2355  equs5aALT  2363  equs5eALT  2364  dral1vOLD  2367  cbv1h  2404  dral1  2438  nfald2  2444  equs5a  2456  equs5e  2457  equs5  2459  axc14  2462  nfsb4t  2498  sbcom3  2505  nfmo1  2551  nfeu1  2582  moexexlem  2622  2eu6  2652  axi12  2701  nfaba1  2911  nfaba1g  2912  nfabdwOLD  2927  nfra1  3281  nfra2wOLD  3297  ceqsalgALT  3508  elrab3t  3681  sbcbi2OLD  3839  csbie2t  3933  rexdifi  4144  sbcnestgfw  4417  sbcnestgf  4422  dfnfc2  4932  mpteq12f  5235  axrep2  5287  axrep3  5288  axrep4  5289  alxfr  5404  axprlem4  5423  axprlem5  5424  copsex2t  5491  mosubopt  5509  fv3  6906  fvmptt  7015  fnoprabg  7527  pssnn  9164  pssnnOLD  9261  fiint  9320  aceq1  10108  zorn2lem4  10490  zfcndrep  10605  mreexexd  17588  fineqvrep  34083  dfon2lem7  34749  bj-alalbial  35567  bj-exalbial  35568  bj-biexal1  35571  bj-bialal  35574  bj-cbv1hv  35662  ax11-pm  35698  bj-snsetex  35832  exlimim  36211  exellim  36213  difunieq  36243  fvineqsneq  36281  wl-nfimf1  36383  wl-nfae1  36384  wl-sb8t  36405  wl-sbnf1  36408  wl-2spsbbi  36418  wl-lem-moexsb  36421  wl-mo2tf  36424  wl-eutf  36426  wl-mo2t  36428  wl-mo3t  36429  wl-sb8eut  36430  wl-ax11-lem3  36437  sbali  36968  setindtr  41748  unielss  41952  ismnushort  43045  axc11next  43150  pm14.122b  43167  pm14.123b  43170  eubiOLD  43180  ax6e2ndeqVD  43655  e2ebindALT  43675  ax6e2ndeqALT  43677  rexsb  45793  nfich1  46101  ichnfimlem  46117  ich2al  46121  pgind  47715