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

Theorem ssel 3302
Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
ssel  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )

Proof of Theorem ssel
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 dfss2 3297 . . . . . 6  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
21biimpi 187 . . . . 5  |-  ( A 
C_  B  ->  A. x
( x  e.  A  ->  x  e.  B ) )
3219.21bi 1770 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
43anim2d 549 . . 3  |-  ( A 
C_  B  ->  (
( x  =  C  /\  x  e.  A
)  ->  ( x  =  C  /\  x  e.  B ) ) )
54eximdv 1629 . 2  |-  ( A 
C_  B  ->  ( E. x ( x  =  C  /\  x  e.  A )  ->  E. x
( x  =  C  /\  x  e.  B
) ) )
6 df-clel 2400 . 2  |-  ( C  e.  A  <->  E. x
( x  =  C  /\  x  e.  A
) )
7 df-clel 2400 . 2  |-  ( C  e.  B  <->  E. x
( x  =  C  /\  x  e.  B
) )
85, 6, 73imtr4g 262 1  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   A.wal 1546   E.wex 1547    = wceq 1649    e. wcel 1721    C_ wss 3280
This theorem is referenced by:  ssel2  3303  sseli  3304  sseld  3307  sstr2  3315  ssralv  3367  ssrexv  3368  ralss  3369  rexss  3370  ssconb  3440  sscon  3441  ssdif  3442  unss1  3476  ssrin  3526  difin2  3563  reuss2  3581  reupick  3585  sssn  3917  uniss  3996  ss2iun  4068  ssiun  4093  iinss  4102  disjss2  4145  disjss1  4148  pwnss  4325  sspwb  4373  ssopab2b  4441  pwssun  4449  soss  4481  oneqmini  4592  sucssel  4633  onssneli  4650  onssnel2i  4651  elpwunsn  4716  ssorduni  4725  onint  4734  oninton  4739  ssnlim  4822  frinxp  4902  ssrel  4923  ssrel2  4925  ssrelrel  4935  xpss12  4940  cnvss  5004  dmss  5028  elreldm  5053  dmcosseq  5096  relssres  5142  iss  5148  resopab2  5149  issref  5206  ssrnres  5268  dfco2a  5329  cores  5332  funssres  5452  fununi  5476  dfimafn  5734  funimass4  5736  funimass3  5805  dff3  5841  dff4  5842  funfvima2  5933  funfvima3  5934  f1elima  5968  isomin  6016  isofrlem  6019  ssoprab2b  6090  resoprab2  6126  releldm2  6356  reldmtpos  6446  dmtpos  6450  riotass2  6536  onfununi  6562  tz7.48lem  6657  tz7.49  6661  omeulem1  6784  omeulem2  6785  omsmolem  6855  omsmo  6856  ss2ixp  7034  boxriin  7063  onomeneq  7255  unblem1  7318  unblem3  7320  fiint  7342  inf3lem2  7540  cantnflem2  7602  tcel  7640  tz9.13  7673  rankr1ag  7684  rankpwi  7705  rankelb  7706  bndrank  7723  cardlim  7815  carduni  7824  acni2  7883  dfac12r  7982  cfub  8085  cflim2  8099  fin1a2lem9  8244  axdc3lem2  8287  axdclem2  8356  gch2  8510  eltsk2g  8582  suplem1pr  8885  fimaxre  9911  lbreu  9914  lbinfm  9917  sup2  9920  sup3  9921  infm3  9923  infmrcl  9943  uzwo  10495  uzwoOLD  10496  eqreznegel  10517  negn0  10518  xrsupsslem  10841  xrinfmsslem  10842  supxrpnf  10853  supxrunb1  10854  supxrunb2  10855  iccsupr  10953  incexclem  12571  gcdcllem1  12966  lubel  14504  clatleglb  14508  mulgpropd  14878  sylow2a  15208  efgi2  15312  lspsnel6  16025  elcls2  17093  isclo2  17107  cmpsublem  17416  cmpsub  17417  hauscmplem  17423  1stcelcls  17477  llyss  17495  nllyss  17496  txkgen  17637  nrmr0reg  17734  uffix  17906  ufinffr  17914  ufilen  17915  fmfnfmlem2  17940  alexsubALTlem2  18032  alexsubALT  18035  metrest  18507  iccntr  18805  reconnlem2  18811  caubl  19213  ulmss  20266  nbgranself2  21401  cusgrarn  21421  ocsh  22738  ococss  22748  shorth  22750  spansnss2  23030  h1datomi  23036  pjss2i  23135  pjssmii  23136  pjorthcoi  23625  pj3si  23663  dfimafnf  23996  funimass4f  23997  1stpreima  24048  2ndpreima  24049  indpi1  24372  cvmlift2lem1  24942  dfon2lem6  25358  trpredmintr  25448  orderseqlem  25466  wfrlem10  25479  frrlem5b  25500  frrlem5d  25502  nofv  25525  nocvxminlem  25558  nocvxmin  25559  axcontlem4  25810  limsucncmpi  26099  ismtyres  26407  ispridlc  26570  nelss  26622  pw2f1ocnv  26998  ssrexf  27551  dfaimafn  27896  swrdccatin2  28018  onfrALTlem3  28341  onfrALTlem2  28343  sspwtr  28643  sspwtrALT  28644  sspwtrALT2  28645  pwtrVD  28646  pwtrrVD  28647  suctrALT2VD  28657  suctrALT2  28658  onfrALTlem3VD  28708  onfrALTlem2VD  28710  bnj518  28963  paddss1  30299  paddss2  30300  lspindp5  32253
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator