Theorem ssrexv 3527

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

Syntax hints:   -> wi 4   e. wcel 1869   E.wrex 2777   C_ wss 3437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-rex 2782  df-in 3444  df-ss 3451

This theorem is referenced by:  iunss1  4309  onfr  5479  moriotass  6293  frxp  6915  frfi  7820  fisupcl  7989  supgtoreq  7990  brwdom3  8101  unwdomg  8103  tcrank  8358  hsmexlem2  8859  pwfseqlem3  9087  grur1  9247  suplem1pr  9479  fimaxre2  10554  suprfinzcl  11052  lbzbi  11254  suprzub  11257  uzsupss  11258  zmin  11262  ssnn0fi  12198  scshwfzeqfzo  12921  rexico  13410  rlim3  13555  rlimclim  13603  caurcvgr  13731  caurcvgrOLD  13732  alzdvds  14348  bitsfzolem  14400  bitsfzolemOLD  14401  pclem  14781  0ram2  14972  0ramcl  14974  symgextfo  17056  lsmless1x  17289  lsmless2x  17290  dprdss  17655  ablfac2  17715  subrgdvds  18015  ssrest  20184  locfincf  20538  fbun  20847  fgss  20880  isucn2  21286  metust  21565  psmetutop  21574  lebnumlem3  21983  lebnumlem3OLD  21986  lebnum  21987  cfil3i  22231  cfilss  22232  fgcfil  22233  iscau4  22241  ivthle  22399  ivthle2  22400  lhop1lem  22957  lhop2  22959  ply1divex  23079  plyss  23145  dgrlem  23175  elqaa  23270  aannenlem2  23277  reeff1olem  23393  rlimcnp  23883  ftalem3  23991  pntlem3  24439  tgisline  24664  axcontlem2  24987  frgrawopreg1  25770  frgrawopreg2  25771  shless  27004  xlt2addrd  28338  ssnnssfz  28367  xreceu  28392  archirngz  28507  archiabllem1b  28510  locfinreflem  28669  crefss  28678  esumpcvgval  28901  sigaclci  28956  eulerpartlemgvv  29211  eulerpartlemgh  29213  signsply0  29442  iccllyscon  29975  frmin  30481  nodenselem4  30572  fgmin  31025  poimirlem26  31924  poimirlem30  31928  volsupnfl  31943  cover2  31998  filbcmb  32025  istotbnd3  32061  sstotbnd  32065  heibor1lem  32099  isdrngo2  32155  isdrngo3  32156  islsati  32523  paddss1  33345  paddss2  33346  hdmap14lem2a  35401  pellfundre  35693  pellfundge  35694  pellfundglb  35697  hbtlem3  35950  hbtlem5  35951  itgoss  35993  radcnvrat  36565  fourierdlem20  37853  iccelpart  38503  ssnn0ssfz  39474  pgrpgt2nabl  39495