Theorem inss2 3348

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 3319	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 3347	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstrri 3180	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

Syntax hints:   ∩ cin 3120   ⊆ wss 3121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-in 3127  df-ss 3134

This theorem is referenced by:  difin0  3487  bnd2  4157  ordin  4368  relin2  4728  relres  4917  ssrnres  5051  cnvcnv  5061  funinsn  5245  funimaexg  5280  fnresin2  5311  ssimaex  5555  ffvresb  5657  ofrfval  6067  ofvalg  6068  ofrval  6069  off  6071  ofres  6073  ofco  6077  offres  6112  tpostpos  6241  smores3  6270  tfrlem5  6291  tfrexlem  6311  erinxp  6584  pmresg  6651  unfiin  6900  ltrelpi  7275  peano5nnnn  7843  peano5nni  8870  rexanuz  10941  structcnvcnv  12421  restsspw  12578  eltg4i  12810  ntrss2  12876  ntrin  12879  isopn3  12880  resttopon  12926  restuni2  12932  cnrest2r  12992  cnptopresti  12993  cnptoprest  12994  lmss  13001  metrest  13261  tgioo  13301  2sqlem8  13714  2sqlem9  13715  peano5set  13937