MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfa1 Structured version   Visualization version   GIF version

Theorem nfa1 2152
Description: The setvar 𝑥 is not free in 𝑥𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1784 changed. (Revised by Wolf Lammen, 11-Sep-2021.) Remove dependency on ax-12 2178. (Revised by Wolf Lammen, 12-Oct-2021.)
Assertion
Ref Expression
nfa1 𝑥𝑥𝜑

Proof of Theorem nfa1
StepHypRef Expression
1 alex 1826 . 2 (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2 nfe1 2151 . . 3 𝑥𝑥 ¬ 𝜑
32nfn 1857 . 2 𝑥 ¬ ∃𝑥 ¬ 𝜑
41, 3nfxfr 1853 1 𝑥𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1538  wex 1779  wnf 1783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-10 2142
This theorem depends on definitions:  df-bi 207  df-or 848  df-ex 1780  df-nf 1784
This theorem is referenced by:  nfna1  2153  nfia1  2154  nfnf1  2155  nfs1v  2157  nfa2  2177  sbalexOLD  2244  sbf2  2272  equs5av  2277  nf5  2282  hba1  2293  axc4i  2321  19.12  2326  exsb  2357  equs5aALT  2364  equs5eALT  2365  cbv1h  2403  dral1  2437  nfald2  2443  equs5a  2455  equs5e  2456  equs5  2458  axc14  2461  nfsb4t  2497  sbcom3  2504  nfmo1  2550  nfeu1  2581  moexexlem  2619  2eu6  2650  axi12  2699  nfaba1  2899  nfaba1OLD  2900  nfaba1g  2901  nfra1  3253  ceqsalgALT  3473  elrab3t  3647  csbie2t  3889  rexdifi  4101  sbcnestgfw  4372  sbcnestgf  4377  dfnfc2  4880  mpteq12f  5177  axrep2  5221  axrep3  5222  axrep4OLD  5225  alxfr  5346  axprlem4OLD  5368  axprlem5OLD  5369  copsex2t  5435  mosubopt  5453  fv3  6840  fvmptt  6950  fnoprabg  7472  pssnn  9082  fiint  9216  fiintOLD  9217  aceq1  10011  zorn2lem4  10393  zfcndrep  10508  mreexexd  17554  dvelimalcased  35048  dvelimexcased  35050  fineqvrep  35076  dfon2lem7  35773  bj-alalbial  36685  bj-exalbial  36686  bj-biexal1  36689  bj-bialal  36692  bj-cbv1hv  36780  ax11-pm  36816  bj-snsetex  36947  exlimim  37326  exellim  37328  difunieq  37358  fvineqsneq  37396  wl-nfimf1  37510  wl-nfae1  37511  wl-sb8t  37536  wl-sbnf1  37539  wl-2spsbbi  37549  wl-lem-moexsb  37552  wl-mo2tf  37555  wl-eutf  37557  wl-mo2t  37559  wl-mo3t  37560  wl-sb8eut  37562  wl-ax11-lem3  37571  sbali  38102  setindtr  43007  unielss  43201  ismnushort  44284  axc11next  44389  pm14.122b  44406  pm14.123b  44409  eubiOLD  44419  ax6e2ndeqVD  44892  e2ebindALT  44912  ax6e2ndeqALT  44914  modelaxreplem2  44963  modelaxreplem3  44964  permaxrep  44990  rexsb  47093  nfich1  47441  ichnfimlem  47457  ich2al  47461  pgind  49712
  Copyright terms: Public domain W3C validator