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

Theorem ssel 3327
Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
ssel

Proof of Theorem ssel
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 dfss2 3322 . . . . . 6
21biimpi 188 . . . . 5
3219.21bi 1797 . . . 4
43anim2d 552 . . 3
54eximdv 1667 . 2
6 df-clel 2418 . 2
7 df-clel 2418 . 2
85, 6, 73imtr4g 264 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 362  A.wal 1580  E.wex 1581  =wceq 1687  e.wcel 1749  C_wss 3305
This theorem is referenced by:  ssel2  3328  sseli  3329  sseld  3332  sstr2  3340  nelss  3392  ssralv  3393  ssrexv  3394  ralss  3395  rexss  3396  ssconb  3466  sscon  3467  ssdif  3468  unss1  3502  ssrin  3552  difin2  3589  reuss2  3607  reupick  3611  elpwunsn  3894  sssn  4006  uniss  4087  ss2iun  4161  ssiun  4187  iinss  4196  disjss2  4240  disjss1  4243  pwnss  4429  sspwb  4513  ssopab2b  4588  pwssun  4598  soss  4630  oneqmini  4741  sucssel  4782  onssneli  4799  onssnel2i  4800  frinxp  4875  ssrel  4899  ssrel2  4901  ssrelrel  4911  xpss12  4916  cnvss  4983  dmss  5010  elreldm  5035  dmcosseq  5072  relssres  5119  iss  5126  resopab2  5127  issref  5183  ssrnres  5248  dfco2a  5310  cores  5313  funssres  5430  fununi  5454  dfimafn  5710  funimass4  5712  funimass3  5789  dff3  5826  dff4  5827  funfvima2  5921  funfvima3  5922  f1elima  5944  isomin  5996  isofrlem  5999  riotass2  6048  ssoprab2b  6113  resoprab2  6157  ssorduni  6367  onint  6376  oninton  6381  ssnlim  6464  releldm2  6593  reldmtpos  6715  dmtpos  6719  onfununi  6761  tz7.48lem  6855  tz7.49  6859  omeulem1  6982  omeulem2  6983  omsmolem  7053  omsmo  7054  ss2ixp  7235  boxriin  7264  onomeneq  7459  unblem1  7523  unblem3  7525  fiint  7547  inf3lem2  7782  cantnflem2  7845  tcel  7912  tz9.13  7945  rankr1ag  7956  rankpwi  7977  rankelb  7978  bndrank  7995  cardlim  8089  carduni  8098  acni2  8163  dfac12r  8262  cfub  8365  cflim2  8379  fin1a2lem9  8524  axdc3lem2  8567  axdclem2  8636  gch2  8788  eltsk2g  8864  suplem1pr  9167  fimaxre  10223  lbreu  10226  lbinfm  10229  sup2  10232  sup3  10233  infm3  10235  infmrcl  10255  uzwo  10862  uzwoOLD  10863  eqreznegel  10885  negn0  10886  xrsupsslem  11214  xrinfmsslem  11215  supxrpnf  11226  supxrunb1  11227  supxrunb2  11228  iccsupr  11327  incexclem  13239  gcdcllem1  13635  lubel  15232  clatleglb  15236  mulgpropd  15597  sylow2a  16055  efgi2  16159  lspsnel6  16884  submabas  18087  elcls2  18382  isclo2  18396  cmpsublem  18706  cmpsub  18707  hauscmplem  18713  1stcelcls  18769  llyss  18787  nllyss  18788  txkgen  18929  nrmr0reg  19026  uffix  19198  ufinffr  19206  ufilen  19207  fmfnfmlem2  19232  alexsubALTlem2  19324  alexsubALT  19327  metrest  19799  iccntr  20098  reconnlem2  20104  caubl  20518  ulmss  21603  axcontlem4  22892  nbgranself2  23026  cusgrarn  23046  ocsh  24365  ococss  24375  shorth  24377  spansnss2  24657  h1datomi  24663  pjss2i  24762  pjssmii  24763  pjorthcoi  25252  pj3si  25290  ssrelf  25625  dfimafnf  25630  funimass4f  25631  1stpreima  25681  2ndpreima  25682  ordtconlem1  26063  indpi1  26187  cvmlift2lem1  26894  dfon2lem6  27303  trpredmintr  27397  orderseqlem  27415  wfrlem10  27435  frrlem5b  27475  frrlem5d  27477  nofv  27500  nocvxminlem  27533  nocvxmin  27534  limsucncmpi  27994  ismtyres  28378  ispridlc  28541  pw2f1ocnv  29059  ssrexf  29408  dfaimafn  29745  gsumlsscl  30512  lincfsuppcl  30531  linccl  30532  onfrALTlem3  30829  onfrALTlem2  30831  sspwtr  31133  sspwtrALT  31134  sspwtrALT2  31137  pwtrVD  31138  pwtrrVD  31139  suctrALT2VD  31150  suctrALT2  31151  onfrALTlem3VD  31201  onfrALTlem2VD  31203  bnj518  31457  paddss1  32898  paddss2  32899  lspindp5  34852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403
This theorem depends on definitions:  df-bi 179  df-an 364  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-clab 2409  df-cleq 2415  df-clel 2418  df-in 3312  df-ss 3319
  Copyright terms: Public domain W3C validator