Theorem ssel 3195

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 3189	. . . . . 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 1582	. . . 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 1904	. 2 |- ( A C_ B -> ( E. x ( x = C /\ x e. A ) -> E. x ( x = C /\ x e. B ) ) )
6		df-clel 2203	. 2 |- ( C e. A <-> E. x ( x = C /\ x e. A ) )
7		df-clel 2203	. 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 1371   = wceq 1373   E.wex 1516   e. wcel 2178   C_ wss 3174

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-in 3180  df-ss 3187

This theorem is referenced by:  ssel2  3196  sseli  3197  sseld  3200  sstr2  3208  nelss  3262  ssrexf  3263  ssralv  3265  ssrexv  3266  ralss  3267  rexss  3268  ssconb  3314  sscon  3315  ssdif  3316  unss1  3350  ssrin  3406  difin2  3443  reuss2  3461  reupick  3465  sssnm  3808  uniss  3885  ss2iun  3956  ssiun  3983  iinss  3993  disjss2  4038  disjss1  4041  pwnss  4219  sspwb  4278  ssopab2b  4341  soss  4379  sucssel  4489  ssorduni  4553  onintonm  4583  onnmin  4634  ssnel  4635  wessep  4644  ssrel  4781  ssrel2  4783  ssrelrel  4793  xpss12  4800  cnvss  4869  dmss  4896  elreldm  4923  dmcosseq  4969  relssres  5016  iss  5024  resopab2  5025  issref  5084  ssrnres  5144  dfco2a  5202  cores  5205  funssres  5332  fununi  5361  funimaexglem  5376  dfimafn  5650  funimass4  5652  funimass3  5719  dff4im  5749  funfvima2  5840  funfvima3  5841  f1elima  5865  riotass2  5949  ssoprab2b  6025  resoprab2  6065  releldm2  6294  reldmtpos  6362  dmtpos  6365  rdgss  6492  ss2ixp  6821  1ndom2  6987  fiintim  7054  negf1o  8489  lbreu  9053  lbinf  9056  eqreznegel  9770  negm  9771  iccsupr  10123  negfi  11654  sumrbdclem  11803  prodrbdclem  11997  fprodmodd  12067  mulgpropdg  13615  subgintm  13649  subrngintm  14089  subrgintm  14120  islssm  14234  lspsnel6  14285  islidlm  14356  metrest  15093  bdop  16010  bj-nnen2lp  16089  exmidsbthrlem  16163