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

Theorem nfa1 1756
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 1719 . 2  |-  ( A. x ph  ->  A. x A. x ph )
21nfi 1538 1  |-  F/ x A. x ph
Colors of variables: wff set class
Syntax hints:   A.wal 1527   F/wnf 1531
This theorem is referenced by:  nfnf1  1757  a5i  1758  nfimd  1761  nfa2  1777  nfia1  1778  19.21t  1790  nf2  1798  19.38  1810  equs5a  1828  nfald2  1912  spimt  1914  ax11v2  1932  equs5  1936  ax15  1961  sbf2  1968  nfsb4t  2020  sb56  2037  sbal1  2065  exsb  2069  nfeu1  2153  eupickbi  2209  moexex  2212  2eu1  2223  2eu4  2226  exists2  2233  nfaba1  2424  nfra1  2593  ceqsalg  2812  csbie2t  3125  sbcnestgf  3128  dfnfc2  3845  mpteq12f  4096  axrep2  4133  axrep3  4134  axrep4  4135  copsexg  4252  copsex2t  4253  mosubopt  4264  ssopab2  4290  alxfr  4547  fv3  5541  fvmptt  5615  fnoprabg  5945  pssnn  7081  fiint  7133  aceq1  7744  zorn2lem4  8126  axextnd  8213  axrepnd  8216  axunnd  8218  axpowndlem3  8221  axpownd  8223  axregndlem1  8224  zfcndrep  8236  mreexexd  13550  dfon2lem7  24145  qusp  25542  setindtr  27117  ax10ext  27606  iotain  27617  pm14.122b  27623  pm14.123b  27626  eubi  27636  rexsb  27946  a9e2ndeqVD  28685  e2ebindALT  28706  a9e2ndeqALT  28708  a12study  29132  a12study2  29134
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-nf 1532
  Copyright terms: Public domain W3C validator