Theorem sseli 3189

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 3187	. 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 2176   C_ wss 3166

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179

This theorem is referenced by:  sselii  3190  sselid  3191  elun1  3340  elun2  3341  finds  4649  finds2  4650  issref  5066  2elresin  5388  fvun1  5647  fvmptssdm  5666  elfvmptrab1  5676  fvimacnvi  5696  elpreima  5701  ofrfval  6169  ofvalg  6170  off  6173  offres  6222  eqopi  6260  op1steq  6267  dfoprab4  6280  f1od2  6323  reldmtpos  6341  smores3  6381  smores2  6382  ctssdccl  7215  pinn  7424  indpi  7457  enq0enq  7546  preqlu  7587  elinp  7589  prop  7590  elnp1st2nd  7591  prarloclem5  7615  cauappcvgprlemladd  7773  peano5nnnn  8007  nnindnn  8008  recn  8060  rexr  8120  peano5nni  9041  nnre  9045  nncn  9046  nnind  9054  nnnn0  9304  nn0re  9306  nn0cn  9307  nn0xnn0  9364  nnz  9393  nn0z  9394  nnq  9756  qcn  9757  rpre  9784  iccshftri  10119  iccshftli  10121  iccdili  10123  icccntri  10125  fzval2  10135  fzelp1  10198  4fvwrd4  10264  elfzo1  10316  infssuzcldc  10380  expcllem  10697  expcl2lemap  10698  m1expcl2  10708  bcm1k  10907  bcpasc  10913  wrdv  11012  ccatclab  11053  pfxfv0  11146  pfxfvlsw  11149  cau3lem  11458  climconst2  11635  fsum3  11731  binomlem  11827  fprodge1  11983  cos12dec  12112  dvdsflip  12195  isprm3  12473  phimullem  12580  prmdiveq  12591  structcnvcnv  12881  fvsetsid  12899  ptex  13129  nmzsubg  13579  nmznsg  13582  nzrring  13978  lringnzr  13988  rege0subm  14379  znrrg  14455  tgval2  14556  qtopbasss  15026  dedekindicc  15138  ivthinc  15148  ivthdec  15149  dvply2  15272  cosz12  15285  cos0pilt1  15357  ioocosf1o  15359  mpodvdsmulf1o  15495  fsumdvdsmul  15496  lgsquadlemofi  15586  lgsquadlem1  15587  lgsquadlem2  15588  exmidsbthrlem  15998