Theorem sseli 3093

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 3091	. 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 1480   C_ wss 3071

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 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084

This theorem is referenced by:  sselii  3094  sseldi  3095  elun1  3243  elun2  3244  finds  4514  finds2  4515  issref  4921  2elresin  5234  fvun1  5487  fvmptssdm  5505  elfvmptrab1  5515  fvimacnvi  5534  elpreima  5539  ofrfval  5990  ofvalg  5991  off  5994  offres  6033  eqopi  6070  op1steq  6077  dfoprab4  6090  f1od2  6132  reldmtpos  6150  smores3  6190  smores2  6191  ctssdccl  6996  pinn  7124  indpi  7157  enq0enq  7246  preqlu  7287  elinp  7289  prop  7290  elnp1st2nd  7291  prarloclem5  7315  cauappcvgprlemladd  7473  peano5nnnn  7707  nnindnn  7708  recn  7760  rexr  7818  peano5nni  8730  nnre  8734  nncn  8735  nnind  8743  nnnn0  8991  nn0re  8993  nn0cn  8994  nn0xnn0  9051  nnz  9080  nn0z  9081  nnq  9432  qcn  9433  rpre  9455  iccshftri  9785  iccshftli  9787  iccdili  9789  icccntri  9791  fzval2  9800  fzelp1  9861  4fvwrd4  9924  elfzo1  9974  expcllem  10311  expcl2lemap  10312  m1expcl2  10322  bcm1k  10513  bcpasc  10519  cau3lem  10893  climconst2  11067  fsum3  11163  binomlem  11259  cos12dec  11481  dvdsflip  11556  infssuzcldc  11651  isprm3  11806  phimullem  11908  structcnvcnv  11985  fvsetsid  12003  tgval2  12230  qtopbasss  12700  dedekindicc  12790  ivthinc  12800  ivthdec  12801  cosz12  12871  exmidsbthrlem  13227