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

Theorem nfd 1783
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 1782 . 2  |-  ( ph  ->  A. x ( ps 
->  A. x ps )
)
4 df-nf 1555 . 2  |-  ( F/ x ps  <->  A. x
( ps  ->  A. x ps ) )
53, 4sylibr 205 1  |-  ( ph  ->  F/ x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1550   F/wnf 1554
This theorem is referenced by:  nfdh  1784  nfnd  1810  nfndOLD  1811  nfald  1872  nfaldOLD  1873  dvelimhw  1877  cbv1h  1975  a16nf  2054  nfeqfOLD  2055  dvelimfOLD  2070  nfsb2  2098  sbal2  2213  copsexg  4445  riotasv2dOLD  6598  riotasv3dOLD  6602  distel  25436  nfaldwAUX7  29526  nfeqfNEW7  29560  a16nfwAUX7  29622  a16nfNEW7  29624  nfsb2NEW7  29635  sb8dwAUX7  29664  nfaldOLD7  29764  dvelimfOLD7  29801  sbal2OLD7  29842
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-11 1762
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-nf 1555
  Copyright terms: Public domain W3C validator