Theorem sseli 3022

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

Syntax hints:   → wi 4   ∈ wcel 1439   ⊆ wss 3000

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-11 1443  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-in 3006  df-ss 3013

This theorem is referenced by:  sselii  3023  sseldi  3024  elun1  3168  elun2  3169  finds  4428  finds2  4429  issref  4827  2elresin  5138  fvun1  5383  fvmptssdm  5400  fvimacnvi  5427  elpreima  5432  ofrfval  5878  fnofval  5879  off  5882  offres  5920  eqopi  5956  op1steq  5963  dfoprab4  5976  f1od2  6014  reldmtpos  6032  smores3  6072  smores2  6073  pinn  6929  indpi  6962  enq0enq  7051  preqlu  7092  elinp  7094  prop  7095  elnp1st2nd  7096  prarloclem5  7120  cauappcvgprlemladd  7278  peano5nnnn  7488  nnindnn  7489  recn  7536  rexr  7594  peano5nni  8486  nnre  8490  nncn  8491  nnind  8499  nnnn0  8741  nn0re  8743  nn0cn  8744  nn0xnn0  8801  nnz  8830  nn0z  8831  nnq  9179  qcn  9180  rpre  9201  iccshftri  9473  iccshftli  9475  iccdili  9477  icccntri  9479  fzval2  9488  fzelp1  9549  4fvwrd4  9612  elfzo1  9662  expcllem  10027  expcl2lemap  10028  m1expcl2  10038  bcm1k  10229  bcpasc  10235  cau3lem  10608  climconst2  10740  fisum  10839  binomlem  10938  dvdsflip  11191  infssuzcldc  11286  isprm3  11439  phimullem  11540  structcnvcnv  11571  fvsetsid  11589  tgval2  11812  exmidsbthrlem  12184