Theorem inss1 1657

Description: The intersection of two classes is a subset of one of them. Part of Exercise 12 of [TakeutiZaring] p. 18.

Assertion

Ref	Expression
inss1	⊢ (A ∩ B) ⊆ A

Proof of Theorem inss1

Step	Hyp	Ref	Expression
1		elin 1635	. . 3 ⊢ (x ∈ (A ∩ B) ↔ (x ∈ A ∧ x ∈ B))
2	1	pm3.26bd 259	. 2 ⊢ (x ∈ (A ∩ B) → x ∈ A)
3	2	ssriv 1508	1 ⊢ (A ∩ B) ⊆ A

Syntax hints:   ∈ wcel 1092   ∩ cin 1486   ⊆ wss 1487

This theorem is referenced by:  inss2 1658  ssin 1659  ssinss1 1664  nssinpss 1665  dfin4 1673  inv 1723  difdisj 1758  wefrc 2195  ordtri3or 2230  onfr 2237  relin 2491  resss 2587  cnvcnvss 2662  funimass2 2713  fnresin1 2735  sbthlem7 3355  zfregs 3491  imadomg 3616  chm1 5378  chdmm1 5398  chabs1t 5432  chabs2t 5433  ledi 5447  pjoml4 5497  cmbr3 5509  cmbr4 5510  cmle 5511  cmm1 5514  3oalem4 5555  pjssm 5572  pjocin 5583  pjin 5584  pjin1 5646  pjclem1 5649  stji1 5683  stm1 5684  dmdbr2 5733  ssmd1 5734  atcvat4 5775

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-in 1491  df-ss 1492

metamath.org