Theorem nfa1 2141

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

Assertion

Ref	Expression
nfa1	⊢ Ⅎ𝑥∀𝑥𝜑

Proof of Theorem nfa1

Step	Hyp	Ref	Expression
1		alex 1821	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		nfe1 2140	. . 3 ⊢ Ⅎ𝑥∃𝑥 ¬ 𝜑
3	2	nfn 1853	. 2 ⊢ Ⅎ𝑥 ¬ ∃𝑥 ¬ 𝜑
4	1, 3	nfxfr 1848	1 ⊢ Ⅎ𝑥∀𝑥𝜑

Syntax hints:  ¬ wn 3  ∀wal 1532  ∃wex 1774  Ⅎwnf 1778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-10 2130

This theorem depends on definitions:  df-bi 206  df-or 847  df-ex 1775  df-nf 1779

This theorem is referenced by:  nfna1  2142  nfia1  2143  nfnf1  2144  nfs1v  2146  nfa2  2166  sbalex  2231  sbf2  2259  equs5av  2266  nf5  2272  hba1  2283  axc4i  2311  19.12  2316  exsb  2351  equs5aALT  2359  equs5eALT  2360  dral1vOLD  2363  cbv1h  2400  dral1  2434  nfald2  2440  equs5a  2452  equs5e  2453  equs5  2455  axc14  2458  nfsb4t  2494  sbcom3  2501  nfmo1  2547  nfeu1  2578  moexexlem  2618  2eu6  2648  axi12  2697  nfaba1  2907  nfaba1g  2908  nfabdwOLD  2923  nfra1  3277  nfra2wOLD  3293  ceqsalgALT  3505  elrab3t  3680  csbie2t  3931  rexdifi  4142  sbcnestgfw  4415  sbcnestgf  4420  dfnfc2  4928  mpteq12f  5231  axrep2  5283  axrep3  5284  axrep4  5285  alxfr  5402  axprlem4  5421  axprlem5  5422  copsex2t  5489  mosubopt  5507  fv3  6910  fvmptt  7020  fnoprabg  7538  pssnn  9187  pssnnOLD  9284  fiint  9343  aceq1  10135  zorn2lem4  10517  zfcndrep  10632  mreexexd  17622  fineqvrep  34710  dfon2lem7  35380  bj-alalbial  36173  bj-exalbial  36174  bj-biexal1  36177  bj-bialal  36180  bj-cbv1hv  36268  ax11-pm  36304  bj-snsetex  36437  exlimim  36816  exellim  36818  difunieq  36848  fvineqsneq  36886  wl-nfimf1  36988  wl-nfae1  36989  wl-sb8t  37014  wl-sbnf1  37017  wl-2spsbbi  37027  wl-lem-moexsb  37030  wl-mo2tf  37033  wl-eutf  37035  wl-mo2t  37037  wl-mo3t  37038  wl-sb8eut  37040  wl-ax11-lem3  37049  sbali  37580  setindtr  42436  unielss  42637  ismnushort  43729  axc11next  43834  pm14.122b  43851  pm14.123b  43854  eubiOLD  43864  ax6e2ndeqVD  44339  e2ebindALT  44359  ax6e2ndeqALT  44361  rexsb  46470  nfich1  46778  ichnfimlem  46794  ich2al  46798  pgind  48139

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »