Theorem sseli 3098

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 3096	. 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 1481   C_ wss 3076

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-in 3082  df-ss 3089

This theorem is referenced by:  sselii  3099  sseldi  3100  elun1  3248  elun2  3249  finds  4522  finds2  4523  issref  4929  2elresin  5242  fvun1  5495  fvmptssdm  5513  elfvmptrab1  5523  fvimacnvi  5542  elpreima  5547  ofrfval  5998  ofvalg  5999  off  6002  offres  6041  eqopi  6078  op1steq  6085  dfoprab4  6098  f1od2  6140  reldmtpos  6158  smores3  6198  smores2  6199  ctssdccl  7004  pinn  7141  indpi  7174  enq0enq  7263  preqlu  7304  elinp  7306  prop  7307  elnp1st2nd  7308  prarloclem5  7332  cauappcvgprlemladd  7490  peano5nnnn  7724  nnindnn  7725  recn  7777  rexr  7835  peano5nni  8747  nnre  8751  nncn  8752  nnind  8760  nnnn0  9008  nn0re  9010  nn0cn  9011  nn0xnn0  9068  nnz  9097  nn0z  9098  nnq  9452  qcn  9453  rpre  9477  iccshftri  9808  iccshftli  9810  iccdili  9812  icccntri  9814  fzval2  9824  fzelp1  9885  4fvwrd4  9948  elfzo1  9998  expcllem  10335  expcl2lemap  10336  m1expcl2  10346  bcm1k  10538  bcpasc  10544  cau3lem  10918  climconst2  11092  fsum3  11188  binomlem  11284  cos12dec  11510  dvdsflip  11585  infssuzcldc  11680  isprm3  11835  phimullem  11937  structcnvcnv  12014  fvsetsid  12032  tgval2  12259  qtopbasss  12729  dedekindicc  12819  ivthinc  12829  ivthdec  12830  cosz12  12909  cos0pilt1  12981  ioocosf1o  12983  exmidsbthrlem  13392