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

Theorem ssel 3344
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 3339 . . . . . 6  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
21biimpi 188 . . . . 5  |-  ( A 
C_  B  ->  A. x
( x  e.  A  ->  x  e.  B ) )
3219.21bi 1775 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
43anim2d 550 . . 3  |-  ( A 
C_  B  ->  (
( x  =  C  /\  x  e.  A
)  ->  ( x  =  C  /\  x  e.  B ) ) )
54eximdv 1633 . 2  |-  ( A 
C_  B  ->  ( E. x ( x  =  C  /\  x  e.  A )  ->  E. x
( x  =  C  /\  x  e.  B
) ) )
6 df-clel 2434 . 2  |-  ( C  e.  A  <->  E. x
( x  =  C  /\  x  e.  A
) )
7 df-clel 2434 . 2  |-  ( C  e.  B  <->  E. x
( x  =  C  /\  x  e.  B
) )
85, 6, 73imtr4g 263 1  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360   A.wal 1550   E.wex 1551    = wceq 1653    e. wcel 1726    C_ wss 3322
This theorem is referenced by:  ssel2  3345  sseli  3346  sseld  3349  sstr2  3357  ssralv  3409  ssrexv  3410  ralss  3411  rexss  3412  ssconb  3482  sscon  3483  ssdif  3484  unss1  3518  ssrin  3568  difin2  3605  reuss2  3623  reupick  3627  sssn  3959  uniss  4038  ss2iun  4110  ssiun  4135  iinss  4144  disjss2  4188  disjss1  4191  pwnss  4368  sspwb  4416  ssopab2b  4484  pwssun  4492  soss  4524  oneqmini  4635  sucssel  4677  onssneli  4694  onssnel2i  4695  elpwunsn  4760  ssorduni  4769  onint  4778  oninton  4783  ssnlim  4866  frinxp  4946  ssrel  4967  ssrel2  4969  ssrelrel  4979  xpss12  4984  cnvss  5048  dmss  5072  elreldm  5097  dmcosseq  5140  relssres  5186  iss  5192  resopab2  5193  issref  5250  ssrnres  5312  dfco2a  5373  cores  5376  funssres  5496  fununi  5520  dfimafn  5778  funimass4  5780  funimass3  5849  dff3  5885  dff4  5886  funfvima2  5977  funfvima3  5978  f1elima  6012  isomin  6060  isofrlem  6063  ssoprab2b  6134  resoprab2  6170  releldm2  6400  reldmtpos  6490  dmtpos  6494  riotass2  6580  onfununi  6606  tz7.48lem  6701  tz7.49  6705  omeulem1  6828  omeulem2  6829  omsmolem  6899  omsmo  6900  ss2ixp  7078  boxriin  7107  onomeneq  7299  unblem1  7362  unblem3  7364  fiint  7386  inf3lem2  7587  cantnflem2  7649  tcel  7687  tz9.13  7720  rankr1ag  7731  rankpwi  7752  rankelb  7753  bndrank  7770  cardlim  7864  carduni  7873  acni2  7932  dfac12r  8031  cfub  8134  cflim2  8148  fin1a2lem9  8293  axdc3lem2  8336  axdclem2  8405  gch2  8555  eltsk2g  8631  suplem1pr  8934  fimaxre  9960  lbreu  9963  lbinfm  9966  sup2  9969  sup3  9970  infm3  9972  infmrcl  9992  uzwo  10544  uzwoOLD  10545  eqreznegel  10566  negn0  10567  xrsupsslem  10890  xrinfmsslem  10891  supxrpnf  10902  supxrunb1  10903  supxrunb2  10904  iccsupr  11002  incexclem  12621  gcdcllem1  13016  lubel  14554  clatleglb  14558  mulgpropd  14928  sylow2a  15258  efgi2  15362  lspsnel6  16075  elcls2  17143  isclo2  17157  cmpsublem  17467  cmpsub  17468  hauscmplem  17474  1stcelcls  17529  llyss  17547  nllyss  17548  txkgen  17689  nrmr0reg  17786  uffix  17958  ufinffr  17966  ufilen  17967  fmfnfmlem2  17992  alexsubALTlem2  18084  alexsubALT  18087  metrest  18559  iccntr  18857  reconnlem2  18863  caubl  19265  ulmss  20318  nbgranself2  21453  cusgrarn  21473  ocsh  22790  ococss  22800  shorth  22802  spansnss2  23082  h1datomi  23088  pjss2i  23187  pjssmii  23188  pjorthcoi  23677  pj3si  23715  dfimafnf  24048  funimass4f  24049  1stpreima  24100  2ndpreima  24101  indpi1  24424  cvmlift2lem1  24994  dfon2lem6  25420  trpredmintr  25514  orderseqlem  25532  wfrlem10  25552  frrlem5b  25592  frrlem5d  25594  nofv  25617  nocvxminlem  25650  nocvxmin  25651  axcontlem4  25911  limsucncmpi  26200  ismtyres  26531  ispridlc  26694  nelss  26746  pw2f1ocnv  27122  ssrexf  27674  dfaimafn  28019  onfrALTlem3  28704  onfrALTlem2  28706  sspwtr  29008  sspwtrALT  29009  sspwtrALT2  29010  pwtrVD  29011  pwtrrVD  29012  suctrALT2VD  29022  suctrALT2  29023  onfrALTlem3VD  29073  onfrALTlem2VD  29075  bnj518  29331  paddss1  30688  paddss2  30689  lspindp5  32642
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator