Theorem ssrexv 3405

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 3338	. . 3 |- ( A C_ B -> ( x e. A -> x e. B ) )
2	1	anim1d 559	. 2 |- ( A C_ B -> ( ( x e. A /\ ph ) -> ( x e. B /\ ph ) ) )
3	2	reximdv2 2815	1 |- ( A C_ B -> ( E. x e. A ph -> E. x e. B ph ) )

Syntax hints:   -> wi 4   e. wcel 1755   E.wrex 2706   C_ wss 3316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-rex 2711  df-in 3323  df-ss 3330

This theorem is referenced by:  iunss1  4170  onfr  4745  moriotass  6069  frxp  6671  frfi  7545  fisupcl  7705  brwdom3  7785  unwdomg  7787  tcrank  8079  hsmexlem2  8584  pwfseqlem3  8814  grur1  8974  suplem1pr  9208  fimaxre2  10265  lbzbi  10930  suprzub  10933  uzsupss  10934  zmin  10936  rexico  12824  rlim3  12959  rlimclim  13007  caurcvgr  13134  alzdvds  13565  bitsfzolem  13612  pclem  13887  0ram2  14064  0ramcl  14066  symgextfo  15906  lsmless1x  16122  lsmless2x  16123  dprdss  16499  ablfac2  16563  subrgdvds  16802  ssrest  18621  fbun  19254  fgss  19287  isucn2  19695  metustOLD  19983  metust  19984  metutopOLD  19998  psmetutop  19999  lebnumlem3  20376  lebnum  20377  cfil3i  20621  cfilss  20622  fgcfil  20623  iscau4  20631  ivthle  20781  ivthle2  20782  lhop1lem  21326  lhop2  21328  ply1divex  21492  plyss  21551  dgrlem  21581  elqaa  21672  aannenlem2  21679  reeff1olem  21795  rlimcnp  22243  ftalem3  22296  pntlem3  22742  tgisline  22905  axcontlem2  23033  shless  24584  xlt2addrd  25875  ssnnssfz  25898  xreceu  25919  archirngz  26029  archiabllem1b  26032  esumpcvgval  26380  sigaclci  26428  eulerpartlemgvv  26606  eulerpartlemgh  26608  signsply0  26799  iccllyscon  26986  frmin  27549  nodenselem4  27671  volsupnfl  28277  locfincf  28419  fgmin  28432  cover2  28448  filbcmb  28475  istotbnd3  28511  sstotbnd  28515  heibor1lem  28549  isdrngo2  28605  isdrngo3  28606  pellfundre  29064  pellfundge  29065  pellfundglb  29068  hbtlem3  29325  hbtlem5  29326  itgoss  29362  scshwfzeqfzo  30335  frgrawopreg1  30486  frgrawopreg2  30487  pgrpgt2nabel  30597  islsati  32209  paddss1  33031  paddss2  33032  hdmap14lem2a  35085