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

Theorem nfa1 1768
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 1731 . 2  |-  ( A. x ph  ->  A. x A. x ph )
21nfi 1541 1  |-  F/ x A. x ph
Colors of variables: wff set class
Syntax hints:   A.wal 1530   F/wnf 1534
This theorem is referenced by:  nfnf1  1769  a5i  1770  nfimd  1773  nfa2  1789  nfia1  1790  19.21t  1802  nf2  1810  19.38  1822  equs5a  1840  nfald2  1925  spimt  1927  ax11v2  1945  equs5  1949  ax15  1974  sbf2  1981  nfsb4t  2033  sb56  2050  sbal1  2078  exsb  2082  nfeu1  2166  eupickbi  2222  moexex  2225  2eu1  2236  2eu4  2239  exists2  2246  nfaba1  2437  nfra1  2606  ceqsalg  2825  csbie2t  3138  sbcnestgf  3141  dfnfc2  3861  mpteq12f  4112  axrep2  4149  axrep3  4150  axrep4  4151  copsexg  4268  copsex2t  4269  mosubopt  4280  ssopab2  4306  alxfr  4563  fv3  5557  fvmptt  5631  fnoprabg  5961  pssnn  7097  fiint  7149  aceq1  7760  zorn2lem4  8142  axextnd  8229  axrepnd  8232  axunnd  8234  axpowndlem3  8237  axpownd  8239  axregndlem1  8240  zfcndrep  8252  mreexexd  13566  dfon2lem7  24216  qusp  25645  setindtr  27220  ax10ext  27709  iotain  27720  pm14.122b  27726  pm14.123b  27729  eubi  27739  rexsb  28049  a9e2ndeqVD  29001  e2ebindALT  29022  a9e2ndeqALT  29024  nfeqfNEW7  29463  dral2w3AUX7  29479  drex2w3AUX7  29480  exdistrfNEW7  29482  spimtNEW7  29484  ax11v2NEW7  29505  ax15NEW7  29511  a16nfNEW7  29525  sbf2NEW7  29535  nfsb2NEW7  29536  nfsb4twAUX7  29551  sbco2wAUX7  29559  sbco3wAUX7  29561  sbcomwAUX7  29562  sb56NEW7  29568  exsbNEW7  29571  sbal1NEW7  29587  ax7w3AUX7  29621  nfa2OLD7  29646  nfald2OLD7  29671  dvelimfOLD7  29681  nfsb4tOLD7  29699  nfsb4tw2AUXOLD7  29700  dvelimdfOLD7  29705  sbco2OLD7  29706  sbcomOLD7  29709  sb9iOLD7  29712  a12study  29754  a12study2  29756
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-nf 1535
  Copyright terms: Public domain W3C validator