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

Theorem ssel 3458
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 3453 . . . . . 6  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
21biimpi 197 . . . . 5  |-  ( A 
C_  B  ->  A. x
( x  e.  A  ->  x  e.  B ) )
3219.21bi 1924 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
43anim2d 567 . . 3  |-  ( A 
C_  B  ->  (
( x  =  C  /\  x  e.  A
)  ->  ( x  =  C  /\  x  e.  B ) ) )
54eximdv 1758 . 2  |-  ( A 
C_  B  ->  ( E. x ( x  =  C  /\  x  e.  A )  ->  E. x
( x  =  C  /\  x  e.  B
) ) )
6 df-clel 2417 . 2  |-  ( C  e.  A  <->  E. x
( x  =  C  /\  x  e.  A
) )
7 df-clel 2417 . 2  |-  ( C  e.  B  <->  E. x
( x  =  C  /\  x  e.  B
) )
85, 6, 73imtr4g 273 1  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370   A.wal 1435    = wceq 1437   E.wex 1657    e. wcel 1872    C_ wss 3436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-in 3443  df-ss 3450
This theorem is referenced by:  ssel2  3459  sseli  3460  sseld  3463  sstr2  3471  nelss  3523  ssrexf  3524  ssralv  3525  ssrexv  3526  ralss  3527  rexss  3528  ssconb  3598  sscon  3599  ssdif  3600  unss1  3635  ssrin  3687  difin2  3735  reuss2  3753  reupick  3757  elpwunsn  4040  sssn  4158  uniss  4240  ss2iun  4315  ssiun  4341  iinss  4350  disjss2  4397  disjss1  4400  pwnss  4589  sspwb  4670  ssopab2b  4747  pwssun  4759  soss  4792  frinxp  4919  ssrel  4942  ssrel2  4944  ssrelrel  4954  xpss12  4959  cnvss  5026  dmss  5053  elreldm  5078  dmcosseq  5115  relssres  5161  iss  5171  resopab2  5172  issref  5232  ssrnres  5294  dfco2a  5354  cores  5357  oneqmini  5493  sucssel  5534  onssneli  5551  onssnel2i  5552  funssres  5641  fununi  5667  dfimafn  5930  funimass4  5932  funimass3  6013  dff3  6050  dff4  6051  funfvima2  6156  funfvima3  6157  f1elima  6179  isomin  6243  isofrlem  6246  riotass2  6293  ssoprab2b  6362  resoprab2  6407  ssorduni  6626  onint  6636  oninton  6641  ssnlim  6724  releldm2  6857  reldmtpos  6992  dmtpos  6996  wfrlem10  7056  onfununi  7071  tz7.48lem  7169  tz7.49  7173  omeulem1  7294  omeulem2  7295  omsmolem  7365  omsmo  7366  ss2ixp  7546  boxriin  7575  onomeneq  7771  unblem1  7832  unblem3  7834  fiint  7857  inf3lem2  8143  cantnflem2  8203  tcel  8237  tz9.13  8270  rankr1ag  8281  rankpwi  8302  rankelb  8303  bndrank  8320  cardlim  8414  carduni  8423  acni2  8484  dfac12r  8583  cfub  8686  cflim2  8700  fin1a2lem9  8845  axdc3lem2  8888  axdclem2  8957  gch2  9107  eltsk2g  9183  suplem1pr  9484  negn0  10055  negf1o  10056  fimaxre  10558  negfi  10561  fiminre  10562  lbreu  10563  lbinf  10566  lbinfmOLD  10567  sup2  10572  sup3  10573  infm3  10575  infmrclOLD  10600  infregelb  10601  uzwo  11229  eqreznegel  11256  xrsupsslem  11599  xrinfmsslem  11600  supxrpnf  11611  supxrunb1  11612  supxrunb2  11613  iccsupr  11734  ssnn0fi  12203  incexclem  13893  gcdcllem1  14472  lcmscllemOLD  14581  lcmfnnval  14593  lcmfnnvalOLD  14596  lcmfnncl  14601  dvdslcmf  14603  lcmfunsnlem2lem2  14611  lcmfdvdsb  14615  lubel  16367  clatleglb  16371  mulgpropd  16790  sylow2a  17270  efgi2  17374  lspsnel6  18216  submabas  19601  pmatcollpw3lem  19805  elcls2  20088  isclo2  20102  cmpsublem  20412  cmpsub  20413  hauscmplem  20419  1stcelcls  20474  llyss  20492  nllyss  20493  txkgen  20665  nrmr0reg  20762  uffix  20934  ufinffr  20942  ufilen  20943  fmfnfmlem2  20968  alexsubALTlem2  21061  alexsubALT  21064  metrest  21537  iccntr  21837  reconnlem2  21843  caubl  22275  ulmss  23350  axcontlem4  24995  nbgranself2  25162  cusgrarn  25185  ocsh  26934  ococss  26944  shorth  26946  spansnss2  27226  h1datomi  27232  pjss2i  27331  pjssmii  27332  pjorthcoi  27820  pj3si  27858  ssrelf  28223  dfimafnf  28235  funimass4f  28236  fmptss  28279  1stpreima  28289  2ndpreima  28290  ordtconlem1  28738  indpi1  28851  bnj518  29705  cvmlift2lem1  30033  dfon2lem6  30441  trpredmintr  30479  orderseqlem  30497  frrlem5b  30526  frrlem5d  30528  nofv  30551  nocvxminlem  30584  nocvxmin  30585  limsucncmpi  31110  finxpreclem4  31750  poimirlem3  31907  poimirlem29  31933  poimirlem32  31936  ismtyres  32104  ispridlc  32267  paddss1  33351  paddss2  33352  lspindp5  35307  pw2f1ocnv  35862  ss2iundf  36221  iunrelexp0  36264  nzss  36636  onfrALTlem3  36880  onfrALTlem2  36882  sspwtr  37182  sspwtrALT  37183  sspwtrALT2  37192  pwtrVD  37193  pwtrrVD  37194  suctrALT2VD  37205  suctrALT2  37206  onfrALTlem3VD  37257  onfrALTlem2VD  37259  dfaimafn  38537  mgmplusfreseq  39393  gsumlsscl  39790  lincfsuppcl  39828  linccl  39829
  Copyright terms: Public domain W3C validator