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

Theorem nfvd 1627
Description: nfv 1626 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1823. (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 1626 . 2  |-  F/ x ps
21a1i 11 1  |-  ( ph  ->  F/ x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   F/wnf 1550
This theorem is referenced by:  cbvald  2062  cbvaldva  2064  cbvexdva  2065  sbiedv  2090  vtocld  2968  sbcied  3161  nfunid  3986  iota2d  5406  iota2  5407  mpt2xopoveq  6433  opiota  6498  riota5f  6537  riotasvdOLD  6556  riotasv2d  6557  riotasv2dOLD  6558  riotasv3dOLD  6562  axrepndlem1  8427  axunndlem1  8430  xrofsup  24083  sbiedvNEW7  29337  cbvaldOLD7  29422  cbvaldvaOLD7  29424  cbvexdvaOLD7  29425  cdleme42b  30964  dihvalcqpre  31722  mapdheq  32215  hdmap1eq  32289  hdmapval2lem  32321
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-17 1623
This theorem depends on definitions:  df-bi 178  df-nf 1551
  Copyright terms: Public domain W3C validator