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

Theorem ssel 3464
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 3459 . . . . . 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 1922 . . . 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 1757 . 2  |-  ( A 
C_  B  ->  ( E. x ( x  =  C  /\  x  e.  A )  ->  E. x
( x  =  C  /\  x  e.  B
) ) )
6 df-clel 2424 . 2  |-  ( C  e.  A  <->  E. x
( x  =  C  /\  x  e.  A
) )
7 df-clel 2424 . 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 1659    e. wcel 1870    C_ wss 3442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-in 3449  df-ss 3456
This theorem is referenced by:  ssel2  3465  sseli  3466  sseld  3469  sstr2  3477  nelss  3529  ssrexf  3530  ssralv  3531  ssrexv  3532  ralss  3533  rexss  3534  ssconb  3604  sscon  3605  ssdif  3606  unss1  3641  ssrin  3693  difin2  3741  reuss2  3759  reupick  3763  elpwunsn  4043  sssn  4161  uniss  4243  ss2iun  4318  ssiun  4344  iinss  4353  disjss2  4400  disjss1  4403  pwnss  4590  sspwb  4671  ssopab2b  4748  pwssun  4760  soss  4793  frinxp  4920  ssrel  4943  ssrel2  4945  ssrelrel  4955  xpss12  4960  cnvss  5027  dmss  5054  elreldm  5079  dmcosseq  5116  relssres  5162  iss  5172  resopab2  5173  issref  5233  ssrnres  5295  dfco2a  5355  cores  5358  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  6989  dmtpos  6993  wfrlem10  7053  onfununi  7068  tz7.48lem  7166  tz7.49  7170  omeulem1  7291  omeulem2  7292  omsmolem  7362  omsmo  7363  ss2ixp  7543  boxriin  7572  onomeneq  7768  unblem1  7829  unblem3  7831  fiint  7854  inf3lem2  8134  cantnflem2  8194  tcel  8228  tz9.13  8261  rankr1ag  8272  rankpwi  8293  rankelb  8294  bndrank  8311  cardlim  8405  carduni  8414  acni2  8475  dfac12r  8574  cfub  8677  cflim2  8691  fin1a2lem9  8836  axdc3lem2  8879  axdclem2  8948  gch2  9099  eltsk2g  9175  suplem1pr  9476  negn0  10047  negf1o  10048  fimaxre  10551  negfi  10554  fiminre  10555  lbreu  10556  lbinf  10559  lbinfmOLD  10560  sup2  10565  sup3  10566  infm3  10568  infmrclOLD  10593  infregelb  10594  uzwo  11222  eqreznegel  11249  xrsupsslem  11592  xrinfmsslem  11593  supxrpnf  11604  supxrunb1  11605  supxrunb2  11606  iccsupr  11727  ssnn0fi  12194  incexclem  13872  gcdcllem1  14447  lcmscllemOLD  14553  lcmfnnval  14565  lcmfnnvalOLD  14568  lcmfnncl  14573  dvdslcmf  14575  lcmfunsnlem2lem2  14583  lcmfdvdsb  14587  lubel  16319  clatleglb  16323  mulgpropd  16742  sylow2a  17206  efgi2  17310  lspsnel6  18152  submabas  19534  pmatcollpw3lem  19738  elcls2  20021  isclo2  20035  cmpsublem  20345  cmpsub  20346  hauscmplem  20352  1stcelcls  20407  llyss  20425  nllyss  20426  txkgen  20598  nrmr0reg  20695  uffix  20867  ufinffr  20875  ufilen  20876  fmfnfmlem2  20901  alexsubALTlem2  20994  alexsubALT  20997  metrest  21470  iccntr  21750  reconnlem2  21756  caubl  22170  ulmss  23217  axcontlem4  24843  nbgranself2  25009  cusgrarn  25032  ocsh  26771  ococss  26781  shorth  26783  spansnss2  27063  h1datomi  27069  pjss2i  27168  pjssmii  27169  pjorthcoi  27657  pj3si  27695  ssrelf  28060  dfimafnf  28073  funimass4f  28074  fmptss  28117  1stpreima  28127  2ndpreima  28128  ordtconlem1  28569  indpi1  28682  bnj518  29485  cvmlift2lem1  29813  dfon2lem6  30221  trpredmintr  30259  orderseqlem  30277  frrlem5b  30306  frrlem5d  30308  nofv  30331  nocvxminlem  30364  nocvxmin  30365  limsucncmpi  30890  poimirlem3  31646  poimirlem29  31672  poimirlem32  31675  ismtyres  31843  ispridlc  32006  paddss1  33090  paddss2  33091  lspindp5  35046  pw2f1ocnv  35597  ss2iundf  35889  iunrelexp0  35932  nzss  36302  onfrALTlem3  36546  onfrALTlem2  36548  sspwtr  36848  sspwtrALT  36849  sspwtrALT2  36858  pwtrVD  36859  pwtrrVD  36860  suctrALT2VD  36871  suctrALT2  36872  onfrALTlem3VD  36923  onfrALTlem2VD  36925  dfaimafn  38056  mgmplusfreseq  38530  gsumlsscl  38927  lincfsuppcl  38965  linccl  38966
  Copyright terms: Public domain W3C validator