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  4648  finds2  4649  issref  5065  2elresin  5387  fvun1  5645  fvmptssdm  5664  elfvmptrab1  5674  fvimacnvi  5694  elpreima  5699  ofrfval  6167  ofvalg  6168  off  6171  offres  6220  eqopi  6258  op1steq  6265  dfoprab4  6278  f1od2  6321  reldmtpos  6339  smores3  6379  smores2  6380  ctssdccl  7213  pinn  7422  indpi  7455  enq0enq  7544  preqlu  7585  elinp  7587  prop  7588  elnp1st2nd  7589  prarloclem5  7613  cauappcvgprlemladd  7771  peano5nnnn  8005  nnindnn  8006  recn  8058  rexr  8118  peano5nni  9039  nnre  9043  nncn  9044  nnind  9052  nnnn0  9302  nn0re  9304  nn0cn  9305  nn0xnn0  9362  nnz  9391  nn0z  9392  nnq  9754  qcn  9755  rpre  9782  iccshftri  10117  iccshftli  10119  iccdili  10121  icccntri  10123  fzval2  10133  fzelp1  10196  4fvwrd4  10262  elfzo1  10314  infssuzcldc  10378  expcllem  10695  expcl2lemap  10696  m1expcl2  10706  bcm1k  10905  bcpasc  10911  wrdv  11010  ccatclab  11050  cau3lem  11425  climconst2  11602  fsum3  11698  binomlem  11794  fprodge1  11950  cos12dec  12079  dvdsflip  12162  isprm3  12440  phimullem  12547  prmdiveq  12558  structcnvcnv  12848  fvsetsid  12866  ptex  13096  nmzsubg  13546  nmznsg  13549  nzrring  13945  lringnzr  13955  rege0subm  14346  znrrg  14422  tgval2  14523  qtopbasss  14993  dedekindicc  15105  ivthinc  15115  ivthdec  15116  dvply2  15239  cosz12  15252  cos0pilt1  15324  ioocosf1o  15326  mpodvdsmulf1o  15462  fsumdvdsmul  15463  lgsquadlemofi  15553  lgsquadlem1  15554  lgsquadlem2  15555  exmidsbthrlem  15961