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

Theorem ssel 3480
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 3475 . . . . . 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 1853 . . . 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 1695 . 2  |-  ( A 
C_  B  ->  ( E. x ( x  =  C  /\  x  e.  A )  ->  E. x
( x  =  C  /\  x  e.  B
) ) )
6 df-clel 2436 . 2  |-  ( C  e.  A  <->  E. x
( x  =  C  /\  x  e.  A
) )
7 df-clel 2436 . 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 1379    = wceq 1381   E.wex 1597    e. wcel 1802    C_ wss 3458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-in 3465  df-ss 3472
This theorem is referenced by:  ssel2  3481  sseli  3482  sseld  3485  sstr2  3493  nelss  3545  ssralv  3546  ssrexv  3547  ralss  3548  rexss  3549  ssconb  3619  sscon  3620  ssdif  3621  unss1  3655  ssrin  3705  difin2  3742  reuss2  3760  reupick  3764  elpwunsn  4051  sssn  4169  uniss  4251  ss2iun  4327  ssiun  4353  iinss  4362  disjss2  4406  disjss1  4409  pwnss  4598  sspwb  4682  ssopab2b  4760  pwssun  4772  soss  4804  oneqmini  4915  sucssel  4956  onssneli  4973  onssnel2i  4974  frinxp  5051  ssrel  5077  ssrel2  5079  ssrelrel  5089  xpss12  5094  cnvss  5161  dmss  5188  elreldm  5213  dmcosseq  5250  relssres  5297  iss  5307  resopab2  5308  issref  5366  ssrnres  5431  dfco2a  5493  cores  5496  funssres  5614  fununi  5640  dfimafn  5903  funimass4  5905  funimass3  5984  dff3  6025  dff4  6026  funfvima2  6129  funfvima3  6130  f1elima  6152  isomin  6214  isofrlem  6217  riotass2  6265  ssoprab2b  6335  resoprab2  6380  ssorduni  6602  onint  6611  oninton  6616  ssnlim  6699  releldm2  6831  reldmtpos  6961  dmtpos  6965  onfununi  7010  tz7.48lem  7104  tz7.49  7108  omeulem1  7229  omeulem2  7230  omsmolem  7300  omsmo  7301  ss2ixp  7480  boxriin  7509  onomeneq  7705  unblem1  7770  unblem3  7772  fiint  7795  inf3lem2  8044  cantnflem2  8107  tcel  8174  tz9.13  8207  rankr1ag  8218  rankpwi  8239  rankelb  8240  bndrank  8257  cardlim  8351  carduni  8360  acni2  8425  dfac12r  8524  cfub  8627  cflim2  8641  fin1a2lem9  8786  axdc3lem2  8829  axdclem2  8898  gch2  9051  eltsk2g  9127  suplem1pr  9428  fimaxre  10491  lbreu  10494  lbinfm  10497  sup2  10500  sup3  10501  infm3  10503  infmrcl  10523  uzwo  11148  uzwoOLD  11149  eqreznegel  11171  negn0  11172  xrsupsslem  11502  xrinfmsslem  11503  supxrpnf  11514  supxrunb1  11515  supxrunb2  11516  iccsupr  11621  ssnn0fi  12068  incexclem  13622  gcdcllem1  14021  lubel  15621  clatleglb  15625  mulgpropd  16044  sylow2a  16508  efgi2  16612  lspsnel6  17508  submabas  18947  pmatcollpw3lem  19151  elcls2  19441  isclo2  19455  cmpsublem  19765  cmpsub  19766  hauscmplem  19772  1stcelcls  19828  llyss  19846  nllyss  19847  txkgen  20019  nrmr0reg  20116  uffix  20288  ufinffr  20296  ufilen  20297  fmfnfmlem2  20322  alexsubALTlem2  20414  alexsubALT  20417  metrest  20893  iccntr  21192  reconnlem2  21198  caubl  21612  ulmss  22657  axcontlem4  24135  nbgranself2  24301  cusgrarn  24324  ocsh  26066  ococss  26076  shorth  26078  spansnss2  26358  h1datomi  26364  pjss2i  26463  pjssmii  26464  pjorthcoi  26953  pj3si  26991  ssrelf  27331  dfimafnf  27338  funimass4f  27339  1stpreima  27389  2ndpreima  27390  ordtconlem1  27772  indpi1  27901  cvmlift2lem1  28613  dfon2lem6  29188  trpredmintr  29282  orderseqlem  29300  wfrlem10  29320  frrlem5b  29360  frrlem5d  29362  nofv  29385  nocvxminlem  29418  nocvxmin  29419  limsucncmpi  29878  ismtyres  30272  ispridlc  30435  pw2f1ocnv  30947  nzss  31191  ssrexf  31335  dfaimafn  32084  mgmplusfreseq  32295  gsumlsscl  32686  lincfsuppcl  32724  linccl  32725  onfrALTlem3  33024  onfrALTlem2  33026  sspwtr  33327  sspwtrALT  33328  sspwtrALT2  33331  pwtrVD  33332  pwtrrVD  33333  suctrALT2VD  33344  suctrALT2  33345  onfrALTlem3VD  33395  onfrALTlem2VD  33397  bnj518  33651  paddss1  35243  paddss2  35244  lspindp5  37199
  Copyright terms: Public domain W3C validator