Theorem inss2 3425

Description: The intersection of two classes is a subset of one of them. Part of Exercise 12 of [TakeutiZaring] p. 18. (Contributed by NM, 27-Apr-1994.)

Assertion

Ref	Expression
inss2	⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

Proof of Theorem inss2

Step	Hyp	Ref	Expression
1		incom 3396	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 3424	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstrri 3257	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

Syntax hints:   ∩ cin 3196   ⊆ wss 3197

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-in 3203  df-ss 3210

This theorem is referenced by:  difin0  3565  bnd2  4256  ordin  4475  relin2  4837  relres  5032  ssrnres  5170  cnvcnv  5180  funinsn  5369  funimaexg  5404  fnresin2  5438  ssimaex  5694  ffvresb  5797  ofrfval  6225  ofvalg  6226  ofrval  6227  off  6229  ofres  6231  ofco  6235  offres  6278  tpostpos  6408  smores3  6437  tfrlem5  6458  tfrexlem  6478  erinxp  6754  pmresg  6821  unfiin  7084  ltrelpi  7507  peano5nnnn  8075  peano5nni  9109  rexanuz  11494  bitsinv1  12468  structcnvcnv  13043  ressbasssd  13097  restsspw  13277  eltg4i  14723  ntrss2  14789  ntrin  14792  isopn3  14793  resttopon  14839  restuni2  14845  cnrest2r  14905  cnptopresti  14906  cnptoprest  14907  lmss  14914  metrest  15174  tgioo  15222  2sqlem8  15796  2sqlem9  15797  peano5set  16261