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

Theorem nfvd 1910
Description: nfv 1909 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1889. (Contributed by Mario Carneiro, 6-Oct-2016.)
Assertion
Ref Expression
nfvd (𝜑 → Ⅎ𝑥𝜓)
Distinct variable group:   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem nfvd
StepHypRef Expression
1 nfv 1909 . 2 𝑥𝜓
21a1i 11 1 (𝜑 → Ⅎ𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-5 1905
This theorem depends on definitions:  df-bi 206  df-ex 1774  df-nf 1778
This theorem is referenced by:  cbvaldw  2328  cbvald  2400  cbvaldva  2402  cbvexdva  2403  sbiedv  2497  nfmodv  2547  nfabdw  2915  issetft  3475  vtocldOLD  3539  sbciedOLD  3820  nfunid  4915  nfopabd  5217  copsexgw  5492  nfiotadw  6504  iota2d  6537  iota2  6538  riota5f  7404  oprabidw  7450  opiota  8064  mpoxopoveq  8225  nfttrcld  9735  axrepndlem1  10617  axunndlem1  10620  fproddivf  15967  xrofsup  32619  bj-cbvaldvav  36411  bj-cbvexdvav  36412  opelopabbv  36753  brabd  36758  cbveud  36982  cbvreud  36983  fvineqsneu  37021  wl-mo2t  37173  wl-sb8eut  37176  wl-sb8eutv  37177  wl-issetft  37180  riotasv2d  38559  cdleme42b  40081  dihvalcqpre  40838  mapdheq  41331  hdmap1eq  41404  hdmapval2lem  41434
  Copyright terms: Public domain W3C validator