Theorem ssrexv 3550

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 3483	. . 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 2914	1 |- ( A C_ B -> ( E. x e. A ph -> E. x e. B ph ) )

Syntax hints:   -> wi 4   e. wcel 1804   E.wrex 2794   C_ wss 3461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-rex 2799  df-in 3468  df-ss 3475

This theorem is referenced by:  iunss1  4327  onfr  4907  moriotass  6271  frxp  6895  frfi  7767  fisupcl  7930  supgtoreq  7931  brwdom3  8011  unwdomg  8013  tcrank  8305  hsmexlem2  8810  pwfseqlem3  9041  grur1  9201  suplem1pr  9433  fimaxre2  10497  suprfinzcl  10983  lbzbi  11179  suprzub  11182  uzsupss  11183  zmin  11187  ssnn0fi  12073  scshwfzeqfzo  12773  rexico  13165  rlim3  13300  rlimclim  13348  caurcvgr  13475  alzdvds  13913  bitsfzolem  13961  pclem  14239  0ram2  14416  0ramcl  14418  symgextfo  16321  lsmless1x  16538  lsmless2x  16539  dprdss  16950  ablfac2  17014  subrgdvds  17317  ssrest  19550  locfincf  19905  fbun  20214  fgss  20247  isucn2  20655  metustOLD  20943  metust  20944  metutopOLD  20958  psmetutop  20959  lebnumlem3  21336  lebnum  21337  cfil3i  21581  cfilss  21582  fgcfil  21583  iscau4  21591  ivthle  21741  ivthle2  21742  lhop1lem  22287  lhop2  22289  ply1divex  22410  plyss  22469  dgrlem  22499  elqaa  22590  aannenlem2  22597  reeff1olem  22713  rlimcnp  23167  ftalem3  23220  pntlem3  23666  tgisline  23879  axcontlem2  24140  frgrawopreg1  24922  frgrawopreg2  24923  shless  26149  xlt2addrd  27450  ssnnssfz  27469  xreceu  27491  archirngz  27606  archiabllem1b  27609  locfinreflem  27716  crefss  27725  esumpcvgval  27957  sigaclci  28005  eulerpartlemgvv  28188  eulerpartlemgh  28190  signsply0  28381  iccllyscon  28568  frmin  29297  nodenselem4  29419  volsupnfl  30034  fgmin  30163  cover2  30179  filbcmb  30206  istotbnd3  30242  sstotbnd  30246  heibor1lem  30280  isdrngo2  30336  isdrngo3  30337  pellfundre  30792  pellfundge  30793  pellfundglb  30796  hbtlem3  31051  hbtlem5  31052  itgoss  31088  radcnvrat  31171  fourierdlem20  31798  ssnn0ssfz  32671  pgrpgt2nabl  32692  islsati  34459  paddss1  35281  paddss2  35282  hdmap14lem2a  37337