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

Theorem nfa1 1807
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 1805 . 2  |-  ( A. x ph  ->  A. x A. x ph )
21nfi 1561 1  |-  F/ x A. x ph
Colors of variables: wff set class
Syntax hints:   A.wal 1550   F/wnf 1554
This theorem is referenced by:  a5i  1808  nfnf1  1809  nfimdOLD  1829  19.12  1870  nfa2  1875  nfia1  1876  dvelimhw  1877  19.21tOLD  1887  nf2  1890  19.38OLD  1896  equs5a  1910  equs5e  1911  spimtOLD  1957  cbv1h  1975  nfald2  2065  ax11v2  2079  ax11v2OLD  2080  equs5  2090  ax15  2109  sbf2  2121  nfsb4t  2129  nfsb4tOLD  2130  sb56  2176  sbal1  2205  exsb  2209  nfeu1  2293  eupickbi  2349  moexex  2352  2eu1  2363  2eu4  2366  exists2  2373  nfaba1  2579  nfra1  2758  ceqsalg  2982  csbie2t  3297  sbcnestgf  3300  dfnfc2  4035  mpteq12f  4288  axrep2  4325  axrep3  4326  axrep4  4327  copsex2t  4446  mosubopt  4457  ssopab2  4483  alxfr  4739  fv3  5747  fvmptt  5823  fnoprabg  6174  pssnn  7330  fiint  7386  aceq1  8003  zorn2lem4  8384  axpowndlem3  8479  zfcndrep  8494  mreexexd  13878  dfon2lem7  25421  setindtr  27109  ax10ext  27597  iotain  27608  pm14.122b  27614  pm14.123b  27617  eubi  27627  rexsb  27936  a9e2ndeqVD  29095  e2ebindALT  29115  a9e2ndeqALT  29117  nfeqfNEW7  29560  dral2w3AUX7  29576  drex2w3AUX7  29577  exdistrfNEW7  29579  spimtNEW7  29581  ax11v2NEW7  29604  ax15NEW7  29610  a16nfNEW7  29624  sbf2NEW7  29634  nfsb2NEW7  29635  nfsb4twAUX7  29650  sbco2wAUX7  29659  sbcomwAUX7  29662  sb8iwAUX7  29663  sb56NEW7  29670  exsbNEW7  29673  sbal1NEW7  29689  ax7w15lemxAUX7  29740  ax7w15lemAUX7  29741  ax7w14lemAUX7  29743  nfa2OLD7  29766  nfald2OLD7  29791  dvelimfOLD7  29801  nfsb4tOLD7  29819  nfsb4tw2AUXOLD7  29820  dvelimdfOLD7  29825  sbco2OLD7  29826  sbcomOLD7  29829  sb9iOLD7  29832
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-nf 1555
  Copyright terms: Public domain W3C validator