Theorem inss2 3380

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	|- ( A i^i B ) C_ B

Proof of Theorem inss2

Step	Hyp	Ref	Expression
1		incom 3351	. 2 |- ( B i^i A ) = ( A i^i B )
2		inss1 3379	. 2 |- ( B i^i A ) C_ B
3	1, 2	eqsstrri 3212	1 |- ( A i^i B ) C_ B

Syntax hints:   i^i cin 3152   C_ wss 3153

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-in 3159  df-ss 3166

This theorem is referenced by:  difin0  3520  bnd2  4202  ordin  4416  relin2  4778  relres  4970  ssrnres  5108  cnvcnv  5118  funinsn  5303  funimaexg  5338  fnresin2  5369  ssimaex  5618  ffvresb  5721  ofrfval  6139  ofvalg  6140  ofrval  6141  off  6143  ofres  6145  ofco  6149  offres  6187  tpostpos  6317  smores3  6346  tfrlem5  6367  tfrexlem  6387  erinxp  6663  pmresg  6730  unfiin  6982  ltrelpi  7384  peano5nnnn  7952  peano5nni  8985  rexanuz  11132  structcnvcnv  12634  ressbasssd  12687  restsspw  12860  eltg4i  14223  ntrss2  14289  ntrin  14292  isopn3  14293  resttopon  14339  restuni2  14345  cnrest2r  14405  cnptopresti  14406  cnptoprest  14407  lmss  14414  metrest  14674  tgioo  14714  2sqlem8  15210  2sqlem9  15211  peano5set  15432