Theorem inss1 2233

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 2210	. . 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 2072	1 |- (A i^i B) (_ A

Syntax hints:   e. wcel 960   i^i cin 2049   (_ wss 2050

This theorem is referenced by:  inss2 2234  ssin 2235  ssinss1 2240  unabs 2241  nssinpss 2243  dfin4 2251  inv1 2303  difdisj 2341  wefrc 2949  ordtri3or 2985  onfr 2992  relin1 3268  resss 3389  cnvcnvss 3494  funimass2 3579  fnresin1 3607  ssimaex 3774  sbthlem7 4459  zfregs 4657  brdom3 4811  brdom5 4812  brdom4 4813  imadomg 4816  tgval2t 7616  unitgt 7622  cnsscnp 7769  bcthlem14 8009  bcthlem16 8011  phnv 8469  minveceu 8579  minvecle 8582  chm1 9374  chdmm1 9395  chabs1t 9434  chabs2t 9435  ledi 9454  lejdi 9456  pjoml4 9525  cmbr3 9538  cmbr4 9539  cmm1 9544  osumcor2 9585  3oalem4 9605  pjssm 9621  pjocin 9638  pjin 9639  mayete3 9668  riesz4t 9992  riesz1t 9993  cnlnadjeu 10005  cnlnadjeut 10006  cnlnssadj 10008  nmopadjle 10016  pjin1 10115  pjclem1 10118  stji1 10164  stm1 10165  dmdbr2 10225  ssmd1 10233  mdslj2 10242  mdsl2b 10245  mdslmd1lem1 10247  mdslmd2 10252  atoml 10304  atcvat4 10319  sumdmdlem2 10341  dmdbr5at 10344  dmdbr6at 10345  dmdbr7at 10346

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-in 2054  df-ss 2056

Copyright terms: Public domain