Theorem ssrexv 3422

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

Assertion

Ref	Expression
ssrexv	|- ( A C_ B -> ( E. x e. A ph -> E. x e. B ph ) )

Distinct variable groups:   x, A   x, B

Allowed substitution hint:   ph( x)

Proof of Theorem ssrexv

Step	Hyp	Ref	Expression
1		ssel 3355	. . 3 |- ( A C_ B -> ( x e. A -> x e. B ) )
2	1	anim1d 564	. 2 |- ( A C_ B -> ( ( x e. A /\ ph ) -> ( x e. B /\ ph ) ) )
3	2	reximdv2 2830	1 |- ( A C_ B -> ( E. x e. A ph -> E. x e. B ph ) )

Syntax hints:   -> wi 4   e. wcel 1756   E.wrex 2721   C_ wss 3333

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-rex 2726  df-in 3340  df-ss 3347

This theorem is referenced by:  iunss1  4187  onfr  4763  moriotass  6086  frxp  6687  frfi  7562  fisupcl  7722  brwdom3  7802  unwdomg  7804  tcrank  8096  hsmexlem2  8601  pwfseqlem3  8832  grur1  8992  suplem1pr  9226  fimaxre2  10283  lbzbi  10948  suprzub  10951  uzsupss  10952  zmin  10954  rexico  12846  rlim3  12981  rlimclim  13029  caurcvgr  13156  alzdvds  13588  bitsfzolem  13635  pclem  13910  0ram2  14087  0ramcl  14089  symgextfo  15932  lsmless1x  16148  lsmless2x  16149  dprdss  16531  ablfac2  16595  subrgdvds  16884  ssrest  18785  fbun  19418  fgss  19451  isucn2  19859  metustOLD  20147  metust  20148  metutopOLD  20162  psmetutop  20163  lebnumlem3  20540  lebnum  20541  cfil3i  20785  cfilss  20786  fgcfil  20787  iscau4  20795  ivthle  20945  ivthle2  20946  lhop1lem  21490  lhop2  21492  ply1divex  21613  plyss  21672  dgrlem  21702  elqaa  21793  aannenlem2  21800  reeff1olem  21916  rlimcnp  22364  ftalem3  22417  pntlem3  22863  tgisline  23039  axcontlem2  23216  shless  24767  xlt2addrd  26056  ssnnssfz  26081  xreceu  26102  archirngz  26211  archiabllem1b  26214  esumpcvgval  26532  sigaclci  26580  eulerpartlemgvv  26764  eulerpartlemgh  26766  signsply0  26957  iccllyscon  27144  frmin  27708  nodenselem4  27830  volsupnfl  28441  locfincf  28583  fgmin  28596  cover2  28612  filbcmb  28639  istotbnd3  28675  sstotbnd  28679  heibor1lem  28713  isdrngo2  28769  isdrngo3  28770  pellfundre  29227  pellfundge  29228  pellfundglb  29231  hbtlem3  29488  hbtlem5  29489  itgoss  29525  scshwfzeqfzo  30497  frgrawopreg1  30648  frgrawopreg2  30649  ssnn0ssfz  30746  supgtoreq  30748  suprfinzcl  30750  ssnn0fi  30751  pgrpgt2nabel  30774  islsati  32644  paddss1  33466  paddss2  33467  hdmap14lem2a  35520