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  4370  elopabran  4371  finds  4691  finds2  4692  issref  5110  2elresin  5433  fvun1  5699  fvmptssdm  5718  elfvmptrab1  5728  fvimacnvi  5748  elpreima  5753  ofrfval  6225  ofvalg  6226  off  6229  offres  6278  eqopi  6316  op1steq  6323  dfoprab4  6336  f1od2  6379  reldmtpos  6397  smores3  6437  smores2  6438  ctssdccl  7274  pinn  7492  indpi  7525  enq0enq  7614  preqlu  7655  elinp  7657  prop  7658  elnp1st2nd  7659  prarloclem5  7683  cauappcvgprlemladd  7841  peano5nnnn  8075  nnindnn  8076  recn  8128  rexr  8188  peano5nni  9109  nnre  9113  nncn  9114  nnind  9122  nnnn0  9372  nn0re  9374  nn0cn  9375  nn0xnn0  9432  nnz  9461  nn0z  9462  nnq  9824  qcn  9825  rpre  9852  iccshftri  10187  iccshftli  10189  iccdili  10191  icccntri  10193  fzval2  10203  fzelp1  10266  4fvwrd4  10332  elfzo1  10386  infssuzcldc  10450  expcllem  10767  expcl2lemap  10768  m1expcl2  10778  bcm1k  10977  bcpasc  10983  wrdv  11082  ccatclab  11124  pfxfv0  11219  pfxfvlsw  11222  cau3lem  11620  climconst2  11797  fsum3  11893  binomlem  11989  fprodge1  12145  cos12dec  12274  dvdsflip  12357  isprm3  12635  phimullem  12742  prmdiveq  12753  structcnvcnv  13043  fvsetsid  13061  ptex  13292  nmzsubg  13742  nmznsg  13745  nzrring  14141  lringnzr  14151  rege0subm  14542  znrrg  14618  tgval2  14719  qtopbasss  15189  dedekindicc  15301  ivthinc  15311  ivthdec  15312  dvply2  15435  cosz12  15448  cos0pilt1  15520  ioocosf1o  15522  mpodvdsmulf1o  15658  fsumdvdsmul  15659  lgsquadlemofi  15749  lgsquadlem1  15750  lgsquadlem2  15751  exmidsbthrlem  16349