MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssrexv Structured version   Unicode version

Theorem ssrexv 3408
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
StepHypRef Expression
1 ssel 3342 . . 3  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21anim1d 548 . 2  |-  ( A 
C_  B  ->  (
( x  e.  A  /\  ph )  ->  (
x  e.  B  /\  ph ) ) )
32reximdv2 2815 1  |-  ( A 
C_  B  ->  ( E. x  e.  A  ph 
->  E. x  e.  B  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   E.wrex 2706    C_ wss 3320
This theorem is referenced by:  iunss1  4104  onfr  4620  frxp  6456  moriotass  6579  frfi  7352  fisupcl  7472  brwdom3  7550  unwdomg  7552  tcrank  7808  hsmexlem2  8307  pwfseqlem3  8535  grur1  8695  suplem1pr  8929  fimaxre2  9956  lbzbi  10564  suprzub  10567  uzsupss  10568  zmin  10570  rexico  12157  rlim3  12292  rlimclim  12340  caurcvgr  12467  alzdvds  12899  bitsfzolem  12946  pclem  13212  0ram2  13389  0ramcl  13391  lsmless1x  15278  lsmless2x  15279  dprdss  15587  ablfac2  15647  subrgdvds  15882  ssrest  17240  fbun  17872  fgss  17905  isucn2  18309  metustOLD  18597  metust  18598  metutopOLD  18612  psmetutop  18613  lebnumlem3  18988  lebnum  18989  cfil3i  19222  cfilss  19223  fgcfil  19224  iscau4  19232  ivthle  19353  ivthle2  19354  lhop1lem  19897  lhop2  19899  ply1divex  20059  plyss  20118  dgrlem  20148  elqaa  20239  aannenlem2  20246  reeff1olem  20362  rlimcnp  20804  ftalem3  20857  pntlem3  21303  shless  22861  xlt2addrd  24124  ssnnssfz  24148  xreceu  24168  esumpcvgval  24468  sigaclci  24515  iccllyscon  24937  frmin  25517  nodenselem4  25639  axcontlem2  25904  volsupnfl  26251  locfincf  26386  fgmin  26399  cover2  26415  filbcmb  26442  istotbnd3  26480  sstotbnd  26484  heibor1lem  26518  isdrngo2  26574  isdrngo3  26575  pellfundre  26944  pellfundge  26945  pellfundglb  26948  hbtlem3  27308  hbtlem5  27309  itgoss  27345  frgrawopreg1  28439  frgrawopreg2  28440  islsati  29792  paddss1  30614  paddss2  30615  hdmap14lem2a  32668
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-rex 2711  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator