Theorem ssel 3242

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 3235	. . . . . 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 1611	. . . 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 1933	. 2 |- ( A C_ B -> ( E. x ( x = C /\ x e. A ) -> E. x ( x = C /\ x e. B ) ) )
6		df-clel 2234	. 2 |- ( C e. A <-> E. x ( x = C /\ x e. A ) )
7		df-clel 2234	. 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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   A.wal 1400   = wceq 1402   E.wex 1545   e. wcel 2209   C_ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  ssel2  3243  sseli  3244  sseld  3247  sstr2  3255  nelss  3309  ssrexf  3310  ssralv  3312  ssrexv  3313  ralss  3314  rexss  3315  ssconb  3362  sscon  3363  ssdif  3364  unss1  3398  ssrin  3456  difin2  3493  reuss2  3513  reupick  3517  sssnm  3879  uniss  3956  ss2iun  4027  ssiun  4054  iinss  4064  disjss2  4109  disjss1  4112  pwnss  4296  sspwb  4356  ssopab2b  4419  soss  4459  sucssel  4569  ssorduni  4634  onintonm  4664  onnmin  4715  ssnel  4716  wessep  4725  ssrel  4863  ssrel2  4865  ssrelrel  4875  xpss12  4882  cnvss  4953  dmss  4980  elreldm  5008  dmcosseq  5054  relssres  5101  iss  5109  resopab2  5110  issref  5170  ssrnres  5230  dfco2a  5288  cores  5291  funssres  5420  fununi  5449  funimaexglem  5464  dfimafn  5751  funimass4  5753  funimass3  5825  dff4im  5854  funfvima2  5951  funfvima3  5952  dfimafnf  5955  f1elima  5979  riotass2  6067  ssoprab2b  6145  resoprab2  6185  relmptopab  6291  funimass4f  6359  releldm2  6419  reldmtpos  6524  dmtpos  6527  rdgss  6654  ss2ixp  6993  1ndom2  7166  fiintim  7238  negf1o  8709  lbreu  9275  lbinf  9278  eqreznegel  10014  negm  10015  iccsupr  10368  negfi  11994  sumrbdclem  12144  prodrbdclem  12338  fprodmodd  12408  mulgpropdg  13967  subgintm  14001  subrngintm  14520  subrgintm  14551  islssm  14694  ellspsn6  14745  islidlm  14816  metrest  15607  bdop  16901  bj-nnen2lp  16980  exmidsbthrlem  17067