Theorem sseli 3220

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 3218	. 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 2200   C_ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  sselii  3221  sselid  3222  elun1  3371  elun2  3372  elopabr  4371  elopabran  4372  finds  4692  finds2  4693  issref  5111  2elresin  5434  fvun1  5700  fvmptssdm  5719  elfvmptrab1  5729  fvimacnvi  5749  elpreima  5754  ofrfval  6227  ofvalg  6228  off  6231  offres  6280  eqopi  6318  op1steq  6325  dfoprab4  6338  f1od2  6381  reldmtpos  6399  smores3  6439  smores2  6440  ctssdccl  7278  pinn  7496  indpi  7529  enq0enq  7618  preqlu  7659  elinp  7661  prop  7662  elnp1st2nd  7663  prarloclem5  7687  cauappcvgprlemladd  7845  peano5nnnn  8079  nnindnn  8080  recn  8132  rexr  8192  peano5nni  9113  nnre  9117  nncn  9118  nnind  9126  nnnn0  9376  nn0re  9378  nn0cn  9379  nn0xnn0  9436  nnz  9465  nn0z  9466  nnq  9828  qcn  9829  rpre  9856  iccshftri  10191  iccshftli  10193  iccdili  10195  icccntri  10197  fzval2  10207  fzelp1  10270  4fvwrd4  10336  elfzo1  10391  infssuzcldc  10455  expcllem  10772  expcl2lemap  10773  m1expcl2  10783  bcm1k  10982  bcpasc  10988  wrdv  11087  ccatclab  11129  pfxfv0  11224  pfxfvlsw  11227  cau3lem  11625  climconst2  11802  fsum3  11898  binomlem  11994  fprodge1  12150  cos12dec  12279  dvdsflip  12362  isprm3  12640  phimullem  12747  prmdiveq  12758  structcnvcnv  13048  fvsetsid  13066  ptex  13297  nmzsubg  13747  nmznsg  13750  nzrring  14147  lringnzr  14157  rege0subm  14548  znrrg  14624  tgval2  14725  qtopbasss  15195  dedekindicc  15307  ivthinc  15317  ivthdec  15318  dvply2  15441  cosz12  15454  cos0pilt1  15526  ioocosf1o  15528  mpodvdsmulf1o  15664  fsumdvdsmul  15665  lgsquadlemofi  15755  lgsquadlem1  15756  lgsquadlem2  15757  wlk1walkdom  16070  exmidsbthrlem  16390