Theorem sseli 3244

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209   ⊆ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  sselii  3245  sselid  3246  elun1  3396  elun2  3397  elopabr  4425  elopabran  4426  finds  4747  finds2  4748  issref  5170  2elresin  5494  fvun1  5769  fvmptssdm  5790  elfvmptrab1  5801  fvopab4ndm  5803  fvimacnvi  5823  elpreima  5828  ofrfval  6311  ofvalg  6312  off  6315  offres  6368  eqopi  6406  op1steq  6413  dfoprab4  6426  f1od2  6471  reldmtpos  6524  smores3  6564  smores2  6565  ctssdccl  7452  pinn  7677  indpi  7710  enq0enq  7799  preqlu  7840  elinp  7842  prop  7843  elnp1st2nd  7844  prarloclem5  7868  cauappcvgprlemladd  8026  peano5nnnn  8260  nnindnn  8261  recn  8313  rexr  8372  peano5nni  9310  nnre  9314  nncn  9315  nnind  9323  nnnn0  9575  nn0re  9577  nn0cn  9578  nn0xnn0  9639  nnz  9668  nn0z  9669  uzuzle35  9975  nnq  10043  qcn  10044  rpre  10072  iccshftri  10408  iccshftli  10410  iccdili  10412  icccntri  10414  fzval2  10425  fzelp1  10492  4fvwrd4  10558  elfzo1  10614  infssuzcldc  10679  expcllem  11002  expcl2lemap  11003  m1expcl2  11013  bcm1k  11214  bcpasc  11220  hashfibclem  11298  wrdv  11336  ccatclab  11378  pfxfv0  11480  pfxfvlsw  11483  cau3lem  11897  climconst2  12076  fsum3  12173  binomlem  12269  fprodge1  12425  cos12dec  12554  dvdsflip  12637  isprm3  12915  phimullem  13026  prmdiveq  13037  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemfmpn  13286  ballotfilemodife  13292  ballotfilemfrceq  13324  structcnvcnv  13420  fvsetsid  13438  ptex  13671  nmzsubg  14066  nmznsg  14069  cntzm  14155  cntzmhm  14167  nzrring  14574  lringnzr  14584  rege0subm  15005  znrrg  15079  psrbagconf1o  15149  tgval2  15243  qtopbasss  15713  dedekindicc  15825  ivthinc  15835  ivthdec  15836  dvply2  15959  cosz12  15973  cos0pilt1  16045  ioocosf1o  16047  mpodvdsmulf1o  16245  fsumdvdsmul  16246  lgsquadlemofi  16361  lgsquadlem1  16362  lgsquadlem2  16363  wlk1walkdom  16766  exmidsbthrlem  17233