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

Theorem ssel 3483
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 3478 . . . . . 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 1874 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
43anim2d 563 . . 3  |-  ( A 
C_  B  ->  (
( x  =  C  /\  x  e.  A
)  ->  ( x  =  C  /\  x  e.  B ) ) )
54eximdv 1715 . 2  |-  ( A 
C_  B  ->  ( E. x ( x  =  C  /\  x  e.  A )  ->  E. x
( x  =  C  /\  x  e.  B
) ) )
6 df-clel 2449 . 2  |-  ( C  e.  A  <->  E. x
( x  =  C  /\  x  e.  A
) )
7 df-clel 2449 . 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 367   A.wal 1396    = wceq 1398   E.wex 1617    e. wcel 1823    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3468  df-ss 3475
This theorem is referenced by:  ssel2  3484  sseli  3485  sseld  3488  sstr2  3496  nelss  3548  ssrexf  3549  ssralv  3550  ssrexv  3551  ralss  3552  rexss  3553  ssconb  3623  sscon  3624  ssdif  3625  unss1  3659  ssrin  3709  difin2  3757  reuss2  3775  reupick  3779  elpwunsn  4057  sssn  4174  uniss  4256  ss2iun  4331  ssiun  4357  iinss  4366  disjss2  4413  disjss1  4416  pwnss  4602  sspwb  4686  ssopab2b  4763  pwssun  4775  soss  4807  oneqmini  4918  sucssel  4959  onssneli  4976  onssnel2i  4977  frinxp  5054  ssrel  5079  ssrel2  5081  ssrelrel  5091  xpss12  5096  cnvss  5164  dmss  5191  elreldm  5216  dmcosseq  5253  relssres  5299  iss  5309  resopab2  5310  issref  5368  ssrnres  5430  dfco2a  5490  cores  5493  funssres  5610  fununi  5636  dfimafn  5897  funimass4  5899  funimass3  5979  dff3  6020  dff4  6021  funfvima2  6123  funfvima3  6124  f1elima  6146  isomin  6208  isofrlem  6211  riotass2  6258  ssoprab2b  6327  resoprab2  6372  ssorduni  6594  onint  6603  oninton  6608  ssnlim  6691  releldm2  6823  reldmtpos  6955  dmtpos  6959  onfununi  7004  tz7.48lem  7098  tz7.49  7102  omeulem1  7223  omeulem2  7224  omsmolem  7294  omsmo  7295  ss2ixp  7475  boxriin  7504  onomeneq  7700  unblem1  7764  unblem3  7766  fiint  7789  inf3lem2  8037  cantnflem2  8100  tcel  8167  tz9.13  8200  rankr1ag  8211  rankpwi  8232  rankelb  8233  bndrank  8250  cardlim  8344  carduni  8353  acni2  8418  dfac12r  8517  cfub  8620  cflim2  8634  fin1a2lem9  8779  axdc3lem2  8822  axdclem2  8891  gch2  9042  eltsk2g  9118  suplem1pr  9419  fimaxre  10485  lbreu  10488  lbinfm  10491  sup2  10494  sup3  10495  infm3  10497  infmrcl  10517  uzwo  11145  uzwoOLD  11146  eqreznegel  11168  negn0  11169  xrsupsslem  11501  xrinfmsslem  11502  supxrpnf  11513  supxrunb1  11514  supxrunb2  11515  iccsupr  11620  ssnn0fi  12079  incexclem  13733  gcdcllem1  14236  lubel  15954  clatleglb  15958  mulgpropd  16377  sylow2a  16841  efgi2  16945  lspsnel6  17838  submabas  19250  pmatcollpw3lem  19454  elcls2  19745  isclo2  19759  cmpsublem  20069  cmpsub  20070  hauscmplem  20076  1stcelcls  20131  llyss  20149  nllyss  20150  txkgen  20322  nrmr0reg  20419  uffix  20591  ufinffr  20599  ufilen  20600  fmfnfmlem2  20625  alexsubALTlem2  20717  alexsubALT  20720  metrest  21196  iccntr  21495  reconnlem2  21501  caubl  21915  ulmss  22961  axcontlem4  24475  nbgranself2  24641  cusgrarn  24664  ocsh  26402  ococss  26412  shorth  26414  spansnss2  26694  h1datomi  26700  pjss2i  26799  pjssmii  26800  pjorthcoi  27289  pj3si  27327  ssrelf  27684  dfimafnf  27697  funimass4f  27698  fmptss  27746  1stpreima  27756  2ndpreima  27757  ordtconlem1  28144  indpi1  28254  cvmlift2lem1  29014  dfon2lem6  29463  trpredmintr  29557  orderseqlem  29575  wfrlem10  29595  frrlem5b  29635  frrlem5d  29637  nofv  29660  nocvxminlem  29693  nocvxmin  29694  limsucncmpi  30141  ismtyres  30547  ispridlc  30710  pw2f1ocnv  31221  nzss  31466  dfaimafn  32492  mgmplusfreseq  32852  gsumlsscl  33249  lincfsuppcl  33287  linccl  33288  onfrALTlem3  33729  onfrALTlem2  33731  sspwtr  34032  sspwtrALT  34033  sspwtrALT2  34042  pwtrVD  34043  pwtrrVD  34044  suctrALT2VD  34055  suctrALT2  34056  onfrALTlem3VD  34107  onfrALTlem2VD  34109  bnj518  34364  paddss1  35957  paddss2  35958  lspindp5  37913  iunrelexp0  38245
  Copyright terms: Public domain W3C validator