Theorem ssrexv 3565

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

Syntax hints:   -> wi 4   e. wcel 1767   E.wrex 2815   C_ wss 3476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-rex 2820  df-in 3483  df-ss 3490

This theorem is referenced by:  iunss1  4337  onfr  4917  moriotass  6272  frxp  6890  frfi  7761  fisupcl  7923  supgtoreq  7924  brwdom3  8004  unwdomg  8006  tcrank  8298  hsmexlem2  8803  pwfseqlem3  9034  grur1  9194  suplem1pr  9426  fimaxre2  10487  suprfinzcl  10971  lbzbi  11166  suprzub  11169  uzsupss  11170  zmin  11174  ssnn0fi  12058  scshwfzeqfzo  12753  rexico  13145  rlim3  13280  rlimclim  13328  caurcvgr  13455  alzdvds  13891  bitsfzolem  13939  pclem  14217  0ram2  14394  0ramcl  14396  symgextfo  16242  lsmless1x  16460  lsmless2x  16461  dprdss  16866  ablfac2  16930  subrgdvds  17226  ssrest  19443  fbun  20076  fgss  20109  isucn2  20517  metustOLD  20805  metust  20806  metutopOLD  20820  psmetutop  20821  lebnumlem3  21198  lebnum  21199  cfil3i  21443  cfilss  21444  fgcfil  21445  iscau4  21453  ivthle  21603  ivthle2  21604  lhop1lem  22149  lhop2  22151  ply1divex  22272  plyss  22331  dgrlem  22361  elqaa  22452  aannenlem2  22459  reeff1olem  22575  rlimcnp  23023  ftalem3  23076  pntlem3  23522  tgisline  23721  axcontlem2  23944  frgrawopreg1  24727  frgrawopreg2  24728  shless  25953  xlt2addrd  27246  ssnnssfz  27265  xreceu  27286  archirngz  27395  archiabllem1b  27398  esumpcvgval  27724  sigaclci  27772  eulerpartlemgvv  27955  eulerpartlemgh  27957  signsply0  28148  iccllyscon  28335  frmin  28899  nodenselem4  29021  volsupnfl  29636  locfincf  29778  fgmin  29791  cover2  29807  filbcmb  29834  istotbnd3  29870  sstotbnd  29874  heibor1lem  29908  isdrngo2  29964  isdrngo3  29965  pellfundre  30421  pellfundge  30422  pellfundglb  30425  hbtlem3  30680  hbtlem5  30681  itgoss  30717  fourierdlem20  31427  ssnn0ssfz  32002  pgrpgt2nabl  32024  islsati  33791  paddss1  34613  paddss2  34614  hdmap14lem2a  36667