Theorem sseli 3180

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 3178	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2167   ⊆ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  sselii  3181  sselid  3182  elun1  3331  elun2  3332  finds  4637  finds2  4638  issref  5053  2elresin  5372  fvun1  5630  fvmptssdm  5649  elfvmptrab1  5659  fvimacnvi  5679  elpreima  5684  ofrfval  6148  ofvalg  6149  off  6152  offres  6201  eqopi  6239  op1steq  6246  dfoprab4  6259  f1od2  6302  reldmtpos  6320  smores3  6360  smores2  6361  ctssdccl  7186  pinn  7395  indpi  7428  enq0enq  7517  preqlu  7558  elinp  7560  prop  7561  elnp1st2nd  7562  prarloclem5  7586  cauappcvgprlemladd  7744  peano5nnnn  7978  nnindnn  7979  recn  8031  rexr  8091  peano5nni  9012  nnre  9016  nncn  9017  nnind  9025  nnnn0  9275  nn0re  9277  nn0cn  9278  nn0xnn0  9335  nnz  9364  nn0z  9365  nnq  9726  qcn  9727  rpre  9754  iccshftri  10089  iccshftli  10091  iccdili  10093  icccntri  10095  fzval2  10105  fzelp1  10168  4fvwrd4  10234  elfzo1  10285  infssuzcldc  10344  expcllem  10661  expcl2lemap  10662  m1expcl2  10672  bcm1k  10871  bcpasc  10877  wrdv  10970  cau3lem  11298  climconst2  11475  fsum3  11571  binomlem  11667  fprodge1  11823  cos12dec  11952  dvdsflip  12035  isprm3  12313  phimullem  12420  prmdiveq  12431  structcnvcnv  12721  fvsetsid  12739  ptex  12968  nmzsubg  13418  nmznsg  13421  nzrring  13817  lringnzr  13827  rege0subm  14218  znrrg  14294  tgval2  14395  qtopbasss  14865  dedekindicc  14977  ivthinc  14987  ivthdec  14988  dvply2  15111  cosz12  15124  cos0pilt1  15196  ioocosf1o  15198  mpodvdsmulf1o  15334  fsumdvdsmul  15335  lgsquadlemofi  15425  lgsquadlem1  15426  lgsquadlem2  15427  exmidsbthrlem  15779