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

Theorem nfd 1758
Description: Deduce that  x is not free in  ph 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 1757 . 2  |-  ( ph  ->  A. x ( ps 
->  A. x ps )
)
4 df-nf 1535 . 2  |-  ( F/ x ps  <->  A. x
( ps  ->  A. x ps ) )
53, 4sylibr 203 1  |-  ( ph  ->  F/ x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1530   F/wnf 1534
This theorem is referenced by:  nfdh  1759  nfnd  1772  nfald  1787  nfeqf  1911  dvelimf  1950  a16nf  2004  nfsb2  2011  sbal2  2086  copsexg  4268  riotasv2dOLD  6366  riotasv3dOLD  6370  distel  24231  nfaldwAUX7  29429  nfeqfNEW7  29463  a16nfwAUX7  29523  a16nfNEW7  29525  nfsb2NEW7  29536  nfaldOLD7  29644  dvelimfOLD7  29681  sbal2OLD7  29724
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-11 1727
This theorem depends on definitions:  df-bi 177  df-nf 1535
  Copyright terms: Public domain W3C validator