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

Theorem ssel 3497
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 3492 . . . . . 6
21biimpi 194 . . . . 5
3219.21bi 1869 . . . 4
43anim2d 565 . . 3
54eximdv 1710 . 2
6 df-clel 2452 . 2
7 df-clel 2452 . 2
85, 6, 73imtr4g 270 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  A.wal 1393  =wceq 1395  E.wex 1612  e.wcel 1818  C_wss 3475
This theorem is referenced by:  ssel2  3498  sseli  3499  sseld  3502  sstr2  3510  nelss  3562  ssralv  3563  ssrexv  3564  ralss  3565  rexss  3566  ssconb  3636  sscon  3637  ssdif  3638  unss1  3672  ssrin  3722  difin2  3759  reuss2  3777  reupick  3781  elpwunsn  4070  sssn  4188  uniss  4270  ss2iun  4346  ssiun  4372  iinss  4381  disjss2  4425  disjss1  4428  pwnss  4617  sspwb  4701  ssopab2b  4779  pwssun  4791  soss  4823  oneqmini  4934  sucssel  4975  onssneli  4992  onssnel2i  4993  frinxp  5070  ssrel  5096  ssrel2  5098  ssrelrel  5108  xpss12  5113  cnvss  5180  dmss  5207  elreldm  5232  dmcosseq  5269  relssres  5316  iss  5326  resopab2  5327  issref  5385  ssrnres  5450  dfco2a  5512  cores  5515  funssres  5633  fununi  5659  dfimafn  5922  funimass4  5924  funimass3  6003  dff3  6044  dff4  6045  funfvima2  6148  funfvima3  6149  f1elima  6171  isomin  6233  isofrlem  6236  riotass2  6284  ssoprab2b  6354  resoprab2  6399  ssorduni  6621  onint  6630  oninton  6635  ssnlim  6718  releldm2  6850  reldmtpos  6982  dmtpos  6986  onfununi  7031  tz7.48lem  7125  tz7.49  7129  omeulem1  7250  omeulem2  7251  omsmolem  7321  omsmo  7322  ss2ixp  7502  boxriin  7531  onomeneq  7727  unblem1  7792  unblem3  7794  fiint  7817  inf3lem2  8067  cantnflem2  8130  tcel  8197  tz9.13  8230  rankr1ag  8241  rankpwi  8262  rankelb  8263  bndrank  8280  cardlim  8374  carduni  8383  acni2  8448  dfac12r  8547  cfub  8650  cflim2  8664  fin1a2lem9  8809  axdc3lem2  8852  axdclem2  8921  gch2  9074  eltsk2g  9150  suplem1pr  9451  fimaxre  10515  lbreu  10518  lbinfm  10521  sup2  10524  sup3  10525  infm3  10527  infmrcl  10547  uzwo  11173  uzwoOLD  11174  eqreznegel  11196  negn0  11197  xrsupsslem  11527  xrinfmsslem  11528  supxrpnf  11539  supxrunb1  11540  supxrunb2  11541  iccsupr  11646  ssnn0fi  12094  incexclem  13648  gcdcllem1  14149  lubel  15752  clatleglb  15756  mulgpropd  16175  sylow2a  16639  efgi2  16743  lspsnel6  17640  submabas  19080  pmatcollpw3lem  19284  elcls2  19575  isclo2  19589  cmpsublem  19899  cmpsub  19900  hauscmplem  19906  1stcelcls  19962  llyss  19980  nllyss  19981  txkgen  20153  nrmr0reg  20250  uffix  20422  ufinffr  20430  ufilen  20431  fmfnfmlem2  20456  alexsubALTlem2  20548  alexsubALT  20551  metrest  21027  iccntr  21326  reconnlem2  21332  caubl  21746  ulmss  22792  axcontlem4  24270  nbgranself2  24436  cusgrarn  24459  ocsh  26201  ococss  26211  shorth  26213  spansnss2  26493  h1datomi  26499  pjss2i  26598  pjssmii  26599  pjorthcoi  27088  pj3si  27126  ssrelf  27466  dfimafnf  27473  funimass4f  27474  1stpreima  27524  2ndpreima  27525  ordtconlem1  27906  indpi1  28035  cvmlift2lem1  28747  dfon2lem6  29220  trpredmintr  29314  orderseqlem  29332  wfrlem10  29352  frrlem5b  29392  frrlem5d  29394  nofv  29417  nocvxminlem  29450  nocvxmin  29451  limsucncmpi  29910  ismtyres  30304  ispridlc  30467  pw2f1ocnv  30979  nzss  31222  ssrexf  31388  dfaimafn  32250  mgmplusfreseq  32461  gsumlsscl  32976  lincfsuppcl  33014  linccl  33015  onfrALTlem3  33316  onfrALTlem2  33318  sspwtr  33619  sspwtrALT  33620  sspwtrALT2  33623  pwtrVD  33624  pwtrrVD  33625  suctrALT2VD  33636  suctrALT2  33637  onfrALTlem3VD  33687  onfrALTlem2VD  33689  bnj518  33944  paddss1  35541  paddss2  35542  lspindp5  37497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator