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

Theorem ssel 3174
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 3169 . . . . . 6  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
21biimpi 186 . . . . 5  |-  ( A 
C_  B  ->  A. x
( x  e.  A  ->  x  e.  B ) )
3219.21bi 1794 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
43anim2d 548 . . 3  |-  ( A 
C_  B  ->  (
( x  =  C  /\  x  e.  A
)  ->  ( x  =  C  /\  x  e.  B ) ) )
54eximdv 1608 . 2  |-  ( A 
C_  B  ->  ( E. x ( x  =  C  /\  x  e.  A )  ->  E. x
( x  =  C  /\  x  e.  B
) ) )
6 df-clel 2279 . 2  |-  ( C  e.  A  <->  E. x
( x  =  C  /\  x  e.  A
) )
7 df-clel 2279 . 2  |-  ( C  e.  B  <->  E. x
( x  =  C  /\  x  e.  B
) )
85, 6, 73imtr4g 261 1  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   A.wal 1527   E.wex 1528    = wceq 1623    e. wcel 1684    C_ wss 3152
This theorem is referenced by:  ssel2  3175  sseli  3176  sseld  3179  sstr2  3186  ssralv  3237  ssrexv  3238  ralss  3239  rexss  3240  ssconb  3309  sscon  3310  ssdif  3311  unss1  3344  ssrin  3394  difin2  3430  reuss2  3448  reupick  3452  sssn  3772  uniss  3848  ss2iun  3920  ssiun  3944  iinss  3953  disjss2  3996  disjss1  3999  pwnss  4176  sspwb  4223  ssopab2b  4291  pwssun  4299  soss  4332  oneqmini  4443  sucssel  4485  onssneli  4502  onssnel2i  4503  elpwunsn  4568  ssorduni  4577  onint  4586  oninton  4591  ssnlim  4674  frinxp  4755  ssrel  4776  ssrelrel  4787  xpss12  4792  cnvss  4854  dmss  4878  elreldm  4903  dmcosseq  4946  relssres  4992  iss  4998  resopab2  4999  issref  5056  ssrnres  5116  dfco2a  5173  cores  5176  funssres  5294  fununi  5316  dfimafn  5571  funimass4  5573  funimass3  5641  dff3  5673  dff4  5674  funfvima2  5754  funfvima3  5755  f1elima  5787  isomin  5834  isofrlem  5837  ssoprab2b  5905  resoprab2  5941  releldm2  6170  reldmtpos  6242  dmtpos  6246  riotass2  6332  onfununi  6358  tz7.48lem  6453  tz7.49  6457  omeulem1  6580  omeulem2  6581  omsmolem  6651  omsmo  6652  ss2ixp  6829  boxriin  6858  onomeneq  7050  unblem1  7109  unblem3  7111  fiint  7133  inf3lem2  7330  cantnflem2  7392  tcel  7430  tz9.13  7463  rankr1ag  7474  rankpwi  7495  rankelb  7496  bndrank  7513  cardlim  7605  carduni  7614  acni2  7673  dfac12r  7772  cfub  7875  cflim2  7889  fin1a2lem9  8034  axdc3lem2  8077  axdclem2  8147  gch2  8301  eltsk2g  8373  suplem1pr  8676  fimaxre  9701  lbreu  9704  lbinfm  9707  sup2  9710  sup3  9711  infm3  9713  infmrcl  9733  uzwo  10281  uzwoOLD  10282  eqreznegel  10303  negn0  10304  xrsupsslem  10625  xrinfmsslem  10626  supxrpnf  10637  supxrunb1  10638  supxrunb2  10639  iccsupr  10736  hashbclem  11390  incexclem  12295  gcdcllem1  12690  lubel  14226  clatleglb  14230  mulgpropd  14600  sylow2a  14930  efgi2  15034  lspsnel6  15751  elcls2  16811  isclo2  16825  cmpsublem  17126  cmpsub  17127  hauscmplem  17133  1stcelcls  17187  llyss  17205  nllyss  17206  txkgen  17346  nrmr0reg  17440  uffix  17616  ufinffr  17624  ufilen  17625  fmfnfmlem2  17650  alexsubALTlem2  17742  alexsubALT  17745  metrest  18070  iccntr  18326  reconnlem2  18332  caubl  18733  ulmss  19774  ocsh  21862  ococss  21872  shorth  21874  spansnss2  22154  h1datomi  22160  pjss2i  22259  pjssmii  22260  pjorthcoi  22749  pj3si  22787  dfimafnf  23041  funimass4f  23042  indpi1  23605  cvmlift2lem1  23833  dfon2lem6  24144  trpredmintr  24234  orderseqlem  24252  wfrlem10  24265  frrlem5b  24286  frrlem5d  24288  nofv  24311  nocvxminlem  24344  nocvxmin  24345  axcontlem4  24595  limsucncmpi  24884  imgfldref2  25064  prj1b  25079  prj3  25080  eqfnung2  25118  intfmu2  25519  supexr  25631  fnctartar  25907  fnctartar2  25908  lemindclsbu  25995  isconcl6a  26103  ismtyres  26532  ispridlc  26695  nelss  26751  pw2f1ocnv  27130  ssrexf  27684  fnvinran  27685  stoweidlem41  27790  stoweidlem44  27793  stoweidlem48  27797  stoweidlem51  27800  stoweidlem52  27801  stoweidlem53  27802  stoweidlem57  27806  stoweidlem59  27808  dfaimafn  28027  nbgranself2  28151  onfrALTlem3  28309  onfrALTlem2  28311  sspwtr  28595  sspwtrALT  28596  sspwtrALT2  28597  pwtrVD  28598  pwtrOLD  28599  pwtrrVD  28600  pwtrrOLD  28601  suctrALT2VD  28612  suctrALT2  28613  onfrALTlem3VD  28663  onfrALTlem2VD  28665  bnj518  28918  paddss1  30006  paddss2  30007  lspindp5  31960
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator