Theorem inss2 2231

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

Assertion

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

Proof of Theorem inss2

Step	Hyp	Ref	Expression
1		incom 2208	. 2 |- (B i^i A) = (A i^i B)
2		inss1 2230	. 2 |- (B i^i A) (_ B
3	1, 2	eqsstr3 2092	1 |- (A i^i B) (_ B

Syntax hints:   i^i cin 2046   (_ wss 2047

This theorem is referenced by:  ssin 2232  ordin 2977  onfr 2986  relin2 3263  relres 3387  intasym 3438  asymref 3439  intirr 3441  ssrnres 3481  cnvcnv 3486  fnresin2 3602  ssimaex 3768  exfo 3822  bnd2 4724  brdom3 4801  brdom5 4802  brdom4 4803  ltrelpi 5017  limsupclt 6530  clm4le 7081  clm4f 7082  clm0 7083  clm4at 7090  climfnn 7092  climconst 7094  2climnn 7102  2climnn0 7103  ser1f0 7170  metres 7823  caussi 7954  bcthlem18 8016  minveceu 8583  occllem6 9178  projlem25 9210  projlem26 9211  chdmm1 9400  chm0 9413  ledi 9459  lejdi 9461  pjoml2 9528  pjoml4 9530  cmcmlem 9534  cmbr4 9544  osumcor 9587  pjssm 9626  mayete3 9673  riesz4t 9997  riesz1t 9998  cnlnadjeut 10011  nmopadjle 10021  pjclem1 10123  pjc 10128  mdbr3 10224  mdbr4 10225  dmdbr2 10230  dmdbr5 10235  ssmd2 10239  mdslj1 10246  mdslj2 10247  mdsl1 10248  mdsl2b 10250  mdslmd1lem1 10252  mdslmd1lem2 10253  mdslmd2 10257  csmdsym 10261  cvexchlem 10295  atoml 10309  atcvat4 10324  subsp 10554

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