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

Theorem nfa1 1840
Description:  x is not free in  A. x ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfa1  |-  F/ x A. x ph

Proof of Theorem nfa1
StepHypRef Expression
1 hba1 1839 . 2  |-  ( A. x ph  ->  A. x A. x ph )
21nfi 1601 1  |-  F/ x A. x ph
Colors of variables: wff setvar class
Syntax hints:   A.wal 1372   F/wnf 1594
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-12 1798
This theorem depends on definitions:  df-bi 185  df-ex 1592  df-nf 1595
This theorem is referenced by:  axc4i  1841  nfnf1  1842  nfna1  1846  ax16nf  1886  19.12  1892  nfa2  1895  nfia1  1896  nf2  1904  equs5a  1922  equs5e  1923  cbv1h  1982  dral1  2035  nfald2  2041  ax12v2  2051  equs5  2060  axc14  2081  sbf2  2091  nfsb4t  2098  sbcom3  2123  sbco3  2132  sb56  2149  sbal1OLD  2189  exsb  2198  nfeu1  2283  mo3OLD  2316  eupickbiOLD  2364  moexex  2366  moexexOLD  2367  2eu1OLD  2382  2eu4OLD  2386  2eu6  2388  exists2  2394  nfaba1  2629  nfra1  2840  ceqsalgALT  3134  elrab3t  3255  csbie2t  3459  sbcnestgf  3834  dfnfc2  4258  mpteq12f  4518  axrep2  4555  axrep3  4556  axrep4  4557  alxfr  4655  copsex2t  4729  mosubopt  4740  fv3  5872  fvmptt  5958  fnoprabg  6380  pssnn  7730  fiint  7788  aceq1  8489  zorn2lem4  8870  axpowndlem3  8966  axpowndlem3OLD  8967  zfcndrep  8983  mreexexd  14894  dfon2lem7  28786  wl-nfimf1  29543  wl-nfae1  29545  wl-sb8t  29565  wl-sbnf1  29568  wl-lem-moexsb  29582  wl-mo2t  29585  wl-mo3t  29586  wl-sb8eut  29587  wl-ax11-lem3  29592  wl-sbcom3  29600  sbali  30107  sbcalf  30109  nfbii2  30160  setindtr  30561  axc11next  30848  iotain  30859  pm14.122b  30865  pm14.123b  30868  eubi  30878  rexsb  31597  ax6e2ndeqVD  32666  e2ebindALT  32686  ax6e2ndeqALT  32688  bj-alalbial  33214  bj-exalbial  33215  bj-biexal1  33218  bj-bialal  33221  bj-cbv1hv  33252  bj-ax16nf  33282  bj-dral1v  33284  bj-axc15v  33288  bj-equs5v  33290  bj-sb56  33307  bj-axrep2  33333  bj-axrep3  33334  bj-axrep4  33335  ax11-pm  33363  bj-snsetex  33479
  Copyright terms: Public domain W3C validator