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

Theorem ssrexv 3238
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 3174 . . 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 2652 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 1684   E.wrex 2544    C_ wss 3152
This theorem is referenced by:  iunss1  3916  onfr  4431  frxp  6225  moriotass  6334  frfi  7102  fisupcl  7218  brwdom3  7296  unwdomg  7298  tcrank  7554  hsmexlem2  8053  pwfseqlem3  8282  grur1  8442  suplem1pr  8676  fimaxre2  9702  lbzbi  10306  suprzub  10309  uzsupss  10310  zmin  10312  rexico  11837  rlim3  11972  rlimclim  12020  caurcvgr  12146  alzdvds  12578  bitsfzolem  12625  pclem  12891  0ram2  13068  0ramcl  13070  lsmless1x  14955  lsmless2x  14956  dprdss  15264  ablfac2  15324  subrgdvds  15559  ssrest  16907  fbun  17535  fgss  17568  lebnumlem3  18461  lebnum  18462  cfil3i  18695  cfilss  18696  fgcfil  18697  iscau4  18705  ivthle  18816  ivthle2  18817  lhop1lem  19360  lhop2  19362  ply1divex  19522  plyss  19581  dgrlem  19611  elqaa  19702  aannenlem2  19709  reeff1olem  19822  rlimcnp  20260  ftalem3  20312  pntlem3  20758  shless  21938  xreceu  23105  xlt2addrd  23253  ssnnssfz  23277  esumpcvgval  23446  sigaclci  23493  iccllyscon  23781  frmin  24242  nodenselem4  24338  axcontlem2  24593  basexre  25522  altretop  25600  locfincf  26306  fgmin  26319  cover2  26358  filbcmb  26432  istotbnd3  26495  sstotbnd  26499  heibor1lem  26533  isdrngo2  26589  isdrngo3  26590  pellfundre  26966  pellfundge  26967  pellfundglb  26970  hbtlem3  27331  hbtlem5  27332  itgoss  27368  islsati  29184  paddss1  30006  paddss2  30007  hdmap14lem2a  32060
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-rex 2549  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator