Theorem sseli 3223

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 3221	. 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 2202   C_ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  sselii  3224  sselid  3225  elun1  3374  elun2  3375  elopabr  4377  elopabran  4378  finds  4698  finds2  4699  issref  5119  2elresin  5443  fvun1  5712  fvmptssdm  5731  elfvmptrab1  5741  fvimacnvi  5761  elpreima  5766  ofrfval  6244  ofvalg  6245  off  6248  offres  6297  eqopi  6335  op1steq  6342  dfoprab4  6355  f1od2  6400  reldmtpos  6419  smores3  6459  smores2  6460  ctssdccl  7310  pinn  7529  indpi  7562  enq0enq  7651  preqlu  7692  elinp  7694  prop  7695  elnp1st2nd  7696  prarloclem5  7720  cauappcvgprlemladd  7878  peano5nnnn  8112  nnindnn  8113  recn  8165  rexr  8225  peano5nni  9146  nnre  9150  nncn  9151  nnind  9159  nnnn0  9409  nn0re  9411  nn0cn  9412  nn0xnn0  9469  nnz  9498  nn0z  9499  uzuzle35  9799  nnq  9867  qcn  9868  rpre  9895  iccshftri  10230  iccshftli  10232  iccdili  10234  icccntri  10236  fzval2  10246  fzelp1  10309  4fvwrd4  10375  elfzo1  10431  infssuzcldc  10496  expcllem  10813  expcl2lemap  10814  m1expcl2  10824  bcm1k  11023  bcpasc  11029  wrdv  11133  ccatclab  11175  pfxfv0  11277  pfxfvlsw  11280  cau3lem  11692  climconst2  11869  fsum3  11966  binomlem  12062  fprodge1  12218  cos12dec  12347  dvdsflip  12430  isprm3  12708  phimullem  12815  prmdiveq  12826  structcnvcnv  13116  fvsetsid  13134  ptex  13365  nmzsubg  13815  nmznsg  13818  nzrring  14216  lringnzr  14226  rege0subm  14617  znrrg  14693  tgval2  14794  qtopbasss  15264  dedekindicc  15376  ivthinc  15386  ivthdec  15387  dvply2  15510  cosz12  15523  cos0pilt1  15595  ioocosf1o  15597  mpodvdsmulf1o  15733  fsumdvdsmul  15734  lgsquadlemofi  15824  lgsquadlem1  15825  lgsquadlem2  15826  wlk1walkdom  16229  exmidsbthrlem  16677