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

Theorem nfa1 2156
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 2179. (Revised by Wolf Lammen, 12-Oct-2021.)
Assertion
Ref Expression
nfa1 𝑥𝑥𝜑

Proof of Theorem nfa1
StepHypRef Expression
1 alex 1827 . 2 (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2 nfe1 2155 . . 3 𝑥𝑥 ¬ 𝜑
32nfn 1858 . 2 𝑥 ¬ ∃𝑥 ¬ 𝜑
41, 3nfxfr 1854 1 𝑥𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1536  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 2146
This theorem depends on definitions:  df-bi 210  df-or 845  df-ex 1782  df-nf 1786
This theorem is referenced by:  nfna1  2157  nfia1  2158  nfnf1  2159  nfs1v  2161  nfa2  2178  sbf2  2274  sb56OLD  2280  equs5av  2281  nf5  2292  hba1  2303  spsbimvOLD  2330  axc4i  2343  19.12  2348  exsb  2380  equs5aALT  2386  equs5eALT  2387  dral1v  2389  cbv1h  2427  dral1  2463  nfald2  2469  equs5a  2482  equs5e  2483  equs5  2485  axc14  2488  nfsb4t  2541  sbcom3  2550  nfsb4tALT  2606  nfmo1  2642  nfeu1  2675  moexexlem  2714  2eu6  2745  axi12  2794  nfaba1  2990  nfaba1g  2991  nfabdw  3003  nfra1  3213  ceqsalgALT  3516  elrab3t  3665  sbcbi2OLD  3817  csbie2t  3904  rexdifi  4108  sbcnestgfw  4353  sbcnestgf  4358  dfnfc2  4846  mpteq12f  5136  axrep2  5180  axrep3  5181  axrep4  5182  alxfr  5296  axprlem4  5315  axprlem5  5316  copsex2t  5371  mosubopt  5388  fv3  6681  fvmptt  6781  fnoprabg  7270  pssnn  8735  fiint  8794  aceq1  9543  zorn2lem4  9921  zfcndrep  10036  mreexexd  16921  dfon2lem7  33119  bj-alalbial  34120  bj-exalbial  34121  bj-biexal1  34124  bj-bialal  34127  bj-cbv1hv  34205  ax11-pm  34242  bj-snsetex  34371  exlimim  34731  exellim  34733  difunieq  34763  fvineqsneq  34801  wl-nfimf1  34903  wl-nfae1  34904  wl-sb8t  34925  wl-sbnf1  34928  wl-2spsbbi  34938  wl-lem-moexsb  34941  wl-mo2tf  34944  wl-eutf  34946  wl-mo2t  34948  wl-mo3t  34949  wl-sb8eut  34950  wl-ax11-lem3  34956  sbali  35522  setindtr  39909  axc11next  41058  pm14.122b  41075  pm14.123b  41078  eubiOLD  41088  ax6e2ndeqVD  41563  e2ebindALT  41583  ax6e2ndeqALT  41585  rexsb  43607  nfich1  43917  ichnfimlem  43933  ich2al  43937
  Copyright terms: Public domain W3C validator