Theorem ssel 3164

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 3159	. . . . . 6 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
2	1	biimpi 120	. . . . 5 |- ( A C_ B -> A. x ( x e. A -> x e. B ) )
3	2	19.21bi 1569	. . . 4 |- ( A C_ B -> ( x e. A -> x e. B ) )
4	3	anim2d 337	. . 3 |- ( A C_ B -> ( ( x = C /\ x e. A ) -> ( x = C /\ x e. B ) ) )
5	4	eximdv 1891	. 2 |- ( A C_ B -> ( E. x ( x = C /\ x e. A ) -> E. x ( x = C /\ x e. B ) ) )
6		df-clel 2185	. 2 |- ( C e. A <-> E. x ( x = C /\ x e. A ) )
7		df-clel 2185	. 2 |- ( C e. B <-> E. x ( x = C /\ x e. B ) )
8	5, 6, 7	3imtr4g 205	1 |- ( A C_ B -> ( C e. A -> C e. B ) )

Syntax hints:   -> wi 4   /\ wa 104   A.wal 1362   = wceq 1364   E.wex 1503   e. wcel 2160   C_ wss 3144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-in 3150  df-ss 3157

This theorem is referenced by:  ssel2  3165  sseli  3166  sseld  3169  sstr2  3177  nelss  3231  ssrexf  3232  ssralv  3234  ssrexv  3235  ralss  3236  rexss  3237  ssconb  3283  sscon  3284  ssdif  3285  unss1  3319  ssrin  3375  difin2  3412  reuss2  3430  reupick  3434  sssnm  3769  uniss  3845  ss2iun  3916  ssiun  3943  iinss  3953  disjss2  3998  disjss1  4001  pwnss  4177  sspwb  4234  ssopab2b  4294  soss  4332  sucssel  4442  ssorduni  4504  onintonm  4534  onnmin  4585  ssnel  4586  wessep  4595  ssrel  4732  ssrel2  4734  ssrelrel  4744  xpss12  4751  cnvss  4818  dmss  4844  elreldm  4871  dmcosseq  4916  relssres  4963  iss  4971  resopab2  4972  issref  5029  ssrnres  5089  dfco2a  5147  cores  5150  funssres  5277  fununi  5303  funimaexglem  5318  dfimafn  5584  funimass4  5586  funimass3  5652  dff4im  5682  funfvima2  5769  funfvima3  5770  f1elima  5794  riotass2  5877  ssoprab2b  5952  resoprab2  5992  releldm2  6209  reldmtpos  6277  dmtpos  6280  rdgss  6407  ss2ixp  6736  fiintim  6956  negf1o  8368  lbreu  8931  lbinf  8934  eqreznegel  9643  negm  9644  iccsupr  9995  negfi  11267  sumrbdclem  11416  prodrbdclem  11610  fprodmodd  11680  mulgpropdg  13101  subgintm  13134  subrngintm  13556  subrgintm  13587  islssm  13670  lspsnel6  13721  islidlm  13792  metrest  14458  bdop  15080  bj-nnen2lp  15159  exmidsbthrlem  15224