Theorem sseli 3220

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

Syntax hints:   → wi 4   ∈ wcel 2200   ⊆ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  sselii  3221  sselid  3222  elun1  3371  elun2  3372  elopabr  4371  elopabran  4372  finds  4692  finds2  4693  issref  5111  2elresin  5434  fvun1  5702  fvmptssdm  5721  elfvmptrab1  5731  fvimacnvi  5751  elpreima  5756  ofrfval  6233  ofvalg  6234  off  6237  offres  6286  eqopi  6324  op1steq  6331  dfoprab4  6344  f1od2  6387  reldmtpos  6405  smores3  6445  smores2  6446  ctssdccl  7289  pinn  7507  indpi  7540  enq0enq  7629  preqlu  7670  elinp  7672  prop  7673  elnp1st2nd  7674  prarloclem5  7698  cauappcvgprlemladd  7856  peano5nnnn  8090  nnindnn  8091  recn  8143  rexr  8203  peano5nni  9124  nnre  9128  nncn  9129  nnind  9137  nnnn0  9387  nn0re  9389  nn0cn  9390  nn0xnn0  9447  nnz  9476  nn0z  9477  nnq  9840  qcn  9841  rpre  9868  iccshftri  10203  iccshftli  10205  iccdili  10207  icccntri  10209  fzval2  10219  fzelp1  10282  4fvwrd4  10348  elfzo1  10403  infssuzcldc  10467  expcllem  10784  expcl2lemap  10785  m1expcl2  10795  bcm1k  10994  bcpasc  11000  wrdv  11100  ccatclab  11142  pfxfv0  11239  pfxfvlsw  11242  cau3lem  11640  climconst2  11817  fsum3  11913  binomlem  12009  fprodge1  12165  cos12dec  12294  dvdsflip  12377  isprm3  12655  phimullem  12762  prmdiveq  12773  structcnvcnv  13063  fvsetsid  13081  ptex  13312  nmzsubg  13762  nmznsg  13765  nzrring  14162  lringnzr  14172  rege0subm  14563  znrrg  14639  tgval2  14740  qtopbasss  15210  dedekindicc  15322  ivthinc  15332  ivthdec  15333  dvply2  15456  cosz12  15469  cos0pilt1  15541  ioocosf1o  15543  mpodvdsmulf1o  15679  fsumdvdsmul  15680  lgsquadlemofi  15770  lgsquadlem1  15771  lgsquadlem2  15772  wlk1walkdom  16100  exmidsbthrlem  16450