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  6528  smores3  6568  smores2  6569  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  9645  nnz  9674  nn0z  9675  uzuzle35  9981  nnq  10049  qcn  10050  rpre  10078  iccshftri  10414  iccshftli  10416  iccdili  10418  icccntri  10420  fzval2  10431  fzelp1  10498  4fvwrd4  10564  elfzo1  10620  infssuzcldc  10685  expcllem  11008  expcl2lemap  11009  m1expcl2  11019  bcm1k  11220  bcpasc  11226  hashfibclem  11304  wrdv  11342  ccatclab  11384  pfxfv0  11486  pfxfvlsw  11489  cau3lem  11903  climconst2  12082  fsum3  12179  binomlem  12275  fprodge1  12431  cos12dec  12560  dvdsflip  12643  isprm3  12921  phimullem  13032  prmdiveq  13043  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemfmpn  13292  ballotfilemodife  13298  ballotfilemfrceq  13330  structcnvcnv  13426  fvsetsid  13444  ptex  13677  nmzsubg  14072  nmznsg  14075  cntzm  14161  cntzmhm  14173  nzrring  14599  lringnzr  14609  rege0subm  15030  znrrg  15104  psrbagconf1o  15174  tgval2  15277  qtopbasss  15747  dedekindicc  15859  ivthinc  15869  ivthdec  15870  dvply2  15993  cosz12  16007  cos0pilt1  16080  ioocosf1o  16082  mpodvdsmulf1o  16284  fsumdvdsmul  16285  lgsquadlemofi  16400  lgsquadlem1  16401  lgsquadlem2  16402  wlk1walkdom  16805  exmidsbthrlem  17273