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

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

Proof of Theorem nfa1
StepHypRef Expression
1 alex 1750 . 2 (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2 nfe1 2024 . . 3 𝑥𝑥 ¬ 𝜑
32nfn 1781 . 2 𝑥 ¬ ∃𝑥 ¬ 𝜑
41, 3nfxfr 1776 1 𝑥𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1478  wex 1701  wnf 1705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-10 2016
This theorem depends on definitions:  df-bi 197  df-or 385  df-ex 1702  df-nf 1707
This theorem is referenced by:  nfna1  2026  nfia1  2027  nfnf1  2028  nfa2  2037  nf5  2113  axc4i  2127  sb56  2147  hba1  2148  nfnf1OLD  2156  axc16nfOLD  2160  19.12  2161  nfa2OLD  2165  equs5aALT  2176  equs5eALT  2177  cbv1h  2267  axc15  2302  dral1  2324  nfald2  2330  ax12v2OLD  2341  equs5a  2347  equs5e  2348  equs5  2350  axc14  2371  sbf2  2381  nfsb4t  2388  sbcom3  2410  exsb  2467  nfeu1  2479  moexex  2540  2eu6  2557  exists2  2561  nfaba1  2766  nfra1  2937  ceqsalgALT  3221  elrab3t  3350  csbie2t  3548  sbcnestgf  3973  dfnfc2  4427  dfnfc2OLD  4428  mpteq12f  4701  axrep2  4743  axrep3  4744  axrep4  4745  alxfr  4848  copsex2t  4927  mosubopt  4942  fv3  6173  fvmptt  6266  fnoprabg  6726  abnex  6929  pssnn  8138  fiint  8197  aceq1  8900  zorn2lem4  9281  zfcndrep  9396  mreexexd  16248  mreexexdOLD  16249  dfon2lem7  31448  bj-alalbial  32387  bj-exalbial  32388  bj-biexal1  32391  bj-bialal  32394  bj-cbv1hv  32425  bj-dral1v  32444  bj-axrep2  32485  bj-axrep3  32486  bj-axrep4  32487  ax11-pm  32515  bj-mo3OLD  32530  bj-snsetex  32651  exlimim  32860  exellim  32863  wl-nfimf1  32984  wl-nfae1  32986  wl-sb8t  33004  wl-sbnf1  33007  wl-lem-moexsb  33021  wl-mo2tf  33024  wl-eutf  33026  wl-mo2t  33028  wl-mo3t  33029  wl-sb8eut  33030  wl-ax11-lem3  33035  wl-sbcom3  33043  sbali  33586  nfbii2  33638  setindtr  37110  axc11next  38128  iotain  38139  pm14.122b  38145  pm14.123b  38148  eubi  38158  ax6e2ndeqVD  38667  e2ebindALT  38687  ax6e2ndeqALT  38689  rexsb  40502
  Copyright terms: Public domain W3C validator