Theorem inss1 3353

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 3316	. . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
2	1	simplbi 274	. 2 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) → 𝑥 ∈ 𝐴)
3	2	ssriv 3157	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴

Syntax hints:   ∈ wcel 2146   ∩ cin 3126   ⊆ wss 3127

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-v 2737  df-in 3133  df-ss 3140

This theorem is referenced by:  inss2  3354  ssinss1  3362  unabs  3364  inssddif  3374  inv1  3457  disjdif  3493  inundifss  3498  relin1  4738  resss  4924  resmpt3  4949  cnvcnvss  5075  funin  5279  funimass2  5286  fnresin1  5322  fnres  5324  fresin  5386  ssimaex  5569  fneqeql2  5617  isoini2  5810  ofrfval  6081  ofvalg  6082  ofrval  6083  off  6085  ofres  6087  ofco  6091  smores  6283  smores2  6285  tfrlem5  6305  pmresg  6666  unfiin  6915  sbthlem7  6952  peano5nnnn  7866  peano5nni  8895  rexanuz  10965  nninfdclemcl  12416  nninfdclemp1  12418  fvsetsid  12463  tgvalex  13130  tgval2  13131  eltg3  13137  tgcl  13144  tgdom  13152  tgidm  13154  epttop  13170  ntropn  13197  ntrin  13204  cnptopresti  13318  cnptoprest  13319  txcnmpt  13353  xmetres  13462  metres  13463  blin2  13512  metrest  13586  tgioo  13626  limcresi  13715  2sqlem8  14039  bj-charfun  14128  bj-charfundc  14129  bj-charfundcALT  14130