Theorem sseli 3021

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 3019	. 2 |- ( A C_ B -> ( C e. A -> C e. B ) )
3	1, 2	ax-mp 7	1 |- ( C e. A -> C e. B )

Syntax hints:   -> wi 4   e. wcel 1438   C_ wss 2999

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-11 1442  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-in 3005  df-ss 3012

This theorem is referenced by:  sselii  3022  sseldi  3023  elun1  3167  elun2  3168  finds  4415  finds2  4416  issref  4814  2elresin  5125  fvun1  5370  fvmptssdm  5387  fvimacnvi  5413  elpreima  5418  ofrfval  5864  fnofval  5865  off  5868  offres  5906  eqopi  5942  op1steq  5949  dfoprab4  5962  f1od2  6000  reldmtpos  6018  smores3  6058  smores2  6059  pinn  6868  indpi  6901  enq0enq  6990  preqlu  7031  elinp  7033  prop  7034  elnp1st2nd  7035  prarloclem5  7059  cauappcvgprlemladd  7217  peano5nnnn  7427  nnindnn  7428  recn  7475  rexr  7533  peano5nni  8425  nnre  8429  nncn  8430  nnind  8438  nnnn0  8680  nn0re  8682  nn0cn  8683  nn0xnn0  8740  nnz  8769  nn0z  8770  nnq  9118  qcn  9119  rpre  9140  iccshftri  9412  iccshftli  9414  iccdili  9416  icccntri  9418  fzval2  9427  fzelp1  9488  4fvwrd4  9551  elfzo1  9601  expcllem  9966  expcl2lemap  9967  m1expcl2  9977  bcm1k  10168  bcpasc  10174  cau3lem  10547  climconst2  10679  fisum  10778  binomlem  10877  dvdsflip  11130  infssuzcldc  11225  isprm3  11378  phimullem  11479  structcnvcnv  11510  fvsetsid  11528  exmidsbthrlem  11912