Theorem sseli 3224

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 3222	. 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 2202   C_ wss 3201

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  sselii  3225  sselid  3226  elun1  3376  elun2  3377  elopabr  4383  elopabran  4384  finds  4704  finds2  4705  issref  5126  2elresin  5450  fvun1  5721  fvmptssdm  5740  elfvmptrab1  5750  fvimacnvi  5770  elpreima  5775  ofrfval  6253  ofvalg  6254  off  6257  offres  6306  eqopi  6344  op1steq  6351  dfoprab4  6364  f1od2  6409  reldmtpos  6462  smores3  6502  smores2  6503  ctssdccl  7370  pinn  7589  indpi  7622  enq0enq  7711  preqlu  7752  elinp  7754  prop  7755  elnp1st2nd  7756  prarloclem5  7780  cauappcvgprlemladd  7938  peano5nnnn  8172  nnindnn  8173  recn  8225  rexr  8284  peano5nni  9205  nnre  9209  nncn  9210  nnind  9218  nnnn0  9468  nn0re  9470  nn0cn  9471  nn0xnn0  9530  nnz  9559  nn0z  9560  uzuzle35  9860  nnq  9928  qcn  9929  rpre  9956  iccshftri  10291  iccshftli  10293  iccdili  10295  icccntri  10297  fzval2  10308  fzelp1  10371  4fvwrd4  10437  elfzo1  10493  infssuzcldc  10558  expcllem  10875  expcl2lemap  10876  m1expcl2  10886  bcm1k  11085  bcpasc  11091  wrdv  11195  ccatclab  11237  pfxfv0  11339  pfxfvlsw  11342  cau3lem  11754  climconst2  11931  fsum3  12028  binomlem  12124  fprodge1  12280  cos12dec  12409  dvdsflip  12492  isprm3  12770  phimullem  12877  prmdiveq  12888  structcnvcnv  13178  fvsetsid  13196  ptex  13427  nmzsubg  13877  nmznsg  13880  nzrring  14278  lringnzr  14288  rege0subm  14680  znrrg  14756  psrbagconf1o  14774  tgval2  14862  qtopbasss  15332  dedekindicc  15444  ivthinc  15454  ivthdec  15455  dvply2  15578  cosz12  15591  cos0pilt1  15663  ioocosf1o  15665  mpodvdsmulf1o  15804  fsumdvdsmul  15805  lgsquadlemofi  15895  lgsquadlem1  15896  lgsquadlem2  15897  wlk1walkdom  16300  exmidsbthrlem  16750