Theorem sseli 3166

Description: Membership inference from subclass relationship. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
sseli.1	⊢ 𝐴 ⊆ 𝐵

Assertion

Ref	Expression
sseli	⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)

Proof of Theorem sseli

Step	Hyp	Ref	Expression
1		sseli.1	. 2 ⊢ 𝐴 ⊆ 𝐵
2		ssel 3164	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2160   ⊆ wss 3144

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-in 3150  df-ss 3157

This theorem is referenced by:  sselii  3167  sselid  3168  elun1  3317  elun2  3318  finds  4614  finds2  4615  issref  5026  2elresin  5343  fvun1  5599  fvmptssdm  5617  elfvmptrab1  5627  fvimacnvi  5647  elpreima  5652  ofrfval  6110  ofvalg  6111  off  6114  offres  6155  eqopi  6192  op1steq  6199  dfoprab4  6212  f1od2  6255  reldmtpos  6273  smores3  6313  smores2  6314  ctssdccl  7135  pinn  7333  indpi  7366  enq0enq  7455  preqlu  7496  elinp  7498  prop  7499  elnp1st2nd  7500  prarloclem5  7524  cauappcvgprlemladd  7682  peano5nnnn  7916  nnindnn  7917  recn  7969  rexr  8028  peano5nni  8947  nnre  8951  nncn  8952  nnind  8960  nnnn0  9208  nn0re  9210  nn0cn  9211  nn0xnn0  9268  nnz  9297  nn0z  9298  nnq  9658  qcn  9659  rpre  9685  iccshftri  10020  iccshftli  10022  iccdili  10024  icccntri  10026  fzval2  10036  fzelp1  10099  4fvwrd4  10165  elfzo1  10215  expcllem  10557  expcl2lemap  10558  m1expcl2  10568  bcm1k  10767  bcpasc  10773  cau3lem  11150  climconst2  11326  fsum3  11422  binomlem  11518  fprodge1  11674  cos12dec  11802  dvdsflip  11884  infssuzcldc  11979  isprm3  12145  phimullem  12252  prmdiveq  12263  structcnvcnv  12523  fvsetsid  12541  ptex  12762  nmzsubg  13142  nmznsg  13145  nzrring  13526  lringnzr  13533  rege0subm  13880  tgval2  13988  qtopbasss  14458  dedekindicc  14548  ivthinc  14558  ivthdec  14559  cosz12  14638  cos0pilt1  14710  ioocosf1o  14712  exmidsbthrlem  15209