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  7393  indpi  7426  enq0enq  7515  preqlu  7556  elinp  7558  prop  7559  elnp1st2nd  7560  prarloclem5  7584  cauappcvgprlemladd  7742  peano5nnnn  7976  nnindnn  7977  recn  8029  rexr  8089  peano5nni  9010  nnre  9014  nncn  9015  nnind  9023  nnnn0  9273  nn0re  9275  nn0cn  9276  nn0xnn0  9333  nnz  9362  nn0z  9363  nnq  9724  qcn  9725  rpre  9752  iccshftri  10087  iccshftli  10089  iccdili  10091  icccntri  10093  fzval2  10103  fzelp1  10166  4fvwrd4  10232  elfzo1  10283  infssuzcldc  10342  expcllem  10659  expcl2lemap  10660  m1expcl2  10670  bcm1k  10869  bcpasc  10875  wrdv  10968  cau3lem  11296  climconst2  11473  fsum3  11569  binomlem  11665  fprodge1  11821  cos12dec  11950  dvdsflip  12033  isprm3  12311  phimullem  12418  prmdiveq  12429  structcnvcnv  12719  fvsetsid  12737  ptex  12966  nmzsubg  13416  nmznsg  13419  nzrring  13815  lringnzr  13825  rege0subm  14216  znrrg  14292  tgval2  14371  qtopbasss  14841  dedekindicc  14953  ivthinc  14963  ivthdec  14964  dvply2  15087  cosz12  15100  cos0pilt1  15172  ioocosf1o  15174  mpodvdsmulf1o  15310  fsumdvdsmul  15311  lgsquadlemofi  15401  lgsquadlem1  15402  lgsquadlem2  15403  exmidsbthrlem  15753