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

Theorem nfvd 1915
Description: nfv 1914 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1894. (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 1914 . 2 𝑥𝜓
21a1i 11 1 (𝜑 → Ⅎ𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-5 1910
This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784
This theorem is referenced by:  cbvaldw  2340  cbvald  2412  cbvaldva  2414  cbvexdva  2415  sbiedv  2509  nfmodv  2559  nfabdw  2927  cbvexeqsetf  3495  nfunid  4913  nfopabd  5211  copsexgw  5495  nfiotadw  6517  iota2d  6549  iota2  6550  riota5f  7416  oprabidw  7462  opiota  8084  mpoxopoveq  8244  nfttrcld  9750  axrepndlem1  10632  axunndlem1  10635  fproddivf  16023  xrofsup  32771  dvelimalcasei  35090  dvelimexcasei  35092  axsepg2  35096  axsepg2ALT  35097  axnulg  35106  bj-cbvaldvav  36804  bj-cbvexdvav  36805  opelopabbv  37144  brabd  37149  cbveud  37373  cbvreud  37374  fvineqsneu  37412  wl-mo2t  37576  wl-sb8eut  37579  wl-sb8eutv  37580  wl-issetft  37583  riotasv2d  38958  cdleme42b  40480  dihvalcqpre  41237  mapdheq  41730  hdmap1eq  41803  hdmapval2lem  41833
  Copyright terms: Public domain W3C validator