Theorem ssel 3597

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.

Step	Hyp	Ref	Expression
1		dfss2 3591	. . . . . 6 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
2	1	biimpi 206	. . . . 5 |- ( A C_ B -> A. x ( x e. A -> x e. B ) )
3	2	19.21bi 2059	. . . 4 |- ( A C_ B -> ( x e. A -> x e. B ) )
4	3	anim2d 589	. . 3 |- ( A C_ B -> ( ( x = C /\ x e. A ) -> ( x = C /\ x e. B ) ) )
5	4	eximdv 1846	. 2 |- ( A C_ B -> ( E. x ( x = C /\ x e. A ) -> E. x ( x = C /\ x e. B ) ) )
6		df-clel 2618	. 2 |- ( C e. A <-> E. x ( x = C /\ x e. A ) )
7		df-clel 2618	. 2 |- ( C e. B <-> E. x ( x = C /\ x e. B ) )
8	5, 6, 7	3imtr4g 285	1 |- ( A C_ B -> ( C e. A -> C e. B ) )

Syntax hints:   -> wi 4   /\ wa 384   A.wal 1481   = wceq 1483   E.wex 1704   e. wcel 1990   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  ssel2  3598  sseli  3599  sseld  3602  sstr2  3610  nelss  3664  ssrexf  3665  ssralv  3666  ssrexv  3667  ralss  3668  rexss  3669  ssconb  3743  sscon  3744  ssdif  3745  unss1  3782  ssrin  3838  difin2  3890  reuss2  3907  reupick  3911  elpwunsn  4224  sssn  4358  uniss  4458  ss2iun  4536  ssiun  4562  iinss  4571  disjss2  4623  disjss1  4626  pwnss  4830  sspwb  4917  ssopab2b  5002  pwssun  5020  soss  5053  frinxp  5184  ssrel  5207  ssrelOLD  5208  ssrel2  5210  ssrelrel  5220  xpss12  5225  cnvssOLD  5295  dmss  5323  elreldm  5350  dmcosseq  5387  relssres  5437  iss  5447  resopab2  5448  issref  5509  ssrnres  5572  dfco2a  5635  cores  5638  oneqmini  5776  sucssel  5819  onssneli  5837  onssnel2i  5838  funssres  5930  fununi  5964  dfimafn  6245  funimass4  6247  funimass3  6333  dff3  6372  dff4  6373  funfvima2  6493  funfvima3  6495  f1elima  6520  isomin  6587  isofrlem  6590  riotass2  6638  ssoprab2b  6712  resoprab2  6757  ssorduni  6985  onint  6995  oninton  7000  ssnlim  7083  releldm2  7218  reldmtpos  7360  dmtpos  7364  wfrlem10  7424  onfununi  7438  tz7.48lem  7536  tz7.49  7540  omeulem1  7662  omeulem2  7663  omsmolem  7733  omsmo  7734  ss2ixp  7921  boxriin  7950  onomeneq  8150  unblem1  8212  unblem3  8214  fiint  8237  inf3lem2  8526  cantnflem2  8587  tcel  8621  tz9.13  8654  rankr1ag  8665  rankpwi  8686  rankelb  8687  bndrank  8704  cardlim  8798  carduni  8807  acni2  8869  dfac12r  8968  cfub  9071  cflim2  9085  fin1a2lem9  9230  axdc3lem2  9273  axdclem2  9342  gch2  9497  eltsk2g  9573  suplem1pr  9874  negn0  10459  negf1o  10460  fimaxre  10968  negfi  10971  fiminre  10972  lbreu  10973  lbinf  10976  sup2  10979  sup3  10980  infm3  10982  infregelb  11007  uzwo  11751  eqreznegel  11774  xrsupsslem  12137  xrinfmsslem  12138  supxrpnf  12148  supxrunb1  12149  supxrunb2  12150  iccsupr  12266  ssnn0fi  12784  incexclem  14568  fprodmodd  14728  sumeven  15110  sumodd  15111  gcdcllem1  15221  lcmfnnval  15337  lcmfnncl  15342  dvdslcmf  15344  lcmfunsnlem2lem2  15352  lcmfdvdsb  15356  lubel  17122  clatleglb  17126  mulgpropd  17584  sylow2a  18034  efgi2  18138  lspsnel6  18994  submabas  20384  pmatcollpw3lem  20588  elcls2  20878  isclo2  20892  cmpsublem  21202  cmpsub  21203  hauscmplem  21209  1stcelcls  21264  llyss  21282  nllyss  21283  txkgen  21455  nrmr0reg  21552  uffix  21725  ufinffr  21733  ufilen  21734  fmfnfmlem2  21759  alexsubALTlem2  21852  alexsubALT  21855  metrest  22329  iccntr  22624  reconnlem2  22630  clmneg1  22882  clmvscom  22890  caubl  23106  ulmss  24151  axcontlem4  25847  ocsh  28142  ococss  28152  shorth  28154  spansnss2  28434  h1datomi  28440  pjss2i  28539  pjssmii  28540  pjorthcoi  29028  pj3si  29066  ssrelf  29425  dfimafnf  29436  funimass4f  29437  mptssALT  29474  1stpreima  29484  2ndpreima  29485  ordtconnlem1  29970  indpi1  30082  bnj518  30956  cvmlift2lem1  31284  dfon2lem6  31693  trpredmintr  31731  orderseqlem  31749  frrlem5b  31785  frrlem5d  31787  nofv  31810  nocvxminlem  31893  nocvxmin  31894  limsucncmpi  32444  finxpreclem4  33231  poimirlem3  33412  poimirlem29  33438  poimirlem32  33441  ismtyres  33607  ispridlc  33869  ssbr  34008  iss2  34112  paddss1  35103  paddss2  35104  lspindp5  37059  pw2f1ocnv  37604  ss2iundf  37951  iunrelexp0  37994  gneispace0nelrn3  38440  nzss  38516  onfrALTlem3  38759  onfrALTlem2  38761  sspwtr  39048  sspwtrALT  39049  sspwtrALT2  39058  pwtrVD  39059  pwtrrVD  39060  suctrALT2VD  39071  suctrALT2  39072  onfrALTlem3VD  39123  onfrALTlem2VD  39125  iinssf  39327  qndenserrnopnlem  40517  dfaimafn  41245  sprsymrelfolem2  41743  mgmplusfreseq  41773  gsumlsscl  42164  lincfsuppcl  42202  linccl  42203  onsetrec  42451