Theorem inss2 3221

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 3192	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 3220	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstr3i 3057	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

Syntax hints:   ∩ cin 2998   ⊆ wss 2999

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-v 2621  df-in 3005  df-ss 3012

This theorem is referenced by:  difin0  3356  bnd2  4008  ordin  4212  relin2  4556  relres  4741  ssrnres  4873  cnvcnv  4883  funinsn  5063  funimaexg  5098  fnresin2  5129  ssimaex  5365  ffvresb  5461  ofrfval  5864  fnofval  5865  ofrval  5866  off  5868  ofres  5869  ofco  5873  offres  5906  tpostpos  6029  smores3  6058  tfrlem5  6079  tfrexlem  6099  erinxp  6366  pmresg  6433  unfiin  6636  ltrelpi  6883  peano5nnnn  7427  peano5nni  8425  rexanuz  10421  structcnvcnv  11510  peano5set  11835