Theorem sseli 3188

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

Syntax hints:   → wi 4   ∈ wcel 2175   ⊆ wss 3165

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-in 3171  df-ss 3178

This theorem is referenced by:  sselii  3189  sselid  3190  elun1  3339  elun2  3340  finds  4647  finds2  4648  issref  5064  2elresin  5386  fvun1  5644  fvmptssdm  5663  elfvmptrab1  5673  fvimacnvi  5693  elpreima  5698  ofrfval  6166  ofvalg  6167  off  6170  offres  6219  eqopi  6257  op1steq  6264  dfoprab4  6277  f1od2  6320  reldmtpos  6338  smores3  6378  smores2  6379  ctssdccl  7212  pinn  7421  indpi  7454  enq0enq  7543  preqlu  7584  elinp  7586  prop  7587  elnp1st2nd  7588  prarloclem5  7612  cauappcvgprlemladd  7770  peano5nnnn  8004  nnindnn  8005  recn  8057  rexr  8117  peano5nni  9038  nnre  9042  nncn  9043  nnind  9051  nnnn0  9301  nn0re  9303  nn0cn  9304  nn0xnn0  9361  nnz  9390  nn0z  9391  nnq  9753  qcn  9754  rpre  9781  iccshftri  10116  iccshftli  10118  iccdili  10120  icccntri  10122  fzval2  10132  fzelp1  10195  4fvwrd4  10261  elfzo1  10312  infssuzcldc  10376  expcllem  10693  expcl2lemap  10694  m1expcl2  10704  bcm1k  10903  bcpasc  10909  wrdv  11008  ccatclab  11048  cau3lem  11367  climconst2  11544  fsum3  11640  binomlem  11736  fprodge1  11892  cos12dec  12021  dvdsflip  12104  isprm3  12382  phimullem  12489  prmdiveq  12500  structcnvcnv  12790  fvsetsid  12808  ptex  13038  nmzsubg  13488  nmznsg  13491  nzrring  13887  lringnzr  13897  rege0subm  14288  znrrg  14364  tgval2  14465  qtopbasss  14935  dedekindicc  15047  ivthinc  15057  ivthdec  15058  dvply2  15181  cosz12  15194  cos0pilt1  15266  ioocosf1o  15268  mpodvdsmulf1o  15404  fsumdvdsmul  15405  lgsquadlemofi  15495  lgsquadlem1  15496  lgsquadlem2  15497  exmidsbthrlem  15894