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  5684  funimass4  5686  funimass3  5753  dff4im  5783  funfvima2  5876  funfvima3  5877  f1elima  5903  riotass2  5989  ssoprab2b  6067  resoprab2  6107  relmptopab  6213  releldm2  6337  reldmtpos  6405  dmtpos  6408  rdgss  6535  ss2ixp  6866  1ndom2  7034  fiintim  7104  negf1o  8539  lbreu  9103  lbinf  9106  eqreznegel  9821  negm  9822  iccsupr  10174  negfi  11755  sumrbdclem  11904  prodrbdclem  12098  fprodmodd  12168  mulgpropdg  13717  subgintm  13751  subrngintm  14192  subrgintm  14223  islssm  14337  lspsnel6  14388  islidlm  14459  metrest  15196  bdop  16321  bj-nnen2lp  16400  exmidsbthrlem  16478