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

Theorem ssel 3334
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 3329 . . . . . 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 1774 . . . 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 1632 . 2  |-  ( A 
C_  B  ->  ( E. x ( x  =  C  /\  x  e.  A )  ->  E. x
( x  =  C  /\  x  e.  B
) ) )
6 df-clel 2431 . 2  |-  ( C  e.  A  <->  E. x
( x  =  C  /\  x  e.  A
) )
7 df-clel 2431 . 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 1549   E.wex 1550    = wceq 1652    e. wcel 1725    C_ wss 3312
This theorem is referenced by:  ssel2  3335  sseli  3336  sseld  3339  sstr2  3347  ssralv  3399  ssrexv  3400  ralss  3401  rexss  3402  ssconb  3472  sscon  3473  ssdif  3474  unss1  3508  ssrin  3558  difin2  3595  reuss2  3613  reupick  3617  sssn  3949  uniss  4028  ss2iun  4100  ssiun  4125  iinss  4134  disjss2  4177  disjss1  4180  pwnss  4357  sspwb  4405  ssopab2b  4473  pwssun  4481  soss  4513  oneqmini  4624  sucssel  4665  onssneli  4682  onssnel2i  4683  elpwunsn  4748  ssorduni  4757  onint  4766  oninton  4771  ssnlim  4854  frinxp  4934  ssrel  4955  ssrel2  4957  ssrelrel  4967  xpss12  4972  cnvss  5036  dmss  5060  elreldm  5085  dmcosseq  5128  relssres  5174  iss  5180  resopab2  5181  issref  5238  ssrnres  5300  dfco2a  5361  cores  5364  funssres  5484  fununi  5508  dfimafn  5766  funimass4  5768  funimass3  5837  dff3  5873  dff4  5874  funfvima2  5965  funfvima3  5966  f1elima  6000  isomin  6048  isofrlem  6051  ssoprab2b  6122  resoprab2  6158  releldm2  6388  reldmtpos  6478  dmtpos  6482  riotass2  6568  onfununi  6594  tz7.48lem  6689  tz7.49  6693  omeulem1  6816  omeulem2  6817  omsmolem  6887  omsmo  6888  ss2ixp  7066  boxriin  7095  onomeneq  7287  unblem1  7350  unblem3  7352  fiint  7374  inf3lem2  7573  cantnflem2  7635  tcel  7673  tz9.13  7706  rankr1ag  7717  rankpwi  7738  rankelb  7739  bndrank  7756  cardlim  7848  carduni  7857  acni2  7916  dfac12r  8015  cfub  8118  cflim2  8132  fin1a2lem9  8277  axdc3lem2  8320  axdclem2  8389  gch2  8543  eltsk2g  8615  suplem1pr  8918  fimaxre  9944  lbreu  9947  lbinfm  9950  sup2  9953  sup3  9954  infm3  9956  infmrcl  9976  uzwo  10528  uzwoOLD  10529  eqreznegel  10550  negn0  10551  xrsupsslem  10874  xrinfmsslem  10875  supxrpnf  10886  supxrunb1  10887  supxrunb2  10888  iccsupr  10986  incexclem  12604  gcdcllem1  12999  lubel  14537  clatleglb  14541  mulgpropd  14911  sylow2a  15241  efgi2  15345  lspsnel6  16058  elcls2  17126  isclo2  17140  cmpsublem  17450  cmpsub  17451  hauscmplem  17457  1stcelcls  17512  llyss  17530  nllyss  17531  txkgen  17672  nrmr0reg  17769  uffix  17941  ufinffr  17949  ufilen  17950  fmfnfmlem2  17975  alexsubALTlem2  18067  alexsubALT  18070  metrest  18542  iccntr  18840  reconnlem2  18846  caubl  19248  ulmss  20301  nbgranself2  21436  cusgrarn  21456  ocsh  22773  ococss  22783  shorth  22785  spansnss2  23065  h1datomi  23071  pjss2i  23170  pjssmii  23171  pjorthcoi  23660  pj3si  23698  dfimafnf  24031  funimass4f  24032  1stpreima  24083  2ndpreima  24084  indpi1  24407  cvmlift2lem1  24977  dfon2lem6  25399  trpredmintr  25489  orderseqlem  25507  wfrlem10  25520  frrlem5b  25541  frrlem5d  25543  nofv  25566  nocvxminlem  25599  nocvxmin  25600  axcontlem4  25854  limsucncmpi  26143  ismtyres  26454  ispridlc  26617  nelss  26669  pw2f1ocnv  27045  ssrexf  27598  dfaimafn  27943  swrdccatin2  28093  onfrALTlem3  28485  onfrALTlem2  28487  sspwtr  28788  sspwtrALT  28789  sspwtrALT2  28790  pwtrVD  28791  pwtrrVD  28792  suctrALT2VD  28802  suctrALT2  28803  onfrALTlem3VD  28853  onfrALTlem2VD  28855  bnj518  29111  paddss1  30453  paddss2  30454  lspindp5  32407
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 2416
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 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator