Theorem ssrexv 3479

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

Syntax hints:   -> wi 4   e. wcel 1826   E.wrex 2733   C_ wss 3389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-rex 2738  df-in 3396  df-ss 3403

This theorem is referenced by:  iunss1  4255  onfr  4831  moriotass  6186  frxp  6809  frfi  7680  fisupcl  7842  supgtoreq  7843  brwdom3  7923  unwdomg  7925  tcrank  8215  hsmexlem2  8720  pwfseqlem3  8949  grur1  9109  suplem1pr  9341  fimaxre2  10407  suprfinzcl  10894  lbzbi  11089  suprzub  11092  uzsupss  11093  zmin  11097  ssnn0fi  11997  scshwfzeqfzo  12705  rexico  13188  rlim3  13323  rlimclim  13371  caurcvgr  13498  alzdvds  14038  bitsfzolem  14086  pclem  14364  0ram2  14541  0ramcl  14543  symgextfo  16564  lsmless1x  16781  lsmless2x  16782  dprdss  17189  ablfac2  17253  subrgdvds  17556  ssrest  19763  locfincf  20117  fbun  20426  fgss  20459  isucn2  20867  metustOLD  21155  metust  21156  metutopOLD  21170  psmetutop  21171  lebnumlem3  21548  lebnum  21549  cfil3i  21793  cfilss  21794  fgcfil  21795  iscau4  21803  ivthle  21953  ivthle2  21954  lhop1lem  22499  lhop2  22501  ply1divex  22622  plyss  22681  dgrlem  22711  elqaa  22803  aannenlem2  22810  reeff1olem  22926  rlimcnp  23412  ftalem3  23465  pntlem3  23911  tgisline  24127  axcontlem2  24389  frgrawopreg1  25171  frgrawopreg2  25172  shless  26394  xlt2addrd  27728  ssnnssfz  27750  xreceu  27771  archirngz  27886  archiabllem1b  27889  locfinreflem  27997  crefss  28006  esumpcvgval  28226  sigaclci  28281  eulerpartlemgvv  28498  eulerpartlemgh  28500  signsply0  28691  iccllyscon  28884  frmin  29487  nodenselem4  29609  volsupnfl  30224  fgmin  30354  cover2  30370  filbcmb  30397  istotbnd3  30433  sstotbnd  30437  heibor1lem  30471  isdrngo2  30527  isdrngo3  30528  pellfundre  30982  pellfundge  30983  pellfundglb  30986  hbtlem3  31244  hbtlem5  31245  itgoss  31280  radcnvrat  31363  fourierdlem20  32075  ssnn0ssfz  33138  pgrpgt2nabl  33159  islsati  35132  paddss1  35954  paddss2  35955  hdmap14lem2a  38010