Theorem ssel 3173

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 3168	. . . . . 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 2189	. 2 |- ( C e. A <-> E. x ( x = C /\ x e. A ) )
7		df-clel 2189	. 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 2164   C_ wss 3153

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 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3159  df-ss 3166

This theorem is referenced by:  ssel2  3174  sseli  3175  sseld  3178  sstr2  3186  nelss  3240  ssrexf  3241  ssralv  3243  ssrexv  3244  ralss  3245  rexss  3246  ssconb  3292  sscon  3293  ssdif  3294  unss1  3328  ssrin  3384  difin2  3421  reuss2  3439  reupick  3443  sssnm  3780  uniss  3856  ss2iun  3927  ssiun  3954  iinss  3964  disjss2  4009  disjss1  4012  pwnss  4188  sspwb  4245  ssopab2b  4307  soss  4345  sucssel  4455  ssorduni  4519  onintonm  4549  onnmin  4600  ssnel  4601  wessep  4610  ssrel  4747  ssrel2  4749  ssrelrel  4759  xpss12  4766  cnvss  4835  dmss  4861  elreldm  4888  dmcosseq  4933  relssres  4980  iss  4988  resopab2  4989  issref  5048  ssrnres  5108  dfco2a  5166  cores  5169  funssres  5296  fununi  5322  funimaexglem  5337  dfimafn  5605  funimass4  5607  funimass3  5674  dff4im  5704  funfvima2  5791  funfvima3  5792  f1elima  5816  riotass2  5900  ssoprab2b  5975  resoprab2  6015  releldm2  6238  reldmtpos  6306  dmtpos  6309  rdgss  6436  ss2ixp  6765  fiintim  6985  negf1o  8401  lbreu  8964  lbinf  8967  eqreznegel  9679  negm  9680  iccsupr  10032  negfi  11371  sumrbdclem  11520  prodrbdclem  11714  fprodmodd  11784  mulgpropdg  13234  subgintm  13268  subrngintm  13708  subrgintm  13739  islssm  13853  lspsnel6  13904  islidlm  13975  metrest  14674  bdop  15367  bj-nnen2lp  15446  exmidsbthrlem  15512