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

Theorem nfvd 1620
Description: nfv 1619 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1810. (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 1619 . 2  |-  F/ x ps
21a1i 10 1  |-  ( ph  ->  F/ x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   F/wnf 1544
This theorem is referenced by:  cbvald  2013  cbvaldva  2015  cbvexdva  2016  sbiedv  2042  vtocld  2912  sbcied  3103  nfunid  3913  iota2d  5323  iota2  5324  opiota  6374  riota5f  6413  riotasvdOLD  6432  riotasv2d  6433  riotasv2dOLD  6434  riotasv3dOLD  6438  isinf  7161  axrepndlem1  8301  axunndlem1  8304  xrofsup  23324  prtlem5  26045  mpt2xopoveq  27439  sbiedvNEW7  29033  cbvaldOLD7  29118  cbvaldvaOLD7  29120  cbvexdvaOLD7  29121  cdleme42b  30719  dihvalcqpre  31477  mapdheq  31970  hdmap1eq  32044  hdmapval2lem  32076
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-17 1616
This theorem depends on definitions:  df-bi 177  df-nf 1545
  Copyright terms: Public domain W3C validator