Theorem inss2 3442

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 3411	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 3441	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstrri 3271	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

Syntax hints:   ∩ cin 3210   ⊆ wss 3211

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 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-in 3217  df-ss 3224

This theorem is referenced by:  difin0  3583  bnd2  4286  ordin  4506  relin2  4871  relres  5066  ssrnres  5205  cnvcnv  5215  funinsn  5405  funimaexg  5440  fnresin2  5474  ssimaex  5738  ffvresb  5840  fnfvimad  5922  ofrfval  6275  ofvalg  6276  ofrval  6277  off  6279  ofres  6281  ofco  6285  offres  6328  tpostpos  6495  smores3  6524  tfrlem5  6545  tfrexlem  6565  erinxp  6843  pmresg  6910  unfiin  7186  ltrelpi  7639  peano5nnnn  8207  peano5nni  9240  rexanuz  11673  bitsinv1  12648  structcnvcnv  13228  ressbasssd  13282  restsspw  13462  eltg4i  14920  ntrss2  14986  ntrin  14989  isopn3  14990  resttopon  15036  restuni2  15042  cnrest2r  15102  cnptopresti  15103  cnptoprest  15104  lmss  15111  metrest  15371  tgioo  15419  2sqlem8  15996  2sqlem9  15997  peano5set  16710