Theorem sseli 3188

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

Syntax hints:   → wi 4   ∈ wcel 2175   ⊆ wss 3165

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-in 3171  df-ss 3178

This theorem is referenced by:  sselii  3189  sselid  3190  elun1  3339  elun2  3340  finds  4646  finds2  4647  issref  5062  2elresin  5381  fvun1  5639  fvmptssdm  5658  elfvmptrab1  5668  fvimacnvi  5688  elpreima  5693  ofrfval  6157  ofvalg  6158  off  6161  offres  6210  eqopi  6248  op1steq  6255  dfoprab4  6268  f1od2  6311  reldmtpos  6329  smores3  6369  smores2  6370  ctssdccl  7195  pinn  7404  indpi  7437  enq0enq  7526  preqlu  7567  elinp  7569  prop  7570  elnp1st2nd  7571  prarloclem5  7595  cauappcvgprlemladd  7753  peano5nnnn  7987  nnindnn  7988  recn  8040  rexr  8100  peano5nni  9021  nnre  9025  nncn  9026  nnind  9034  nnnn0  9284  nn0re  9286  nn0cn  9287  nn0xnn0  9344  nnz  9373  nn0z  9374  nnq  9736  qcn  9737  rpre  9764  iccshftri  10099  iccshftli  10101  iccdili  10103  icccntri  10105  fzval2  10115  fzelp1  10178  4fvwrd4  10244  elfzo1  10295  infssuzcldc  10359  expcllem  10676  expcl2lemap  10677  m1expcl2  10687  bcm1k  10886  bcpasc  10892  wrdv  10985  ccatclab  11025  cau3lem  11344  climconst2  11521  fsum3  11617  binomlem  11713  fprodge1  11869  cos12dec  11998  dvdsflip  12081  isprm3  12359  phimullem  12466  prmdiveq  12477  structcnvcnv  12767  fvsetsid  12785  ptex  13014  nmzsubg  13464  nmznsg  13467  nzrring  13863  lringnzr  13873  rege0subm  14264  znrrg  14340  tgval2  14441  qtopbasss  14911  dedekindicc  15023  ivthinc  15033  ivthdec  15034  dvply2  15157  cosz12  15170  cos0pilt1  15242  ioocosf1o  15244  mpodvdsmulf1o  15380  fsumdvdsmul  15381  lgsquadlemofi  15471  lgsquadlem1  15472  lgsquadlem2  15473  exmidsbthrlem  15825