Theorem ssel 3218

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		ssalel 3212	. . . . . 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 1604	. . . 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 1926	. 2 |- ( A C_ B -> ( E. x ( x = C /\ x e. A ) -> E. x ( x = C /\ x e. B ) ) )
6		df-clel 2225	. 2 |- ( C e. A <-> E. x ( x = C /\ x e. A ) )
7		df-clel 2225	. 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 1393   = wceq 1395   E.wex 1538   e. wcel 2200   C_ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  ssel2  3219  sseli  3220  sseld  3223  sstr2  3231  nelss  3285  ssrexf  3286  ssralv  3288  ssrexv  3289  ralss  3290  rexss  3291  ssconb  3337  sscon  3338  ssdif  3339  unss1  3373  ssrin  3429  difin2  3466  reuss2  3484  reupick  3488  sssnm  3832  uniss  3909  ss2iun  3980  ssiun  4007  iinss  4017  disjss2  4062  disjss1  4065  pwnss  4243  sspwb  4302  ssopab2b  4365  soss  4405  sucssel  4515  ssorduni  4579  onintonm  4609  onnmin  4660  ssnel  4661  wessep  4670  ssrel  4807  ssrel2  4809  ssrelrel  4819  xpss12  4826  cnvss  4895  dmss  4922  elreldm  4950  dmcosseq  4996  relssres  5043  iss  5051  resopab2  5052  issref  5111  ssrnres  5171  dfco2a  5229  cores  5232  funssres  5360  fununi  5389  funimaexglem  5404  dfimafn  5682  funimass4  5684  funimass3  5751  dff4im  5781  funfvima2  5872  funfvima3  5873  f1elima  5897  riotass2  5983  ssoprab2b  6061  resoprab2  6101  relmptopab  6207  releldm2  6331  reldmtpos  6399  dmtpos  6402  rdgss  6529  ss2ixp  6858  1ndom2  7026  fiintim  7093  negf1o  8528  lbreu  9092  lbinf  9095  eqreznegel  9809  negm  9810  iccsupr  10162  negfi  11739  sumrbdclem  11888  prodrbdclem  12082  fprodmodd  12152  mulgpropdg  13701  subgintm  13735  subrngintm  14176  subrgintm  14207  islssm  14321  lspsnel6  14372  islidlm  14443  metrest  15180  bdop  16238  bj-nnen2lp  16317  exmidsbthrlem  16390