Theorem inss1 3357

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

Syntax hints:   ∈ wcel 2148   ∩ cin 3130   ⊆ wss 3131

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2741  df-in 3137  df-ss 3144

This theorem is referenced by:  inss2  3358  ssinss1  3366  unabs  3368  inssddif  3378  inv1  3461  disjdif  3497  inundifss  3502  relin1  4746  resss  4933  resmpt3  4958  cnvcnvss  5085  funin  5289  funimass2  5296  fnresin1  5332  fnres  5334  fresin  5396  ssimaex  5579  fneqeql2  5627  isoini2  5822  ofrfval  6093  ofvalg  6094  ofrval  6095  off  6097  ofres  6099  ofco  6103  smores  6295  smores2  6297  tfrlem5  6317  pmresg  6678  unfiin  6927  sbthlem7  6964  peano5nnnn  7893  peano5nni  8924  rexanuz  10999  nninfdclemcl  12451  nninfdclemp1  12453  fvsetsid  12498  tgvalex  12717  tgval2  13590  eltg3  13596  tgcl  13603  tgdom  13611  tgidm  13613  epttop  13629  ntropn  13656  ntrin  13663  cnptopresti  13777  cnptoprest  13778  txcnmpt  13812  xmetres  13921  metres  13922  blin2  13971  metrest  14045  tgioo  14085  limcresi  14174  2sqlem8  14509  bj-charfun  14598  bj-charfundc  14599  bj-charfundcALT  14600