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

Step	Hyp	Ref	Expression
1		rspcdv.1	. 2
2		rspcdv.2	. . 3
3	2	biimprd 223	. 2
4	1, 3	rspcimedv 3212	1

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