Theorem sseli 3244

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   C_ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  sselii  3245  sselid  3246  elun1  3396  elun2  3397  elopabr  4427  elopabran  4428  finds  4749  finds2  4750  issref  5173  2elresin  5497  fvun1  5772  fvmptssdm  5793  elfvmptrab1  5804  fvopab4ndm  5806  fvimacnvi  5826  elpreima  5831  ofrfval  6315  ofvalg  6316  off  6319  offres  6372  eqopi  6410  op1steq  6417  dfoprab4  6430  f1od2  6475  reldmtpos  6529  smores3  6569  smores2  6570  ctssdccl  7457  pinn  7682  indpi  7715  enq0enq  7804  preqlu  7845  elinp  7847  prop  7848  elnp1st2nd  7849  prarloclem5  7873  cauappcvgprlemladd  8031  peano5nnnn  8265  nnindnn  8266  recn  8318  rexr  8377  peano5nni  9316  nnre  9320  nncn  9321  nnind  9329  nnnn0  9581  nn0re  9583  nn0cn  9584  nn0xnn0  9643  nnz  9672  nn0z  9673  uzuzle35  9980  nnq  10048  qcn  10049  rpre  10077  iccshftri  10413  iccshftli  10415  iccdili  10417  icccntri  10419  fzval2  10430  fzelp1  10497  4fvwrd4  10563  elfzo1  10619  infssuzcldc  10684  expcllem  11007  expcl2lemap  11008  m1expcl2  11018  bcm1k  11219  bcpasc  11225  hashfibclem  11303  wrdv  11341  ccatclab  11383  pfxfv0  11485  pfxfvlsw  11488  cau3lem  11902  climconst2  12081  fsum3  12178  binomlem  12274  fprodge1  12430  cos12dec  12559  dvdsflip  12642  isprm3  12920  phimullem  13031  prmdiveq  13042  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemfmpn  13291  ballotfilemodife  13297  ballotfilemfrceq  13329  structcnvcnv  13425  fvsetsid  13443  ptex  13676  nmzsubg  14071  nmznsg  14074  cntzm  14160  cntzmhm  14172  nzrring  14598  lringnzr  14608  rege0subm  15029  znrrg  15103  psrbagconf1o  15177  tgval2  15294  qtopbasss  15764  dedekindicc  15876  ivthinc  15886  ivthdec  15887  dvply2  16010  cosz12  16024  cos0pilt1  16097  ioocosf1o  16099  mpodvdsmulf1o  16301  fsumdvdsmul  16302  lgsquadlemofi  16417  lgsquadlem1  16418  lgsquadlem2  16419  wlk1walkdom  16822  exmidsbthrlem  17290