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

Theorem ssel 3347
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 3342 . . . . . 6  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
21biimpi 194 . . . . 5  |-  ( A 
C_  B  ->  A. x
( x  e.  A  ->  x  e.  B ) )
3219.21bi 1809 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
43anim2d 562 . . 3  |-  ( A 
C_  B  ->  (
( x  =  C  /\  x  e.  A
)  ->  ( x  =  C  /\  x  e.  B ) ) )
54eximdv 1681 . 2  |-  ( A 
C_  B  ->  ( E. x ( x  =  C  /\  x  e.  A )  ->  E. x
( x  =  C  /\  x  e.  B
) ) )
6 df-clel 2437 . 2  |-  ( C  e.  A  <->  E. x
( x  =  C  /\  x  e.  A
) )
7 df-clel 2437 . 2  |-  ( C  e.  B  <->  E. x
( x  =  C  /\  x  e.  B
) )
85, 6, 73imtr4g 270 1  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   A.wal 1362    = wceq 1364   E.wex 1591    e. wcel 1761    C_ wss 3325
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-in 3332  df-ss 3339
This theorem is referenced by:  ssel2  3348  sseli  3349  sseld  3352  sstr2  3360  nelss  3412  ssralv  3413  ssrexv  3414  ralss  3415  rexss  3416  ssconb  3486  sscon  3487  ssdif  3488  unss1  3522  ssrin  3572  difin2  3609  reuss2  3627  reupick  3631  elpwunsn  3914  sssn  4028  uniss  4109  ss2iun  4183  ssiun  4209  iinss  4218  disjss2  4262  disjss1  4265  pwnss  4454  sspwb  4538  ssopab2b  4613  pwssun  4623  soss  4655  oneqmini  4766  sucssel  4807  onssneli  4824  onssnel2i  4825  frinxp  4900  ssrel  4924  ssrel2  4926  ssrelrel  4936  xpss12  4941  cnvss  5008  dmss  5035  elreldm  5060  dmcosseq  5097  relssres  5144  iss  5151  resopab2  5152  issref  5208  ssrnres  5273  dfco2a  5335  cores  5338  funssres  5455  fununi  5481  dfimafn  5737  funimass4  5739  funimass3  5816  dff3  5853  dff4  5854  funfvima2  5950  funfvima3  5951  f1elima  5973  isomin  6025  isofrlem  6028  riotass2  6077  ssoprab2b  6142  resoprab2  6186  ssorduni  6396  onint  6405  oninton  6410  ssnlim  6493  releldm2  6623  reldmtpos  6752  dmtpos  6756  onfununi  6798  tz7.48lem  6892  tz7.49  6896  omeulem1  7017  omeulem2  7018  omsmolem  7088  omsmo  7089  ss2ixp  7272  boxriin  7301  onomeneq  7496  unblem1  7560  unblem3  7562  fiint  7584  inf3lem2  7831  cantnflem2  7894  tcel  7961  tz9.13  7994  rankr1ag  8005  rankpwi  8026  rankelb  8027  bndrank  8044  cardlim  8138  carduni  8147  acni2  8212  dfac12r  8311  cfub  8414  cflim2  8428  fin1a2lem9  8573  axdc3lem2  8616  axdclem2  8685  gch2  8838  eltsk2g  8914  suplem1pr  9217  fimaxre  10273  lbreu  10276  lbinfm  10279  sup2  10282  sup3  10283  infm3  10285  infmrcl  10305  uzwo  10913  uzwoOLD  10914  eqreznegel  10936  negn0  10937  xrsupsslem  11265  xrinfmsslem  11266  supxrpnf  11277  supxrunb1  11278  supxrunb2  11279  iccsupr  11378  incexclem  13295  gcdcllem1  13691  lubel  15288  clatleglb  15292  mulgpropd  15653  sylow2a  16111  efgi2  16215  lspsnel6  17053  submabas  18348  elcls2  18637  isclo2  18651  cmpsublem  18961  cmpsub  18962  hauscmplem  18968  1stcelcls  19024  llyss  19042  nllyss  19043  txkgen  19184  nrmr0reg  19281  uffix  19453  ufinffr  19461  ufilen  19462  fmfnfmlem2  19487  alexsubALTlem2  19579  alexsubALT  19582  metrest  20058  iccntr  20357  reconnlem2  20363  caubl  20777  ulmss  21821  axcontlem4  23148  nbgranself2  23282  cusgrarn  23302  ocsh  24621  ococss  24631  shorth  24633  spansnss2  24913  h1datomi  24919  pjss2i  25018  pjssmii  25019  pjorthcoi  25508  pj3si  25546  ssrelf  25880  dfimafnf  25885  funimass4f  25886  1stpreima  25936  2ndpreima  25937  ordtconlem1  26290  indpi1  26414  cvmlift2lem1  27121  dfon2lem6  27530  trpredmintr  27624  orderseqlem  27642  wfrlem10  27662  frrlem5b  27702  frrlem5d  27704  nofv  27727  nocvxminlem  27760  nocvxmin  27761  limsucncmpi  28221  ismtyres  28632  ispridlc  28795  pw2f1ocnv  29311  ssrexf  29660  dfaimafn  29996  gsumlsscl  30715  lincfsuppcl  30788  linccl  30789  onfrALTlem3  31085  onfrALTlem2  31087  sspwtr  31389  sspwtrALT  31390  sspwtrALT2  31393  pwtrVD  31394  pwtrrVD  31395  suctrALT2VD  31406  suctrALT2  31407  onfrALTlem3VD  31457  onfrALTlem2VD  31459  bnj518  31713  paddss1  33183  paddss2  33184  lspindp5  35137
  Copyright terms: Public domain W3C validator