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

Theorem nfvd 1708
Description: nfv 1707 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1917. (Contributed by Mario Carneiro, 6-Oct-2016.)
Assertion
Ref Expression
nfvd
Distinct variable group:   ,

Proof of Theorem nfvd
StepHypRef Expression
1 nfv 1707 . 2
21a1i 11 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  F/wnf 1616
This theorem is referenced by:  cbvald  2025  cbvaldva  2032  cbvexdva  2033  sbiedv  2152  vtocld  3159  sbcied  3364  nfunid  4256  iota2d  5581  iota2  5582  riota5f  6282  opiota  6859  mpt2xopoveq  6966  axrepndlem1  8988  axunndlem1  8991  xrofsup  27582  wl-mo2t  30020  wl-sb8eut  30022  fproddivf  31588  bj-cbvaldvav  34306  bj-cbvexdvav  34307  riotasv2d  34688  cdleme42b  36204  dihvalcqpre  36962  mapdheq  37455  hdmap1eq  37529  hdmapval2lem  37561
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-5 1704
This theorem depends on definitions:  df-bi 185  df-nf 1617
  Copyright terms: Public domain W3C validator