Theorem inss2 3426

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 3397	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 3425	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstrri 3258	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

Syntax hints:   ∩ cin 3197   ⊆ wss 3198

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 2802  df-in 3204  df-ss 3211

This theorem is referenced by:  difin0  3566  bnd2  4259  ordin  4478  relin2  4842  relres  5037  ssrnres  5175  cnvcnv  5185  funinsn  5374  funimaexg  5409  fnresin2  5443  ssimaex  5701  ffvresb  5804  fnfvimad  5883  ofrfval  6237  ofvalg  6238  ofrval  6239  off  6241  ofres  6243  ofco  6247  offres  6290  tpostpos  6423  smores3  6452  tfrlem5  6473  tfrexlem  6493  erinxp  6771  pmresg  6838  unfiin  7109  ltrelpi  7532  peano5nnnn  8100  peano5nni  9134  rexanuz  11536  bitsinv1  12510  structcnvcnv  13085  ressbasssd  13139  restsspw  13319  eltg4i  14766  ntrss2  14832  ntrin  14835  isopn3  14836  resttopon  14882  restuni2  14888  cnrest2r  14948  cnptopresti  14949  cnptoprest  14950  lmss  14957  metrest  15217  tgioo  15265  2sqlem8  15839  2sqlem9  15840  peano5set  16445