Theorem ssel 3222

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 3216	. . . . . 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 1607	. . . 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 1928	. 2 |- ( A C_ B -> ( E. x ( x = C /\ x e. A ) -> E. x ( x = C /\ x e. B ) ) )
6		df-clel 2227	. 2 |- ( C e. A <-> E. x ( x = C /\ x e. A ) )
7		df-clel 2227	. 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 1396   = wceq 1398   E.wex 1541   e. wcel 2202   C_ wss 3201

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  ssel2  3223  sseli  3224  sseld  3227  sstr2  3235  nelss  3289  ssrexf  3290  ssralv  3292  ssrexv  3293  ralss  3294  rexss  3295  ssconb  3342  sscon  3343  ssdif  3344  unss1  3378  ssrin  3434  difin2  3471  reuss2  3489  reupick  3493  sssnm  3842  uniss  3919  ss2iun  3990  ssiun  4017  iinss  4027  disjss2  4072  disjss1  4075  pwnss  4255  sspwb  4314  ssopab2b  4377  soss  4417  sucssel  4527  ssorduni  4591  onintonm  4621  onnmin  4672  ssnel  4673  wessep  4682  ssrel  4820  ssrel2  4822  ssrelrel  4832  xpss12  4839  cnvss  4909  dmss  4936  elreldm  4964  dmcosseq  5010  relssres  5057  iss  5065  resopab2  5066  issref  5126  ssrnres  5186  dfco2a  5244  cores  5247  funssres  5376  fununi  5405  funimaexglem  5420  dfimafn  5703  funimass4  5705  funimass3  5772  dff4im  5801  funfvima2  5897  funfvima3  5898  f1elima  5924  riotass2  6010  ssoprab2b  6088  resoprab2  6128  relmptopab  6234  releldm2  6357  reldmtpos  6462  dmtpos  6465  rdgss  6592  ss2ixp  6923  1ndom2  7094  fiintim  7166  negf1o  8620  lbreu  9184  lbinf  9187  eqreznegel  9909  negm  9910  iccsupr  10262  negfi  11868  sumrbdclem  12018  prodrbdclem  12212  fprodmodd  12282  mulgpropdg  13831  subgintm  13865  subrngintm  14307  subrgintm  14338  islssm  14453  lspsnel6  14504  islidlm  14575  metrest  15317  bdop  16591  bj-nnen2lp  16670  exmidsbthrlem  16750