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

Theorem ssrexv 3251
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 3187 . . 3  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21anim1d 547 . 2  |-  ( A 
C_  B  ->  (
( x  e.  A  /\  ph )  ->  (
x  e.  B  /\  ph ) ) )
32reximdv2 2665 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 1696   E.wrex 2557    C_ wss 3165
This theorem is referenced by:  iunss1  3932  onfr  4447  frxp  6241  moriotass  6350  frfi  7118  fisupcl  7234  brwdom3  7312  unwdomg  7314  tcrank  7570  hsmexlem2  8069  pwfseqlem3  8298  grur1  8458  suplem1pr  8692  fimaxre2  9718  lbzbi  10322  suprzub  10325  uzsupss  10326  zmin  10328  rexico  11853  rlim3  11988  rlimclim  12036  caurcvgr  12162  alzdvds  12594  bitsfzolem  12641  pclem  12907  0ram2  13084  0ramcl  13086  lsmless1x  14971  lsmless2x  14972  dprdss  15280  ablfac2  15340  subrgdvds  15575  ssrest  16923  fbun  17551  fgss  17584  lebnumlem3  18477  lebnum  18478  cfil3i  18711  cfilss  18712  fgcfil  18713  iscau4  18721  ivthle  18832  ivthle2  18833  lhop1lem  19376  lhop2  19378  ply1divex  19538  plyss  19597  dgrlem  19627  elqaa  19718  aannenlem2  19725  reeff1olem  19838  rlimcnp  20276  ftalem3  20328  pntlem3  20774  shless  21954  xreceu  23121  xlt2addrd  23268  ssnnssfz  23292  esumpcvgval  23461  sigaclci  23508  iccllyscon  23796  frmin  24313  nodenselem4  24409  axcontlem2  24665  basexre  25625  altretop  25703  locfincf  26409  fgmin  26422  cover2  26461  filbcmb  26535  istotbnd3  26598  sstotbnd  26602  heibor1lem  26636  isdrngo2  26692  isdrngo3  26693  pellfundre  27069  pellfundge  27070  pellfundglb  27073  hbtlem3  27434  hbtlem5  27435  itgoss  27471  islsati  29806  paddss1  30628  paddss2  30629  hdmap14lem2a  32682
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-rex 2562  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator