Theorem inss1 2230

Description: The intersection of two classes is a subset of one of them. Part of Exercise 12 of [TakeutiZaring] p. 18.

Assertion

Ref	Expression
inss1	|- (A i^i B) (_ A

Proof of Theorem inss1

Step	Hyp	Ref	Expression
1		elin 2207	. . 3 |- (x e. (A i^i B) <-> (x e. A /\ x e. B))
2	1	pm3.26bi 322	. 2 |- (x e. (A i^i B) -> x e. A)
3	2	ssriv 2069	1 |- (A i^i B) (_ A

Syntax hints:   e. wcel 958   i^i cin 2046   (_ wss 2047

This theorem is referenced by:  inss2 2231  ssin 2232  ssinss1 2237  unabs 2238  nssinpss 2240  dfin4 2248  inv1 2299  difdisj 2337  wefrc 2943  ordtri3or 2979  onfr 2986  relin1 3262  resss 3383  cnvcnvss 3488  funimass2 3573  fnresin1 3601  ssimaex 3768  sbthlem7 4453  zfregs 4647  brdom3 4801  brdom5 4802  brdom4 4803  imadomg 4806  tgval2t 7617  unitgt 7623  cnsscnp 7772  bcthlem14 8012  bcthlem16 8014  phnv 8473  minveceu 8583  minvecle 8586  chm1 9379  chdmm1 9400  chabs1t 9439  chabs2t 9440  ledi 9459  lejdi 9461  pjoml4 9530  cmbr3 9543  cmbr4 9544  cmm1 9549  osumcor2 9590  3oalem4 9610  pjssm 9626  pjocin 9643  pjin 9644  mayete3 9673  riesz4t 9997  riesz1t 9998  cnlnadjeu 10010  cnlnadjeut 10011  cnlnssadj 10013  nmopadjle 10021  pjin1 10120  pjclem1 10123  stji1 10169  stm1 10170  dmdbr2 10230  ssmd1 10238  mdslj2 10247  mdsl2b 10250  mdslmd1lem1 10252  mdslmd2 10257  atoml 10309  atcvat4 10324  sumdmdlem2 10346  dmdbr5at 10349  dmdbr6at 10350  dmdbr7at 10351

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-in 2051  df-ss 2053

Copyright terms: Public domain