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

Theorem nfa1 1833
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 1832 . 2  |-  ( A. x ph  ->  A. x A. x ph )
21nfi 1597 1  |-  F/ x A. x ph
Colors of variables: wff setvar class
Syntax hints:   A.wal 1368   F/wnf 1590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-ex 1588  df-nf 1591
This theorem is referenced by:  axc4i  1834  nfnf1  1835  nfna1  1839  ax16nf  1879  19.12  1885  nfa2  1888  nfia1  1889  nf2  1897  equs5a  1915  equs5e  1916  cbv1h  1971  dral1  2024  nfald2  2030  ax12v2  2040  equs5  2049  axc14  2070  sbf2  2080  nfsb4t  2087  sbcom3  2112  sbco3  2121  sb56  2139  sbal1OLD  2179  exsb  2188  nfeu1  2273  mo3OLD  2306  eupickbiOLD  2354  moexex  2356  moexexOLD  2357  2eu1OLD  2372  2eu4OLD  2376  2eu6  2378  exists2  2384  nfaba1  2618  nfra1  2877  ceqsalgALT  3096  elrab3t  3215  csbie2t  3416  sbcnestgf  3791  dfnfc2  4209  mpteq12f  4468  axrep2  4505  axrep3  4506  axrep4  4507  alxfr  4605  copsex2t  4678  mosubopt  4689  fv3  5804  fvmptt  5890  fnoprabg  6293  pssnn  7634  fiint  7691  aceq1  8390  zorn2lem4  8771  axpowndlem3  8867  axpowndlem3OLD  8868  zfcndrep  8884  mreexexd  14690  dfon2lem7  27738  wl-nfimf1  28494  wl-nfae1  28496  wl-sb8t  28516  wl-sbnf1  28519  wl-lem-moexsb  28533  wl-mo2t  28536  wl-mo3t  28537  wl-sb8eut  28538  wl-ax11-lem3  28543  wl-sbcom3  28551  sbali  29058  sbcalf  29060  nfbii2  29111  setindtr  29513  axc11next  29800  iotain  29811  pm14.122b  29817  pm14.123b  29820  eubi  29830  rexsb  30132  ax6e2ndeqVD  31947  e2ebindALT  31967  ax6e2ndeqALT  31969  bj-alalbial  32493  bj-exalbial  32494  bj-biexal1  32497  bj-bialal  32500  bj-cbv1hv  32531  bj-ax16nf  32561  bj-dral1v  32563  bj-axc15v  32567  bj-equs5v  32569  bj-sb56  32586  bj-axrep2  32612  bj-axrep3  32613  bj-axrep4  32614  ax11-pm  32642  bj-snsetex  32758
  Copyright terms: Public domain W3C validator