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

Theorem nfvd 1684
Description: nfv 1683 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1864. (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 1683 . 2  |-  F/ x ps
21a1i 11 1  |-  ( ph  ->  F/ x ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   F/wnf 1599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-nf 1600
This theorem is referenced by:  cbvald  1998  cbvaldva  2005  cbvexdva  2006  sbiedv  2127  vtocld  3168  sbcied  3373  nfunid  4258  iota2d  5582  iota2  5583  riota5f  6281  opiota  6854  mpt2xopoveq  6959  axrepndlem1  8979  axunndlem1  8982  xrofsup  27413  wl-mo2t  29954  wl-sb8eut  29956  bj-cbvaldvav  33794  bj-cbvexdvav  33795  riotasv2d  34166  cdleme42b  35680  dihvalcqpre  36438  mapdheq  36931  hdmap1eq  37005  hdmapval2lem  37037
  Copyright terms: Public domain W3C validator