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

Theorem nfa1 1796
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 1794 . 2  |-  ( A. x ph  ->  A. x A. x ph )
21nfi 1557 1  |-  F/ x A. x ph
Colors of variables: wff set class
Syntax hints:   A.wal 1546   F/wnf 1550
This theorem is referenced by:  a5i  1797  nfnf1  1798  nfimdOLD  1818  19.12  1859  nfa2  1867  nfia1  1868  19.21tOLD  1875  nf2  1878  19.38OLD  1884  equs5a  1898  equs5e  1899  spimtOLD  1947  nfald2  2016  ax11v2  2031  equs5  2035  ax15  2056  sbf2  2063  nfsb4t  2115  sb56  2133  sbal1  2162  exsb  2166  nfeu1  2250  eupickbi  2306  moexex  2309  2eu1  2320  2eu4  2323  exists2  2330  nfaba1  2530  nfra1  2701  ceqsalg  2925  csbie2t  3240  sbcnestgf  3243  dfnfc2  3977  mpteq12f  4228  axrep2  4265  axrep3  4266  axrep4  4267  copsex2t  4386  mosubopt  4397  ssopab2  4423  alxfr  4678  fv3  5686  fvmptt  5761  fnoprabg  6112  pssnn  7265  fiint  7321  aceq1  7933  zorn2lem4  8314  axpowndlem3  8409  zfcndrep  8424  mreexexd  13802  dfon2lem7  25171  setindtr  26788  ax10ext  27277  iotain  27288  pm14.122b  27294  pm14.123b  27297  eubi  27307  rexsb  27616  a9e2ndeqVD  28364  e2ebindALT  28385  a9e2ndeqALT  28387  nfeqfNEW7  28826  dral2w3AUX7  28842  drex2w3AUX7  28843  exdistrfNEW7  28845  spimtNEW7  28847  ax11v2NEW7  28868  ax15NEW7  28874  a16nfNEW7  28888  sbf2NEW7  28898  nfsb2NEW7  28899  nfsb4twAUX7  28914  sbco2wAUX7  28922  sbcomwAUX7  28925  sb56NEW7  28931  exsbNEW7  28934  sbal1NEW7  28950  nfa2OLD7  29010  nfald2OLD7  29035  dvelimfOLD7  29045  nfsb4tOLD7  29063  nfsb4tw2AUXOLD7  29064  dvelimdfOLD7  29069  sbco2OLD7  29070  sbcomOLD7  29073  sb9iOLD7  29076
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator