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

Theorem ssel 3187
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 3182 . . . . . 6  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
21biimpi 186 . . . . 5  |-  ( A 
C_  B  ->  A. x
( x  e.  A  ->  x  e.  B ) )
3219.21bi 1806 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
43anim2d 548 . . 3  |-  ( A 
C_  B  ->  (
( x  =  C  /\  x  e.  A
)  ->  ( x  =  C  /\  x  e.  B ) ) )
54eximdv 1612 . 2  |-  ( A 
C_  B  ->  ( E. x ( x  =  C  /\  x  e.  A )  ->  E. x
( x  =  C  /\  x  e.  B
) ) )
6 df-clel 2292 . 2  |-  ( C  e.  A  <->  E. x
( x  =  C  /\  x  e.  A
) )
7 df-clel 2292 . 2  |-  ( C  e.  B  <->  E. x
( x  =  C  /\  x  e.  B
) )
85, 6, 73imtr4g 261 1  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   A.wal 1530   E.wex 1531    = wceq 1632    e. wcel 1696    C_ wss 3165
This theorem is referenced by:  ssel2  3188  sseli  3189  sseld  3192  sstr2  3199  ssralv  3250  ssrexv  3251  ralss  3252  rexss  3253  ssconb  3322  sscon  3323  ssdif  3324  unss1  3357  ssrin  3407  difin2  3443  reuss2  3461  reupick  3465  sssn  3788  uniss  3864  ss2iun  3936  ssiun  3960  iinss  3969  disjss2  4012  disjss1  4015  pwnss  4192  sspwb  4239  ssopab2b  4307  pwssun  4315  soss  4348  oneqmini  4459  sucssel  4501  onssneli  4518  onssnel2i  4519  elpwunsn  4584  ssorduni  4593  onint  4602  oninton  4607  ssnlim  4690  frinxp  4771  ssrel  4792  ssrelrel  4803  xpss12  4808  cnvss  4870  dmss  4894  elreldm  4919  dmcosseq  4962  relssres  5008  iss  5014  resopab2  5015  issref  5072  ssrnres  5132  dfco2a  5189  cores  5192  funssres  5310  fununi  5332  dfimafn  5587  funimass4  5589  funimass3  5657  dff3  5689  dff4  5690  funfvima2  5770  funfvima3  5771  f1elima  5803  isomin  5850  isofrlem  5853  ssoprab2b  5921  resoprab2  5957  releldm2  6186  reldmtpos  6258  dmtpos  6262  riotass2  6348  onfununi  6374  tz7.48lem  6469  tz7.49  6473  omeulem1  6596  omeulem2  6597  omsmolem  6667  omsmo  6668  ss2ixp  6845  boxriin  6874  onomeneq  7066  unblem1  7125  unblem3  7127  fiint  7149  inf3lem2  7346  cantnflem2  7408  tcel  7446  tz9.13  7479  rankr1ag  7490  rankpwi  7511  rankelb  7512  bndrank  7529  cardlim  7621  carduni  7630  acni2  7689  dfac12r  7788  cfub  7891  cflim2  7905  fin1a2lem9  8050  axdc3lem2  8093  axdclem2  8163  gch2  8317  eltsk2g  8389  suplem1pr  8692  fimaxre  9717  lbreu  9720  lbinfm  9723  sup2  9726  sup3  9727  infm3  9729  infmrcl  9749  uzwo  10297  uzwoOLD  10298  eqreznegel  10319  negn0  10320  xrsupsslem  10641  xrinfmsslem  10642  supxrpnf  10653  supxrunb1  10654  supxrunb2  10655  iccsupr  10752  hashbclem  11406  incexclem  12311  gcdcllem1  12706  lubel  14242  clatleglb  14246  mulgpropd  14616  sylow2a  14946  efgi2  15050  lspsnel6  15767  elcls2  16827  isclo2  16841  cmpsublem  17142  cmpsub  17143  hauscmplem  17149  1stcelcls  17203  llyss  17221  nllyss  17222  txkgen  17362  nrmr0reg  17456  uffix  17632  ufinffr  17640  ufilen  17641  fmfnfmlem2  17666  alexsubALTlem2  17758  alexsubALT  17761  metrest  18086  iccntr  18342  reconnlem2  18348  caubl  18749  ulmss  19790  ocsh  21878  ococss  21888  shorth  21890  spansnss2  22170  h1datomi  22176  pjss2i  22275  pjssmii  22276  pjorthcoi  22765  pj3si  22803  dfimafnf  23057  funimass4f  23058  indpi1  23620  cvmlift2lem1  23848  dfon2lem6  24215  trpredmintr  24305  orderseqlem  24323  wfrlem10  24336  frrlem5b  24357  frrlem5d  24359  nofv  24382  nocvxminlem  24415  nocvxmin  24416  axcontlem4  24667  limsucncmpi  24956  imgfldref2  25167  prj1b  25182  prj3  25183  eqfnung2  25221  intfmu2  25622  supexr  25734  fnctartar  26010  fnctartar2  26011  lemindclsbu  26098  isconcl6a  26206  ismtyres  26635  ispridlc  26798  nelss  26854  pw2f1ocnv  27233  ssrexf  27787  fnvinran  27788  stoweidlem41  27893  stoweidlem44  27896  stoweidlem48  27900  stoweidlem51  27903  stoweidlem52  27904  stoweidlem53  27905  stoweidlem57  27909  stoweidlem59  27911  dfaimafn  28133  nbgranself2  28285  onfrALTlem3  28608  onfrALTlem2  28610  sspwtr  28911  sspwtrALT  28912  sspwtrALT2  28913  pwtrVD  28914  pwtrOLD  28915  pwtrrVD  28916  pwtrrOLD  28917  suctrALT2VD  28928  suctrALT2  28929  onfrALTlem3VD  28979  onfrALTlem2VD  28981  bnj518  29234  paddss1  30628  paddss2  30629  lspindp5  32582
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-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator