Theorem sseli 3179

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 3177	. 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 2167   C_ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  sselii  3180  sselid  3181  elun1  3330  elun2  3331  finds  4636  finds2  4637  issref  5052  2elresin  5369  fvun1  5627  fvmptssdm  5646  elfvmptrab1  5656  fvimacnvi  5676  elpreima  5681  ofrfval  6144  ofvalg  6145  off  6148  offres  6192  eqopi  6230  op1steq  6237  dfoprab4  6250  f1od2  6293  reldmtpos  6311  smores3  6351  smores2  6352  ctssdccl  7177  pinn  7376  indpi  7409  enq0enq  7498  preqlu  7539  elinp  7541  prop  7542  elnp1st2nd  7543  prarloclem5  7567  cauappcvgprlemladd  7725  peano5nnnn  7959  nnindnn  7960  recn  8012  rexr  8072  peano5nni  8993  nnre  8997  nncn  8998  nnind  9006  nnnn0  9256  nn0re  9258  nn0cn  9259  nn0xnn0  9316  nnz  9345  nn0z  9346  nnq  9707  qcn  9708  rpre  9735  iccshftri  10070  iccshftli  10072  iccdili  10074  icccntri  10076  fzval2  10086  fzelp1  10149  4fvwrd4  10215  elfzo1  10266  infssuzcldc  10325  expcllem  10642  expcl2lemap  10643  m1expcl2  10653  bcm1k  10852  bcpasc  10858  wrdv  10951  cau3lem  11279  climconst2  11456  fsum3  11552  binomlem  11648  fprodge1  11804  cos12dec  11933  dvdsflip  12016  isprm3  12286  phimullem  12393  prmdiveq  12404  structcnvcnv  12694  fvsetsid  12712  ptex  12935  nmzsubg  13340  nmznsg  13343  nzrring  13739  lringnzr  13749  rege0subm  14140  znrrg  14216  tgval2  14287  qtopbasss  14757  dedekindicc  14869  ivthinc  14879  ivthdec  14880  dvply2  15003  cosz12  15016  cos0pilt1  15088  ioocosf1o  15090  mpodvdsmulf1o  15226  fsumdvdsmul  15227  lgsquadlemofi  15317  lgsquadlem1  15318  lgsquadlem2  15319  exmidsbthrlem  15666