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

Theorem nfvd 1606
Description: nfv 1605 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1761. (Contributed by Mario Carneiro, 6-Oct-2016.)
Assertion
Ref Expression
nfvd  |-  ( ph  ->  F/ x ps )
Distinct variable group:    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem nfvd
StepHypRef Expression
1 nfv 1605 . 2  |-  F/ x ps
21a1i 10 1  |-  ( ph  ->  F/ x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   F/wnf 1531
This theorem is referenced by:  cbvald  1948  cbvaldva  1950  cbvexdva  1951  sbiedv  1977  vtocld  2836  sbcied  3027  nfunid  3834  iota2d  5244  iota2  5245  opiota  6290  riota5f  6329  riotasvdOLD  6348  riotasv2d  6349  riotasv2dOLD  6350  riotasv3dOLD  6354  isinf  7076  axrepndlem1  8214  axunndlem1  8217  xrofsup  23255  prtlem5  26722  mpt2xopoveq  28085  cdleme42b  30667  dihvalcqpre  31425  mapdheq  31918  hdmap1eq  31992  hdmapval2lem  32024
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-17 1603
This theorem depends on definitions:  df-bi 177  df-nf 1532
  Copyright terms: Public domain W3C validator