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

Theorem nfvd 1631
Description: nfv 1630 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1829. (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 1630 . 2  |-  F/ x ps
21a1i 11 1  |-  ( ph  ->  F/ x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   F/wnf 1554
This theorem is referenced by:  cbvaldOLD  1990  cbvaldva  1997  cbvexdva  1998  sbiedv  2159  vtocld  3010  sbcied  3203  nfunid  4046  iota2d  5472  iota2  5473  mpt2xopoveq  6499  opiota  6564  riota5f  6603  riotasvdOLD  6622  riotasv2d  6623  riotasv2dOLD  6624  riotasv3dOLD  6628  axrepndlem1  8498  axunndlem1  8501  xrofsup  24157  cbvaldwAUX7  29613  sbiedvNEW7  29730  cbvaldOLD7  29832  cbvaldvaOLD7  29834  cbvexdvaOLD7  29835  cdleme42b  31373  dihvalcqpre  32131  mapdheq  32624  hdmap1eq  32698  hdmapval2lem  32730
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-17 1627
This theorem depends on definitions:  df-bi 179  df-nf 1555
  Copyright terms: Public domain W3C validator