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

Theorem ssel 3355
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 3350 . . . . . 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 1804 . . . 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 1676 . 2  |-  ( A 
C_  B  ->  ( E. x ( x  =  C  /\  x  e.  A )  ->  E. x
( x  =  C  /\  x  e.  B
) ) )
6 df-clel 2439 . 2  |-  ( C  e.  A  <->  E. x
( x  =  C  /\  x  e.  A
) )
7 df-clel 2439 . 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 1367    = wceq 1369   E.wex 1586    e. wcel 1756    C_ wss 3333
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3340  df-ss 3347
This theorem is referenced by:  ssel2  3356  sseli  3357  sseld  3360  sstr2  3368  nelss  3420  ssralv  3421  ssrexv  3422  ralss  3423  rexss  3424  ssconb  3494  sscon  3495  ssdif  3496  unss1  3530  ssrin  3580  difin2  3617  reuss2  3635  reupick  3639  elpwunsn  3922  sssn  4036  uniss  4117  ss2iun  4191  ssiun  4217  iinss  4226  disjss2  4270  disjss1  4273  pwnss  4462  sspwb  4546  ssopab2b  4620  pwssun  4632  soss  4664  oneqmini  4775  sucssel  4816  onssneli  4833  onssnel2i  4834  frinxp  4909  ssrel  4933  ssrel2  4935  ssrelrel  4945  xpss12  4950  cnvss  5017  dmss  5044  elreldm  5069  dmcosseq  5106  relssres  5152  iss  5159  resopab2  5160  issref  5216  ssrnres  5281  dfco2a  5343  cores  5346  funssres  5463  fununi  5489  dfimafn  5745  funimass4  5747  funimass3  5824  dff3  5861  dff4  5862  funfvima2  5958  funfvima3  5959  f1elima  5981  isomin  6033  isofrlem  6036  riotass2  6084  ssoprab2b  6148  resoprab2  6192  ssorduni  6402  onint  6411  oninton  6416  ssnlim  6499  releldm2  6629  reldmtpos  6758  dmtpos  6762  onfununi  6807  tz7.48lem  6901  tz7.49  6905  omeulem1  7026  omeulem2  7027  omsmolem  7097  omsmo  7098  ss2ixp  7281  boxriin  7310  onomeneq  7505  unblem1  7569  unblem3  7571  fiint  7593  inf3lem2  7840  cantnflem2  7903  tcel  7970  tz9.13  8003  rankr1ag  8014  rankpwi  8035  rankelb  8036  bndrank  8053  cardlim  8147  carduni  8156  acni2  8221  dfac12r  8320  cfub  8423  cflim2  8437  fin1a2lem9  8582  axdc3lem2  8625  axdclem2  8694  gch2  8847  eltsk2g  8923  suplem1pr  9226  fimaxre  10282  lbreu  10285  lbinfm  10288  sup2  10291  sup3  10292  infm3  10294  infmrcl  10314  uzwo  10922  uzwoOLD  10923  eqreznegel  10945  negn0  10946  xrsupsslem  11274  xrinfmsslem  11275  supxrpnf  11286  supxrunb1  11287  supxrunb2  11288  iccsupr  11387  incexclem  13304  gcdcllem1  13700  lubel  15297  clatleglb  15301  mulgpropd  15665  sylow2a  16123  efgi2  16227  lspsnel6  17080  mplcoe5lem  17552  submabas  18394  elcls2  18683  isclo2  18697  cmpsublem  19007  cmpsub  19008  hauscmplem  19014  1stcelcls  19070  llyss  19088  nllyss  19089  txkgen  19230  nrmr0reg  19327  uffix  19499  ufinffr  19507  ufilen  19508  fmfnfmlem2  19533  alexsubALTlem2  19625  alexsubALT  19628  metrest  20104  iccntr  20403  reconnlem2  20409  caubl  20823  ulmss  21867  axcontlem4  23218  nbgranself2  23352  cusgrarn  23372  ocsh  24691  ococss  24701  shorth  24703  spansnss2  24983  h1datomi  24989  pjss2i  25088  pjssmii  25089  pjorthcoi  25578  pj3si  25616  ssrelf  25950  dfimafnf  25955  funimass4f  25956  1stpreima  26006  2ndpreima  26007  ordtconlem1  26359  indpi1  26483  cvmlift2lem1  27196  dfon2lem6  27606  trpredmintr  27700  orderseqlem  27718  wfrlem10  27738  frrlem5b  27778  frrlem5d  27780  nofv  27803  nocvxminlem  27836  nocvxmin  27837  limsucncmpi  28296  ismtyres  28712  ispridlc  28875  pw2f1ocnv  29391  ssrexf  29740  dfaimafn  30076  ssnn0fi  30751  gsumlsscl  30819  lincfsuppcl  30952  linccl  30953  onfrALTlem3  31257  onfrALTlem2  31259  sspwtr  31560  sspwtrALT  31561  sspwtrALT2  31564  pwtrVD  31565  pwtrrVD  31566  suctrALT2VD  31577  suctrALT2  31578  onfrALTlem3VD  31628  onfrALTlem2VD  31630  bnj518  31884  paddss1  33466  paddss2  33467  lspindp5  35420
  Copyright terms: Public domain W3C validator