Theorem inss1 3370

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	⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴

Proof of Theorem inss1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elin 3333	. . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
2	1	simplbi 274	. 2 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) → 𝑥 ∈ 𝐴)
3	2	ssriv 3174	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴

Syntax hints:   ∈ wcel 2160   ∩ cin 3143   ⊆ wss 3144

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 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-in 3150  df-ss 3157

This theorem is referenced by:  inss2  3371  ssinss1  3379  unabs  3381  inssddif  3391  inv1  3474  disjdif  3510  inundifss  3515  relin1  4762  resss  4949  resmpt3  4974  cnvcnvss  5101  funin  5306  funimass2  5313  fnresin1  5349  fnres  5351  fresin  5413  ssimaex  5598  fneqeql2  5646  isoini2  5841  ofrfval  6116  ofvalg  6117  ofrval  6118  off  6120  ofres  6122  ofco  6126  smores  6318  smores2  6320  tfrlem5  6340  pmresg  6703  unfiin  6955  infidc  6965  sbthlem7  6993  peano5nnnn  7922  peano5nni  8953  rexanuz  11032  nninfdclemcl  12502  nninfdclemp1  12504  fvsetsid  12549  tgvalex  12771  tgval2  14028  eltg3  14034  tgcl  14041  tgdom  14049  tgidm  14051  epttop  14067  ntropn  14094  ntrin  14101  cnptopresti  14215  cnptoprest  14216  txcnmpt  14250  xmetres  14359  metres  14360  blin2  14409  metrest  14483  tgioo  14523  limcresi  14612  2sqlem8  14948  bj-charfun  15037  bj-charfundc  15038  bj-charfundcALT  15039