Theorem sseli 3197

Description: Membership inference from subclass relationship. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
sseli.1	|- A C_ B

Assertion

Ref	Expression
sseli	|- ( C e. A -> C e. B )

Proof of Theorem sseli

Step	Hyp	Ref	Expression
1		sseli.1	. 2 |- A C_ B
2		ssel 3195	. 2 |- ( A C_ B -> ( C e. A -> C e. B ) )
3	1, 2	ax-mp 5	1 |- ( C e. A -> C e. B )

Syntax hints:   -> wi 4   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:  sselii  3198  sselid  3199  elun1  3348  elun2  3349  finds  4666  finds2  4667  issref  5084  2elresin  5406  fvun1  5668  fvmptssdm  5687  elfvmptrab1  5697  fvimacnvi  5717  elpreima  5722  ofrfval  6190  ofvalg  6191  off  6194  offres  6243  eqopi  6281  op1steq  6288  dfoprab4  6301  f1od2  6344  reldmtpos  6362  smores3  6402  smores2  6403  ctssdccl  7239  pinn  7457  indpi  7490  enq0enq  7579  preqlu  7620  elinp  7622  prop  7623  elnp1st2nd  7624  prarloclem5  7648  cauappcvgprlemladd  7806  peano5nnnn  8040  nnindnn  8041  recn  8093  rexr  8153  peano5nni  9074  nnre  9078  nncn  9079  nnind  9087  nnnn0  9337  nn0re  9339  nn0cn  9340  nn0xnn0  9397  nnz  9426  nn0z  9427  nnq  9789  qcn  9790  rpre  9817  iccshftri  10152  iccshftli  10154  iccdili  10156  icccntri  10158  fzval2  10168  fzelp1  10231  4fvwrd4  10297  elfzo1  10351  infssuzcldc  10415  expcllem  10732  expcl2lemap  10733  m1expcl2  10743  bcm1k  10942  bcpasc  10948  wrdv  11047  ccatclab  11088  pfxfv0  11183  pfxfvlsw  11186  cau3lem  11540  climconst2  11717  fsum3  11813  binomlem  11909  fprodge1  12065  cos12dec  12194  dvdsflip  12277  isprm3  12555  phimullem  12662  prmdiveq  12673  structcnvcnv  12963  fvsetsid  12981  ptex  13211  nmzsubg  13661  nmznsg  13664  nzrring  14060  lringnzr  14070  rege0subm  14461  znrrg  14537  tgval2  14638  qtopbasss  15108  dedekindicc  15220  ivthinc  15230  ivthdec  15231  dvply2  15354  cosz12  15367  cos0pilt1  15439  ioocosf1o  15441  mpodvdsmulf1o  15577  fsumdvdsmul  15578  lgsquadlemofi  15668  lgsquadlem1  15669  lgsquadlem2  15670  exmidsbthrlem  16163