Theorem ssrexv 3480

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

Syntax hints:   -> wi 4   e. wcel 1904   E.wrex 2757   C_ wss 3390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-rex 2762  df-in 3397  df-ss 3404

This theorem is referenced by:  iunss1  4281  onfr  5469  moriotass  6298  frxp  6925  frfi  7834  fisupcl  8003  supgtoreq  8004  brwdom3  8115  unwdomg  8117  tcrank  8373  hsmexlem2  8875  pwfseqlem3  9103  grur1  9263  suplem1pr  9495  fimaxre2  10574  suprfinzcl  11073  lbzbi  11275  suprzub  11278  uzsupss  11279  zmin  11283  ssnn0fi  12235  elss2prb  12684  scshwfzeqfzo  12982  rexico  13493  rlim3  13639  rlimclim  13687  caurcvgr  13815  caurcvgrOLD  13816  alzdvds  14432  bitsfzolem  14486  bitsfzolemOLD  14487  pclem  14867  0ram2  15058  0ramcl  15060  symgextfo  17141  lsmless1x  17374  lsmless2x  17375  dprdss  17740  ablfac2  17800  subrgdvds  18100  ssrest  20269  locfincf  20623  fbun  20933  fgss  20966  isucn2  21372  metust  21651  psmetutop  21660  lebnumlem3  22069  lebnumlem3OLD  22072  lebnum  22073  cfil3i  22317  cfilss  22318  fgcfil  22319  iscau4  22327  ivthle  22485  ivthle2  22486  lhop1lem  23044  lhop2  23046  ply1divex  23166  plyss  23232  dgrlem  23262  elqaa  23357  aannenlem2  23364  reeff1olem  23480  rlimcnp  23970  ftalem3  24078  pntlem3  24526  tgisline  24751  axcontlem2  25074  frgrawopreg1  25857  frgrawopreg2  25858  shless  27093  xlt2addrd  28413  ssnnssfz  28442  xreceu  28466  archirngz  28580  archiabllem1b  28583  locfinreflem  28741  crefss  28750  esumpcvgval  28973  sigaclci  29028  eulerpartlemgvv  29282  eulerpartlemgh  29284  signsply0  29512  iccllyscon  30045  frmin  30551  nodenselem4  30644  fgmin  31097  poimirlem26  32030  poimirlem30  32034  volsupnfl  32049  cover2  32104  filbcmb  32131  istotbnd3  32167  sstotbnd  32171  heibor1lem  32205  isdrngo2  32261  isdrngo3  32262  islsati  32631  paddss1  33453  paddss2  33454  hdmap14lem2a  35509  pellfundre  35800  pellfundge  35801  pellfundglb  35804  hbtlem3  36057  hbtlem5  36058  itgoss  36100  radcnvrat  36733  fourierdlem20  38101  iccelpart  38892  ssn0rex  39136  ssnn0ssfz  40638  pgrpgt2nabl  40659