Theorem inss1 3379

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

Proof of Theorem inss1

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elin 3342	. . 3 |- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
2	1	simplbi 274	. 2 |- ( x e. ( A i^i B ) -> x e. A )
3	2	ssriv 3183	1 |- ( A i^i B ) C_ A

Syntax hints:   e. wcel 2164   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:  inss2  3380  ssinss1  3388  unabs  3390  inssddif  3400  inv1  3483  disjdif  3519  inundifss  3524  relin1  4777  resss  4966  resmpt3  4991  cnvcnvss  5120  funin  5325  funimass2  5332  fnresin1  5368  fnres  5370  fresin  5432  ssimaex  5618  fneqeql2  5667  isoini2  5862  ofrfval  6139  ofvalg  6140  ofrval  6141  off  6143  ofres  6145  ofco  6149  smores  6345  smores2  6347  tfrlem5  6367  pmresg  6730  unfiin  6982  infidc  6993  sbthlem7  7022  peano5nnnn  7952  peano5nni  8985  rexanuz  11132  nninfdclemcl  12605  nninfdclemp1  12607  fvsetsid  12652  tgvalex  12874  tgval2  14219  eltg3  14225  tgcl  14232  tgdom  14240  tgidm  14242  epttop  14258  ntropn  14285  ntrin  14292  cnptopresti  14406  cnptoprest  14407  txcnmpt  14441  xmetres  14550  metres  14551  blin2  14600  metrest  14674  tgioo  14714  limcresi  14820  2sqlem8  15210  bj-charfun  15299  bj-charfundc  15300  bj-charfundcALT  15301