Theorem ssrexv 3564

Description: Existential quantification restricted to a subclass. (Contributed by NM, 11-Jan-2007.)

Assertion

Ref	Expression
ssrexv

Distinct variable groups:   ,   ,

Proof of Theorem ssrexv

Step	Hyp	Ref	Expression
1		ssel 3497	. . 3
2	1	anim1d 564	. 2
3	2	reximdv2 2928	1

Syntax hints:  ->wi 4  e.wcel 1818  E.wrex 2808  C_wss 3475

This theorem is referenced by:  iunss1  4342  onfr  4922  moriotass  6286  frxp  6910  frfi  7785  fisupcl  7948  supgtoreq  7949  brwdom3  8029  unwdomg  8031  tcrank  8323  hsmexlem2  8828  pwfseqlem3  9059  grur1  9219  suplem1pr  9451  fimaxre2  10516  suprfinzcl  11003  lbzbi  11199  suprzub  11202  uzsupss  11203  zmin  11207  ssnn0fi  12094  scshwfzeqfzo  12794  rexico  13186  rlim3  13321  rlimclim  13369  caurcvgr  13496  alzdvds  14036  bitsfzolem  14084  pclem  14362  0ram2  14539  0ramcl  14541  symgextfo  16447  lsmless1x  16664  lsmless2x  16665  dprdss  17076  ablfac2  17140  subrgdvds  17443  ssrest  19677  locfincf  20032  fbun  20341  fgss  20374  isucn2  20782  metustOLD  21070  metust  21071  metutopOLD  21085  psmetutop  21086  lebnumlem3  21463  lebnum  21464  cfil3i  21708  cfilss  21709  fgcfil  21710  iscau4  21718  ivthle  21868  ivthle2  21869  lhop1lem  22414  lhop2  22416  ply1divex  22537  plyss  22596  dgrlem  22626  elqaa  22718  aannenlem2  22725  reeff1olem  22841  rlimcnp  23295  ftalem3  23348  pntlem3  23794  tgisline  24007  axcontlem2  24268  frgrawopreg1  25050  frgrawopreg2  25051  shless  26277  xlt2addrd  27578  ssnnssfz  27597  xreceu  27618  archirngz  27733  archiabllem1b  27736  locfinreflem  27843  crefss  27852  esumpcvgval  28084  sigaclci  28132  eulerpartlemgvv  28315  eulerpartlemgh  28317  signsply0  28508  iccllyscon  28695  frmin  29322  nodenselem4  29444  volsupnfl  30059  fgmin  30188  cover2  30204  filbcmb  30231  istotbnd3  30267  sstotbnd  30271  heibor1lem  30305  isdrngo2  30361  isdrngo3  30362  pellfundre  30817  pellfundge  30818  pellfundglb  30821  hbtlem3  31076  hbtlem5  31077  itgoss  31112  radcnvrat  31195  fourierdlem20  31909  ssnn0ssfz  32938  pgrpgt2nabl  32959  islsati  34719  paddss1  35541  paddss2  35542  hdmap14lem2a  37597

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-rex 2813  df-in 3482  df-ss 3489