Theorem inss2 2234

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 2211	. 2 |- (B i^i A) = (A i^i B)
2		inss1 2233	. 2 |- (B i^i A) (_ B
3	1, 2	eqsstr3 2095	1 |- (A i^i B) (_ B

Syntax hints:   i^i cin 2049   (_ wss 2050

This theorem is referenced by:  ssin 2235  ordin 2983  onfr 2992  relin2 3269  relres 3393  intasym 3444  asymref 3445  intirr 3447  ssrnres 3487  cnvcnv 3492  fnresin2 3608  ssimaex 3774  exfo 3828  bnd2 4734  brdom3 4811  brdom5 4812  brdom4 4813  ltrelpi 5029  limsupclt 6531  clm4le 7081  clm4f 7082  clm0 7083  clm4at 7090  climfnn 7092  climconst 7094  2climnn 7102  2climnn0 7103  ser1f0 7170  metres 7820  caussi 7951  bcthlem18 8013  minveceu 8579  occllem6 9173  projlem25 9205  projlem26 9206  chdmm1 9395  chm0 9408  ledi 9454  lejdi 9456  pjoml2 9523  pjoml4 9525  cmcmlem 9529  cmbr4 9539  osumcor 9582  pjssm 9621  mayete3 9668  riesz4t 9992  riesz1t 9993  cnlnadjeut 10006  nmopadjle 10016  pjclem1 10118  pjc 10123  mdbr3 10219  mdbr4 10220  dmdbr2 10225  dmdbr5 10230  ssmd2 10234  mdslj1 10241  mdslj2 10242  mdsl1 10243  mdsl2b 10245  mdslmd1lem1 10247  mdslmd1lem2 10248  mdslmd2 10252  csmdsym 10256  cvexchlem 10290  atoml 10304  atcvat4 10319  subsp 10540

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