Theorem sseli 3124

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 3122	. 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 2128   C_ wss 3102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-in 3108  df-ss 3115

This theorem is referenced by:  sselii  3125  sseldi  3126  elun1  3274  elun2  3275  finds  4557  finds2  4558  issref  4965  2elresin  5278  fvun1  5531  fvmptssdm  5549  elfvmptrab1  5559  fvimacnvi  5578  elpreima  5583  ofrfval  6034  ofvalg  6035  off  6038  offres  6077  eqopi  6114  op1steq  6121  dfoprab4  6134  f1od2  6176  reldmtpos  6194  smores3  6234  smores2  6235  ctssdccl  7045  pinn  7212  indpi  7245  enq0enq  7334  preqlu  7375  elinp  7377  prop  7378  elnp1st2nd  7379  prarloclem5  7403  cauappcvgprlemladd  7561  peano5nnnn  7795  nnindnn  7796  recn  7848  rexr  7906  peano5nni  8819  nnre  8823  nncn  8824  nnind  8832  nnnn0  9080  nn0re  9082  nn0cn  9083  nn0xnn0  9140  nnz  9169  nn0z  9170  nnq  9524  qcn  9525  rpre  9549  iccshftri  9881  iccshftli  9883  iccdili  9885  icccntri  9887  fzval2  9897  fzelp1  9958  4fvwrd4  10021  elfzo1  10071  expcllem  10412  expcl2lemap  10413  m1expcl2  10423  bcm1k  10616  bcpasc  10622  cau3lem  10996  climconst2  11170  fsum3  11266  binomlem  11362  fprodge1  11518  cos12dec  11646  dvdsflip  11724  infssuzcldc  11819  isprm3  11975  phimullem  12077  prmdiveq  12088  structcnvcnv  12166  fvsetsid  12184  tgval2  12411  qtopbasss  12881  dedekindicc  12971  ivthinc  12981  ivthdec  12982  cosz12  13061  cos0pilt1  13133  ioocosf1o  13135  exmidsbthrlem  13555