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

Theorem rspcedv 3214
Description: Restricted existential specialization, using implicit substitution. (Contributed by FL, 17-Apr-2007.) (Revised by Mario Carneiro, 4-Jan-2017.)
Hypotheses
Ref Expression
rspcdv.1
rspcdv.2
Assertion
Ref Expression
rspcedv
Distinct variable groups:   ,   ,   ,   ,

Proof of Theorem rspcedv
StepHypRef Expression
1 rspcdv.1 . 2
2 rspcdv.2 . . 3
32biimprd 223 . 2
41, 3rspcimedv 3212 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:  rspcedvd  3215  fsuppmapnn0fiub  12097  0csh0  12764  gcdcllem1  14149  nn0gsumfz  17012  pmatcollpw3lem  19284  pmatcollpw3fi1lem2  19288  pm2mpfo  19315  f1otrg  24174  cusgrafilem2  24480  wwlknredwwlkn  24726  wwlkextprop  24744  numclwwlkun  25079  xrofsup  27582  rexzrexnn0  30737  lcoel0  33029  lcoss  33037  el0ldep  33067  ldepspr  33074  islindeps2  33084  isldepslvec2  33086
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