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

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

Proof of Theorem nfa1
StepHypRef Expression
1 alex 1898 . 2 (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2 nfe1 2172 . . 3 𝑥𝑥 ¬ 𝜑
32nfn 1929 . 2 𝑥 ¬ ∃𝑥 ¬ 𝜑
41, 3nfxfr 1924 1 𝑥𝑥𝜑
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3  ∀wal 1626  ∃wex 1849  Ⅎwnf 1853 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-10 2164 This theorem depends on definitions:  df-bi 197  df-or 384  df-ex 1850  df-nf 1855 This theorem is referenced by:  nfna1  2174  nfia1  2175  nfnf1  2176  nfa2  2185  nf5  2259  axc4i  2274  sb56  2293  hba1  2294  nfnf1OLD  2302  axc16nfOLD  2304  19.12  2305  nfa2OLD  2309  equs5aALT  2318  equs5eALT  2319  cbv1h  2409  axc15  2444  dral1  2461  nfald2  2467  equs5a  2481  equs5e  2482  equs5  2484  axc14  2505  sbf2  2515  nfsb4t  2522  sbcom3  2544  exsb  2601  nfeu1  2613  moexex  2675  2eu6  2692  exists2  2696  nfaba1  2904  nfra1  3075  ceqsalgALT  3367  elrab3t  3499  csbie2t  3699  sbcnestgf  4134  dfnfc2  4602  dfnfc2OLD  4603  mpteq12f  4879  axrep2  4921  axrep3  4922  axrep4  4923  alxfr  5023  copsex2t  5101  mosubopt  5116  fv3  6363  fvmptt  6458  fnoprabg  6922  pssnn  8339  fiint  8398  aceq1  9126  zorn2lem4  9509  zfcndrep  9624  mreexexd  16506  dfon2lem7  31995  bj-alalbial  32994  bj-exalbial  32995  bj-biexal1  32998  bj-bialal  33001  bj-cbv1hv  33032  bj-dral1v  33050  bj-axrep2  33091  bj-axrep3  33092  bj-axrep4  33093  ax11-pm  33121  bj-mo3OLD  33134  bj-snsetex  33253  exlimim  33496  exellim  33499  wl-nfimf1  33622  wl-nfae1  33624  wl-sb8t  33642  wl-sbnf1  33645  wl-lem-moexsb  33659  wl-mo2tf  33662  wl-eutf  33664  wl-mo2t  33666  wl-mo3t  33667  wl-sb8eut  33668  wl-ax11-lem3  33673  wl-sbcom3  33681  sbali  34224  nfbii2  34276  setindtr  38089  axc11next  39105  iotain  39116  pm14.122b  39122  pm14.123b  39125  eubi  39135  ax6e2ndeqVD  39640  e2ebindALT  39660  ax6e2ndeqALT  39662  rexsb  41670
 Copyright terms: Public domain W3C validator