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  5702  fvmptssdm  5721  elfvmptrab1  5731  fvimacnvi  5751  elpreima  5756  ofrfval  6233  ofvalg  6234  off  6237  offres  6286  eqopi  6324  op1steq  6331  dfoprab4  6344  f1od2  6387  reldmtpos  6405  smores3  6445  smores2  6446  ctssdccl  7289  pinn  7507  indpi  7540  enq0enq  7629  preqlu  7670  elinp  7672  prop  7673  elnp1st2nd  7674  prarloclem5  7698  cauappcvgprlemladd  7856  peano5nnnn  8090  nnindnn  8091  recn  8143  rexr  8203  peano5nni  9124  nnre  9128  nncn  9129  nnind  9137  nnnn0  9387  nn0re  9389  nn0cn  9390  nn0xnn0  9447  nnz  9476  nn0z  9477  nnq  9840  qcn  9841  rpre  9868  iccshftri  10203  iccshftli  10205  iccdili  10207  icccntri  10209  fzval2  10219  fzelp1  10282  4fvwrd4  10348  elfzo1  10403  infssuzcldc  10467  expcllem  10784  expcl2lemap  10785  m1expcl2  10795  bcm1k  10994  bcpasc  11000  wrdv  11100  ccatclab  11142  pfxfv0  11240  pfxfvlsw  11243  cau3lem  11641  climconst2  11818  fsum3  11914  binomlem  12010  fprodge1  12166  cos12dec  12295  dvdsflip  12378  isprm3  12656  phimullem  12763  prmdiveq  12774  structcnvcnv  13064  fvsetsid  13082  ptex  13313  nmzsubg  13763  nmznsg  13766  nzrring  14163  lringnzr  14173  rege0subm  14564  znrrg  14640  tgval2  14741  qtopbasss  15211  dedekindicc  15323  ivthinc  15333  ivthdec  15334  dvply2  15457  cosz12  15470  cos0pilt1  15542  ioocosf1o  15544  mpodvdsmulf1o  15680  fsumdvdsmul  15681  lgsquadlemofi  15771  lgsquadlem1  15772  lgsquadlem2  15773  wlk1walkdom  16105  exmidsbthrlem  16478