Theorem sseli 3244

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 3242	. 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 2209   C_ wss 3220

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 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 theorem 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 referenced by:  sselii  3245  sselid  3246  elun1  3396  elun2  3397  elopabr  4420  elopabran  4421  finds  4742  finds2  4743  issref  5165  2elresin  5489  fvun1  5763  fvmptssdm  5784  elfvmptrab1  5794  fvimacnvi  5814  elpreima  5819  ofrfval  6301  ofvalg  6302  off  6305  offres  6358  eqopi  6396  op1steq  6403  dfoprab4  6416  f1od2  6461  reldmtpos  6514  smores3  6554  smores2  6555  ctssdccl  7441  pinn  7666  indpi  7699  enq0enq  7788  preqlu  7829  elinp  7831  prop  7832  elnp1st2nd  7833  prarloclem5  7857  cauappcvgprlemladd  8015  peano5nnnn  8249  nnindnn  8250  recn  8302  rexr  8361  peano5nni  9286  nnre  9290  nncn  9291  nnind  9299  nnnn0  9549  nn0re  9551  nn0cn  9552  nn0xnn0  9613  nnz  9642  nn0z  9643  uzuzle35  9944  nnq  10012  qcn  10013  rpre  10040  iccshftri  10376  iccshftli  10378  iccdili  10380  icccntri  10382  fzval2  10393  fzelp1  10459  4fvwrd4  10525  elfzo1  10581  infssuzcldc  10646  expcllem  10965  expcl2lemap  10966  m1expcl2  10976  bcm1k  11176  bcpasc  11182  hashfibclem  11260  wrdv  11298  ccatclab  11340  pfxfv0  11442  pfxfvlsw  11445  cau3lem  11858  climconst2  12035  fsum3  12132  binomlem  12228  fprodge1  12384  cos12dec  12513  dvdsflip  12596  isprm3  12874  phimullem  12981  prmdiveq  12992  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemfmpn  13212  ballotfilemodife  13218  ballotfilemfrceq  13250  structcnvcnv  13346  fvsetsid  13364  ptex  13595  nmzsubg  13990  nmznsg  13993  nzrring  14463  lringnzr  14473  rege0subm  14893  znrrg  14967  psrbagconf1o  14987  tgval2  15075  qtopbasss  15545  dedekindicc  15657  ivthinc  15667  ivthdec  15668  dvply2  15791  cosz12  15804  cos0pilt1  15876  ioocosf1o  15878  mpodvdsmulf1o  16018  fsumdvdsmul  16019  lgsquadlemofi  16109  lgsquadlem1  16110  lgsquadlem2  16111  wlk1walkdom  16514  exmidsbthrlem  16972