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

Theorem rspcedvd 3215
 Description: Restricted existential specialization, using implicit substitution. Variant of rspcdv 3213. (Contributed by AV, 27-Nov-2019.)
Hypotheses
Ref Expression
rspcedvd.1
rspcedvd.2
rspcedvd.3
Assertion
Ref Expression
rspcedvd
Distinct variable groups:   ,   ,   ,   ,

Proof of Theorem rspcedvd
StepHypRef Expression
1 rspcedvd.3 . 2
2 rspcedvd.1 . . 3
3 rspcedvd.2 . . 3
42, 3rspcedv 3214 . 2
51, 4mpd 15 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  E.wrex 2808 This theorem is referenced by:  rspcedeq1vd  3216  rspcedeq2vd  3217  ssnn0fi  12094  fsuppmapnn0fiubex  12098  isnsgrp  15915  mgmnsgrpex  16049  sgrpnmndex  16050  cply1coe0bi  18342  scmatid  19016  scmataddcl  19018  scmatsubcl  19019  scmatmulcl  19020  scmatrhmcl  19030  mat0scmat  19040  symgmatr01lem  19155  pmatcoe1fsupp  19202  cpmatacl  19217  cpmatinvcl  19218  m2cpmfo  19257  pmatcollpw3fi1lem2  19288  f1otrg  24174  fargshiftfo  24638  usg2cwwkdifex  24821  numclwlk1lem2fo  25095  usgvincvad  32404  usgvincvadALT  32407  1odd  32499  nnsgrpnmnd  32506  fullestrcsetc  32657  equivestrcsetc  32658  fullsetcestrc  32672  0even  32737  2even  32739  2zlidl  32740  2zrngamgm  32745  2zrngamnd  32747  2zrngagrp  32749  2zrngmmgm  32752  2zrngnmlid  32755  ply1mulgsumlem1  32986  ply1mulgsumlem2  32987  el0ldep  33067  imo72b2lem0  37982  imo72b2lem2  37984  imo72b2lem1  37988  imo72b2  37993 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-v 3111
 Copyright terms: Public domain W3C validator