Theorem sseli 2995

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

Syntax hints:   → wi 4   ∈ wcel 1433   ⊆ wss 2973

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-11 1437  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-in 2979  df-ss 2986

This theorem is referenced by:  sselii  2996  sseldi  2997  elun1  3139  elun2  3140  finds  4341  finds2  4342  issref  4727  2elresin  5030  fvun1  5260  fvmptssdm  5276  fvimacnvi  5302  elpreima  5307  ofrfval  5740  fnofval  5741  off  5744  offres  5782  eqopi  5818  op1steq  5825  dfoprab4  5838  f1od2  5876  reldmtpos  5891  smores3  5931  smores2  5932  pinn  6499  indpi  6532  enq0enq  6621  preqlu  6662  elinp  6664  prop  6665  elnp1st2nd  6666  prarloclem5  6690  cauappcvgprlemladd  6848  peano5nnnn  7058  nnindnn  7059  recn  7106  rexr  7164  peano5nni  8042  nnre  8046  nncn  8047  nnind  8055  nnnn0  8295  nn0re  8297  nn0cn  8298  nnz  8370  nn0z  8371  nnq  8718  qcn  8719  rpre  8740  iccshftri  9017  iccshftli  9019  iccdili  9021  icccntri  9023  fzval2  9032  fzelp1  9091  4fvwrd4  9150  elfzo1  9199  expcllem  9487  expcl2lemap  9488  m1expcl2  9498  bcm1k  9687  bcpasc  9693  cau3lem  10000  climconst2  10130  dvdsflip  10251  infssuzcldc  10347  isprm3  10500