Theorem nfa1 2086

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

Assertion

Ref	Expression
nfa1	⊢ Ⅎ𝑥∀𝑥𝜑

Proof of Theorem nfa1

Step	Hyp	Ref	Expression
1		alex 1788	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		nfe1 2085	. . 3 ⊢ Ⅎ𝑥∃𝑥 ¬ 𝜑
3	2	nfn 1819	. 2 ⊢ Ⅎ𝑥 ¬ ∃𝑥 ¬ 𝜑
4	1, 3	nfxfr 1815	1 ⊢ Ⅎ𝑥∀𝑥𝜑

Syntax hints:  ¬ wn 3  ∀wal 1505  ∃wex 1742  Ⅎwnf 1746

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-10 2077

This theorem depends on definitions:  df-bi 199  df-or 834  df-ex 1743  df-nf 1747

This theorem is referenced by:  nfna1  2087  nfia1  2088  nfnf1  2089  nfa2  2103  sbf2  2198  nfs1v  2200  sb56OLD  2205  nf5  2214  hba1  2225  spsbimvOLD  2249  axc4i  2260  19.12  2265  exsb  2290  equs5aALT  2296  equs5eALT  2297  cbv1h  2336  axc15OLD  2356  dral1  2373  nfald2  2379  equs5a  2392  equs5e  2393  equs5  2395  axc14  2398  exsbOLD  2420  nfsb4t  2458  sbcom3  2470  nfsb4tALT  2528  nfmo1  2566  nfeu1  2602  moexexvw  2656  2moswapv  2657  moexex  2664  2eu6  2683  exists2OLD  2690  axi12  2741  nfaba1  2933  nfra1  3163  ceqsalgALT  3445  elrab3t  3588  sbcbi2  3730  csbie2t  3813  sbcnestgf  4253  dfnfc2  4724  mpteq12f  5004  axrep2  5046  axrep3  5047  axrep4  5048  alxfr  5155  axprlem4  5177  axprlem5  5178  copsex2t  5232  mosubopt  5249  fv3  6511  fvmptt  6608  fnoprabg  7085  pssnn  8523  fiint  8582  aceq1  9329  zorn2lem4  9711  zfcndrep  9826  mreexexd  16767  dfon2lem7  32494  bj-alalbial  33484  bj-exalbial  33485  bj-biexal1  33488  bj-bialal  33491  bj-cbv1hv  33517  bj-dral1v  33533  bj-axrep2  33559  bj-axrep3  33560  bj-axrep4  33561  ax11-pm  33586  bj-snsetex  33728  exlimim  34000  exellim  34002  difunieq  34032  fvineqsneq  34069  wl-nfimf1  34145  wl-nfae1  34146  wl-sb8t  34165  wl-sbnf1  34168  wl-2spsbbi  34178  wl-ich-lem1  34180  wl-ich-lem1b  34182  wl-ich-lem1d  34185  wl-lem-moexsb  34193  wl-mo2tf  34196  wl-eutf  34198  wl-mo2t  34200  wl-mo3t  34201  wl-sb8eut  34202  wl-ax11-lem3  34208  sbali  34782  setindtr  38962  axc11next  40099  pm14.122b  40116  pm14.123b  40119  eubiOLD  40129  ax6e2ndeqVD  40606  e2ebindALT  40626  ax6e2ndeqALT  40628  rexsb  42649  nfich1  42925  dfich2bi  42930