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

Theorem ssel 3394
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 3389 . . . . . 6  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
21biimpi 199 . . . . 5  |-  ( A 
C_  B  ->  A. x
( x  e.  A  ->  x  e.  B ) )
3219.21bi 1952 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
43anim2d 573 . . 3  |-  ( A 
C_  B  ->  (
( x  =  C  /\  x  e.  A
)  ->  ( x  =  C  /\  x  e.  B ) ) )
54eximdv 1768 . 2  |-  ( A 
C_  B  ->  ( E. x ( x  =  C  /\  x  e.  A )  ->  E. x
( x  =  C  /\  x  e.  B
) ) )
6 df-clel 2448 . 2  |-  ( C  e.  A  <->  E. x
( x  =  C  /\  x  e.  A
) )
7 df-clel 2448 . 2  |-  ( C  e.  B  <->  E. x
( x  =  C  /\  x  e.  B
) )
85, 6, 73imtr4g 278 1  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375   A.wal 1446    = wceq 1448   E.wex 1667    e. wcel 1891    C_ wss 3372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-in 3379  df-ss 3386
This theorem is referenced by:  ssel2  3395  sseli  3396  sseld  3399  sstr2  3407  nelss  3459  ssrexf  3460  ssralv  3461  ssrexv  3462  ralss  3463  rexss  3464  ssconb  3534  sscon  3535  ssdif  3536  unss1  3571  ssrin  3625  difin2  3673  reuss2  3691  reupick  3695  elpwunsn  3980  sssn  4099  uniss  4189  ss2iun  4264  ssiun  4290  iinss  4299  disjss2  4348  disjss1  4351  pwnss  4541  sspwb  4622  ssopab2b  4701  pwssun  4718  soss  4751  frinxp  4878  ssrel  4901  ssrel2  4903  ssrelrel  4913  xpss12  4918  cnvss  4985  dmss  5012  elreldm  5037  dmcosseq  5074  relssres  5120  iss  5130  resopab2  5131  issref  5191  ssrnres  5253  dfco2a  5314  cores  5317  oneqmini  5453  sucssel  5494  onssneli  5511  onssnel2i  5512  funssres  5601  fununi  5631  dfimafn  5897  funimass4  5899  funimass3  5982  dff3  6019  dff4  6020  funfvima2  6127  funfvima3  6128  f1elima  6150  isomin  6214  isofrlem  6217  riotass2  6264  ssoprab2b  6336  resoprab2  6381  ssorduni  6600  onint  6610  oninton  6615  ssnlim  6698  releldm2  6831  reldmtpos  6968  dmtpos  6972  wfrlem10  7032  onfununi  7047  tz7.48lem  7145  tz7.49  7149  omeulem1  7270  omeulem2  7271  omsmolem  7341  omsmo  7342  ss2ixp  7522  boxriin  7551  onomeneq  7749  unblem1  7810  unblem3  7812  fiint  7835  inf3lem2  8121  cantnflem2  8182  tcel  8216  tz9.13  8249  rankr1ag  8260  rankpwi  8281  rankelb  8282  bndrank  8299  cardlim  8393  carduni  8402  acni2  8464  dfac12r  8563  cfub  8666  cflim2  8680  fin1a2lem9  8825  axdc3lem2  8868  axdclem2  8937  gch2  9087  eltsk2g  9163  suplem1pr  9464  negn0  10037  negf1o  10038  fimaxre  10540  negfi  10543  fiminre  10544  lbreu  10545  lbinf  10548  lbinfmOLD  10549  sup2  10554  sup3  10555  infm3  10557  infmrclOLD  10582  infregelb  10583  uzwo  11212  eqreznegel  11239  xrsupsslem  11582  xrinfmsslem  11583  supxrpnf  11594  supxrunb1  11595  supxrunb2  11596  iccsupr  11717  ssnn0fi  12191  incexclem  13905  gcdcllem1  14484  lcmscllemOLD  14593  lcmfnnval  14605  lcmfnnvalOLD  14608  lcmfnncl  14613  dvdslcmf  14615  lcmfunsnlem2lem2  14623  lcmfdvdsb  14627  lubel  16379  clatleglb  16383  mulgpropd  16802  sylow2a  17282  efgi2  17386  lspsnel6  18228  submabas  19614  pmatcollpw3lem  19818  elcls2  20101  isclo2  20115  cmpsublem  20425  cmpsub  20426  hauscmplem  20432  1stcelcls  20487  llyss  20505  nllyss  20506  txkgen  20678  nrmr0reg  20775  uffix  20947  ufinffr  20955  ufilen  20956  fmfnfmlem2  20981  alexsubALTlem2  21074  alexsubALT  21077  metrest  21550  iccntr  21850  reconnlem2  21856  caubl  22288  ulmss  23364  axcontlem4  25009  nbgranself2  25176  cusgrarn  25199  ocsh  26948  ococss  26958  shorth  26960  spansnss2  27240  h1datomi  27246  pjss2i  27345  pjssmii  27346  pjorthcoi  27834  pj3si  27872  ssrelf  28230  dfimafnf  28242  funimass4f  28243  fmptss  28285  1stpreima  28295  2ndpreima  28296  ordtconlem1  28737  indpi1  28850  bnj518  29703  cvmlift2lem1  30031  dfon2lem6  30440  trpredmintr  30478  orderseqlem  30496  frrlem5b  30525  frrlem5d  30527  nofv  30550  nocvxminlem  30585  nocvxmin  30586  limsucncmpi  31111  finxpreclem4  31788  poimirlem3  31945  poimirlem29  31971  poimirlem32  31974  ismtyres  32142  ispridlc  32305  paddss1  33384  paddss2  33385  lspindp5  35340  pw2f1ocnv  35894  ss2iundf  36253  iunrelexp0  36296  nzss  36667  onfrALTlem3  36911  onfrALTlem2  36913  sspwtr  37206  sspwtrALT  37207  sspwtrALT2  37216  pwtrVD  37217  pwtrrVD  37218  suctrALT2VD  37229  suctrALT2  37230  onfrALTlem3VD  37281  onfrALTlem2VD  37283  qndenserrnopnlem  38223  dfaimafn  38758  mgmplusfreseq  40098  gsumlsscl  40493  lincfsuppcl  40531  linccl  40532
  Copyright terms: Public domain W3C validator