Theorem inss2 2227

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 2204	. 2 |- (B i^i A) = (A i^i B)
2		inss1 2226	. 2 |- (B i^i A) (_ B
3	1, 2	eqsstr3 2088	1 |- (A i^i B) (_ B

Syntax hints:   i^i cin 2042   (_ wss 2043

This theorem is referenced by:  ssin 2228  ordin 2972  onfr 2981  relin2 3258  relres 3379  intasym 3430  asymref 3431  intirr 3433  ssrnres 3473  cnvcnv 3478  fnresin2 3594  ssimaex 3759  exfo 3813  bnd2 4704  brdom3 4781  brdom5 4782  brdom4 4783  ltrelpi 4997  limsupclt 6470  clm4le 7027  clm4f 7028  clm0 7029  clm4at 7036  climfnn 7038  climconst 7039  2climnn 7047  2climnn0 7048  ser1f0 7114  metres 7775  caussi 7905  bcthlem18 7966  minveceu 8527  occllem6 9117  projlem25 9149  projlem26 9150  chdmm1 9338  chm0 9351  ledi 9397  lejdi 9399  pjoml2 9468  pjoml4 9470  cmcmlem 9474  cmbr4 9484  osumcor 9527  pjssm 9566  mayete3 9613  riesz4t 9935  riesz1t 9936  cnlnadjeut 9949  nmopadjle 9959  pjclem1 10061  pjc 10066  mdbr3 10162  mdbr4 10163  dmdbr2 10168  ssmd2 10176  mdslj1 10183  mdslj2 10184  mdsl1 10185  mdsl2b 10187  mdslmd1lem1 10189  mdslmd1lem2 10190  mdslmd2 10194  csmdsym 10198  cvexchlem 10232  atoml 10246  atcvat4 10261  subsp 10465

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-in 2047  df-ss 2049

Copyright terms: Public domain