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

Theorem ssel 3498
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 3493 . . . . . 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 1818 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
43anim2d 565 . . 3  |-  ( A 
C_  B  ->  (
( x  =  C  /\  x  e.  A
)  ->  ( x  =  C  /\  x  e.  B ) ) )
54eximdv 1686 . 2  |-  ( A 
C_  B  ->  ( E. x ( x  =  C  /\  x  e.  A )  ->  E. x
( x  =  C  /\  x  e.  B
) ) )
6 df-clel 2462 . 2  |-  ( C  e.  A  <->  E. x
( x  =  C  /\  x  e.  A
) )
7 df-clel 2462 . 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 1377    = wceq 1379   E.wex 1596    e. wcel 1767    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490
This theorem is referenced by:  ssel2  3499  sseli  3500  sseld  3503  sstr2  3511  nelss  3563  ssralv  3564  ssrexv  3565  ralss  3566  rexss  3567  ssconb  3637  sscon  3638  ssdif  3639  unss1  3673  ssrin  3723  difin2  3760  reuss2  3778  reupick  3782  elpwunsn  4068  sssn  4185  uniss  4266  ss2iun  4341  ssiun  4367  iinss  4376  disjss2  4420  disjss1  4423  pwnss  4612  sspwb  4696  ssopab2b  4774  pwssun  4786  soss  4818  oneqmini  4929  sucssel  4970  onssneli  4987  onssnel2i  4988  frinxp  5064  ssrel  5089  ssrel2  5091  ssrelrel  5101  xpss12  5106  cnvss  5173  dmss  5200  elreldm  5225  dmcosseq  5262  relssres  5309  iss  5319  resopab2  5320  issref  5378  ssrnres  5443  dfco2a  5505  cores  5508  funssres  5626  fununi  5652  dfimafn  5914  funimass4  5916  funimass3  5995  dff3  6032  dff4  6033  funfvima2  6134  funfvima3  6135  f1elima  6157  isomin  6219  isofrlem  6222  riotass2  6270  ssoprab2b  6336  resoprab2  6381  ssorduni  6599  onint  6608  oninton  6613  ssnlim  6696  releldm2  6831  reldmtpos  6960  dmtpos  6964  onfununi  7009  tz7.48lem  7103  tz7.49  7107  omeulem1  7228  omeulem2  7229  omsmolem  7299  omsmo  7300  ss2ixp  7479  boxriin  7508  onomeneq  7704  unblem1  7768  unblem3  7770  fiint  7793  inf3lem2  8042  cantnflem2  8105  tcel  8172  tz9.13  8205  rankr1ag  8216  rankpwi  8237  rankelb  8238  bndrank  8255  cardlim  8349  carduni  8358  acni2  8423  dfac12r  8522  cfub  8625  cflim2  8639  fin1a2lem9  8784  axdc3lem2  8827  axdclem2  8896  gch2  9049  eltsk2g  9125  suplem1pr  9426  fimaxre  10486  lbreu  10489  lbinfm  10492  sup2  10495  sup3  10496  infm3  10498  infmrcl  10518  uzwo  11140  uzwoOLD  11141  eqreznegel  11163  negn0  11164  xrsupsslem  11494  xrinfmsslem  11495  supxrpnf  11506  supxrunb1  11507  supxrunb2  11508  iccsupr  11613  ssnn0fi  12058  incexclem  13607  gcdcllem1  14004  lubel  15605  clatleglb  15609  mulgpropd  15975  sylow2a  16435  efgi2  16539  lspsnel6  17423  mplcoe5lem  17901  submabas  18847  pmatcollpw3lem  19051  elcls2  19341  isclo2  19355  cmpsublem  19665  cmpsub  19666  hauscmplem  19672  1stcelcls  19728  llyss  19746  nllyss  19747  txkgen  19888  nrmr0reg  19985  uffix  20157  ufinffr  20165  ufilen  20166  fmfnfmlem2  20191  alexsubALTlem2  20283  alexsubALT  20286  metrest  20762  iccntr  21061  reconnlem2  21067  caubl  21481  ulmss  22526  axcontlem4  23946  nbgranself2  24112  cusgrarn  24135  ocsh  25877  ococss  25887  shorth  25889  spansnss2  26169  h1datomi  26175  pjss2i  26274  pjssmii  26275  pjorthcoi  26764  pj3si  26802  ssrelf  27139  dfimafnf  27146  funimass4f  27147  1stpreima  27196  2ndpreima  27197  ordtconlem1  27542  indpi1  27675  cvmlift2lem1  28387  dfon2lem6  28797  trpredmintr  28891  orderseqlem  28909  wfrlem10  28929  frrlem5b  28969  frrlem5d  28971  nofv  28994  nocvxminlem  29027  nocvxmin  29028  limsucncmpi  29487  ismtyres  29907  ispridlc  30070  pw2f1ocnv  30583  nzss  30822  ssrexf  30966  icccncfext  31226  dfaimafn  31717  gsumlsscl  32049  lincfsuppcl  32087  linccl  32088  onfrALTlem3  32396  onfrALTlem2  32398  sspwtr  32699  sspwtrALT  32700  sspwtrALT2  32703  pwtrVD  32704  pwtrrVD  32705  suctrALT2VD  32716  suctrALT2  32717  onfrALTlem3VD  32767  onfrALTlem2VD  32769  bnj518  33023  paddss1  34613  paddss2  34614  lspindp5  36567
  Copyright terms: Public domain W3C validator