Theorem ssrexv 3496

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

Syntax hints:   -> wi 4   e. wcel 1889   E.wrex 2740   C_ wss 3406

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-rex 2745  df-in 3413  df-ss 3420

This theorem is referenced by:  iunss1  4293  onfr  5465  moriotass  6285  frxp  6911  frfi  7821  fisupcl  7990  supgtoreq  7991  brwdom3  8102  unwdomg  8104  tcrank  8360  hsmexlem2  8862  pwfseqlem3  9090  grur1  9250  suplem1pr  9482  fimaxre2  10559  suprfinzcl  11057  lbzbi  11259  suprzub  11262  uzsupss  11263  zmin  11267  ssnn0fi  12204  elss2prb  12650  scshwfzeqfzo  12932  rexico  13428  rlim3  13574  rlimclim  13622  caurcvgr  13750  caurcvgrOLD  13751  alzdvds  14367  bitsfzolem  14419  bitsfzolemOLD  14420  pclem  14800  0ram2  14991  0ramcl  14993  symgextfo  17075  lsmless1x  17308  lsmless2x  17309  dprdss  17674  ablfac2  17734  subrgdvds  18034  ssrest  20204  locfincf  20558  fbun  20867  fgss  20900  isucn2  21306  metust  21585  psmetutop  21594  lebnumlem3  22003  lebnumlem3OLD  22006  lebnum  22007  cfil3i  22251  cfilss  22252  fgcfil  22253  iscau4  22261  ivthle  22419  ivthle2  22420  lhop1lem  22977  lhop2  22979  ply1divex  23099  plyss  23165  dgrlem  23195  elqaa  23290  aannenlem2  23297  reeff1olem  23413  rlimcnp  23903  ftalem3  24011  pntlem3  24459  tgisline  24684  axcontlem2  25007  frgrawopreg1  25790  frgrawopreg2  25791  shless  27024  xlt2addrd  28350  ssnnssfz  28379  xreceu  28403  archirngz  28518  archiabllem1b  28521  locfinreflem  28679  crefss  28688  esumpcvgval  28911  sigaclci  28966  eulerpartlemgvv  29221  eulerpartlemgh  29223  signsply0  29452  iccllyscon  29985  frmin  30492  nodenselem4  30585  fgmin  31038  poimirlem26  31978  poimirlem30  31982  volsupnfl  31997  cover2  32052  filbcmb  32079  istotbnd3  32115  sstotbnd  32119  heibor1lem  32153  isdrngo2  32209  isdrngo3  32210  islsati  32572  paddss1  33394  paddss2  33395  hdmap14lem2a  35450  pellfundre  35741  pellfundge  35742  pellfundglb  35745  hbtlem3  35998  hbtlem5  35999  itgoss  36041  radcnvrat  36674  fourierdlem20  37999  iccelpart  38757  ssn0rex  38999  ssnn0ssfz  40234  pgrpgt2nabl  40255