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

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

Proof of Theorem nfa1
StepHypRef Expression
1 alex 1793 . 2 (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2 nfe1 2067 . . 3 𝑥𝑥 ¬ 𝜑
32nfn 1824 . 2 𝑥 ¬ ∃𝑥 ¬ 𝜑
41, 3nfxfr 1819 1 𝑥𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1521  wex 1744  wnf 1748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-10 2059
This theorem depends on definitions:  df-bi 197  df-or 384  df-ex 1745  df-nf 1750
This theorem is referenced by:  nfna1  2069  nfia1  2070  nfnf1  2071  nfa2  2080  nf5  2154  axc4i  2169  sb56  2188  hba1  2189  nfnf1OLD  2197  axc16nfOLD  2199  19.12  2200  nfa2OLD  2204  equs5aALT  2213  equs5eALT  2214  cbv1h  2304  axc15  2339  dral1  2356  nfald2  2362  equs5a  2376  equs5e  2377  equs5  2379  axc14  2400  sbf2  2410  nfsb4t  2417  sbcom3  2439  exsb  2496  nfeu1  2508  moexex  2570  2eu6  2587  exists2  2591  nfaba1  2799  nfra1  2970  ceqsalgALT  3262  elrab3t  3395  csbie2t  3595  sbcnestgf  4028  dfnfc2  4486  dfnfc2OLD  4487  mpteq12f  4764  axrep2  4806  axrep3  4807  axrep4  4808  alxfr  4908  copsex2t  4986  mosubopt  5001  fv3  6244  fvmptt  6339  fnoprabg  6803  pssnn  8219  fiint  8278  aceq1  8978  zorn2lem4  9359  zfcndrep  9474  mreexexd  16355  mreexexdOLD  16356  dfon2lem7  31818  bj-alalbial  32817  bj-exalbial  32818  bj-biexal1  32821  bj-bialal  32824  bj-cbv1hv  32855  bj-dral1v  32873  bj-axrep2  32914  bj-axrep3  32915  bj-axrep4  32916  ax11-pm  32944  bj-mo3OLD  32957  bj-snsetex  33076  exlimim  33319  exellim  33322  wl-nfimf1  33443  wl-nfae1  33445  wl-sb8t  33463  wl-sbnf1  33466  wl-lem-moexsb  33480  wl-mo2tf  33483  wl-eutf  33485  wl-mo2t  33487  wl-mo3t  33488  wl-sb8eut  33489  wl-ax11-lem3  33494  wl-sbcom3  33502  sbali  34045  nfbii2  34097  setindtr  37908  axc11next  38924  iotain  38935  pm14.122b  38941  pm14.123b  38944  eubi  38954  ax6e2ndeqVD  39459  e2ebindALT  39479  ax6e2ndeqALT  39481  rexsb  41489
  Copyright terms: Public domain W3C validator