Theorem inss2 3430

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 3401	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 3429	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstrri 3261	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

Syntax hints:   ∩ cin 3200   ⊆ wss 3201

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-in 3207  df-ss 3214

This theorem is referenced by:  difin0  3570  bnd2  4269  ordin  4488  relin2  4852  relres  5047  ssrnres  5186  cnvcnv  5196  funinsn  5386  funimaexg  5421  fnresin2  5455  ssimaex  5716  ffvresb  5818  fnfvimad  5900  ofrfval  6253  ofvalg  6254  ofrval  6255  off  6257  ofres  6259  ofco  6263  offres  6306  tpostpos  6473  smores3  6502  tfrlem5  6523  tfrexlem  6543  erinxp  6821  pmresg  6888  unfiin  7161  ltrelpi  7587  peano5nnnn  8155  peano5nni  9188  rexanuz  11611  bitsinv1  12586  structcnvcnv  13161  ressbasssd  13215  restsspw  13395  eltg4i  14849  ntrss2  14915  ntrin  14918  isopn3  14919  resttopon  14965  restuni2  14971  cnrest2r  15031  cnptopresti  15032  cnptoprest  15033  lmss  15040  metrest  15300  tgioo  15348  2sqlem8  15925  2sqlem9  15926  peano5set  16639