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

Theorem nfd 1778
Description: Deduce that  x is not free in  ps in a context. (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
nfd.1  |-  F/ x ph
nfd.2  |-  ( ph  ->  ( ps  ->  A. x ps ) )
Assertion
Ref Expression
nfd  |-  ( ph  ->  F/ x ps )

Proof of Theorem nfd
StepHypRef Expression
1 nfd.1 . . 3  |-  F/ x ph
2 nfd.2 . . 3  |-  ( ph  ->  ( ps  ->  A. x ps ) )
31, 2alrimi 1777 . 2  |-  ( ph  ->  A. x ( ps 
->  A. x ps )
)
4 df-nf 1551 . 2  |-  ( F/ x ps  <->  A. x
( ps  ->  A. x ps ) )
53, 4sylibr 204 1  |-  ( ph  ->  F/ x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1546   F/wnf 1550
This theorem is referenced by:  nfdh  1779  nfnd  1805  nfndOLD  1806  nfald  1867  nfaldOLD  1868  dvelimhw  1872  nfeqf  2016  dvelimf  2021  dvelimfOLD  2041  a16nf  2108  nfsb2  2115  sbal2  2192  copsexg  4410  riotasv2dOLD  6562  riotasv3dOLD  6566  distel  25382  nfaldwAUX7  29170  nfeqfNEW7  29204  a16nfwAUX7  29264  a16nfNEW7  29266  nfsb2NEW7  29277  nfaldOLD7  29386  dvelimfOLD7  29423  sbal2OLD7  29465
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 1662  ax-8 1683  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator