Theorem sseli 3238

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

Syntax hints:   → wi 4   ∈ wcel 2205   ⊆ wss 3214

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227

This theorem is referenced by:  sselii  3239  sselid  3240  elun1  3390  elun2  3391  elopabr  4406  elopabran  4407  finds  4727  finds2  4728  issref  5150  2elresin  5474  fvun1  5748  fvmptssdm  5767  elfvmptrab1  5777  fvimacnvi  5797  elpreima  5802  ofrfval  6284  ofvalg  6285  off  6288  offres  6341  eqopi  6379  op1steq  6386  dfoprab4  6399  f1od2  6444  reldmtpos  6497  smores3  6537  smores2  6538  ctssdccl  7415  pinn  7640  indpi  7673  enq0enq  7762  preqlu  7803  elinp  7805  prop  7806  elnp1st2nd  7807  prarloclem5  7831  cauappcvgprlemladd  7989  peano5nnnn  8223  nnindnn  8224  recn  8276  rexr  8335  peano5nni  9257  nnre  9261  nncn  9262  nnind  9270  nnnn0  9520  nn0re  9522  nn0cn  9523  nn0xnn0  9584  nnz  9613  nn0z  9614  uzuzle35  9915  nnq  9983  qcn  9984  rpre  10011  iccshftri  10347  iccshftli  10349  iccdili  10351  icccntri  10353  fzval2  10364  fzelp1  10430  4fvwrd4  10496  elfzo1  10552  infssuzcldc  10617  expcllem  10936  expcl2lemap  10937  m1expcl2  10947  bcm1k  11147  bcpasc  11153  hashfibclem  11231  wrdv  11265  ccatclab  11307  pfxfv0  11409  pfxfvlsw  11412  cau3lem  11824  climconst2  12001  fsum3  12098  binomlem  12194  fprodge1  12350  cos12dec  12479  dvdsflip  12562  isprm3  12840  phimullem  12947  prmdiveq  12958  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemfmpn  13178  ballotfilemodife  13184  ballotfilemfrceq  13216  structcnvcnv  13312  fvsetsid  13330  ptex  13561  nmzsubg  13963  nmznsg  13966  nzrring  14428  lringnzr  14438  rege0subm  14858  znrrg  14934  psrbagconf1o  14954  tgval2  15042  qtopbasss  15512  dedekindicc  15624  ivthinc  15634  ivthdec  15635  dvply2  15758  cosz12  15771  cos0pilt1  15843  ioocosf1o  15845  mpodvdsmulf1o  15984  fsumdvdsmul  15985  lgsquadlemofi  16075  lgsquadlem1  16076  lgsquadlem2  16077  wlk1walkdom  16480  exmidsbthrlem  16928