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

Theorem nfa1 1806
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 1804 . 2  |-  ( A. x ph  ->  A. x A. x ph )
21nfi 1560 1  |-  F/ x A. x ph
Colors of variables: wff set class
Syntax hints:   A.wal 1549   F/wnf 1553
This theorem is referenced by:  a5i  1807  nfnf1  1808  nfimdOLD  1828  19.12  1869  nfa2  1874  nfia1  1875  dvelimhw  1876  19.21tOLD  1886  nf2  1889  19.38OLD  1895  equs5a  1909  equs5e  1910  spimtOLD  1956  cbv1h  1974  nfald2  2060  ax11v2  2074  ax11v2OLD  2075  equs5  2085  ax15  2101  sbf2  2107  nfsb4t  2154  nfsb4tOLD  2155  sb56  2173  sbal1  2202  exsb  2206  nfeu1  2290  eupickbi  2346  moexex  2349  2eu1  2360  2eu4  2363  exists2  2370  nfaba1  2576  nfra1  2748  ceqsalg  2972  csbie2t  3287  sbcnestgf  3290  dfnfc2  4025  mpteq12f  4277  axrep2  4314  axrep3  4315  axrep4  4316  copsex2t  4435  mosubopt  4446  ssopab2  4472  alxfr  4728  fv3  5736  fvmptt  5812  fnoprabg  6163  pssnn  7319  fiint  7375  aceq1  7990  zorn2lem4  8371  axpowndlem3  8466  zfcndrep  8481  mreexexd  13865  dfon2lem7  25408  setindtr  27086  ax10ext  27574  iotain  27585  pm14.122b  27591  pm14.123b  27594  eubi  27604  rexsb  27913  a9e2ndeqVD  28958  e2ebindALT  28978  a9e2ndeqALT  28980  nfeqfNEW7  29423  dral2w3AUX7  29439  drex2w3AUX7  29440  exdistrfNEW7  29442  spimtNEW7  29444  ax11v2NEW7  29467  ax15NEW7  29473  a16nfNEW7  29487  sbf2NEW7  29497  nfsb2NEW7  29498  nfsb4twAUX7  29513  sbco2wAUX7  29522  sbcomwAUX7  29525  sb8iwAUX7  29526  sb56NEW7  29533  exsbNEW7  29536  sbal1NEW7  29552  ax7w15lemxAUX7  29603  ax7w15lemAUX7  29604  ax7w14lemAUX7  29606  nfa2OLD7  29629  nfald2OLD7  29654  dvelimfOLD7  29664  nfsb4tOLD7  29682  nfsb4tw2AUXOLD7  29683  dvelimdfOLD7  29688  sbco2OLD7  29689  sbcomOLD7  29692  sb9iOLD7  29695
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator