Theorem inss1 3429

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

Syntax hints:   ∈ wcel 2202   ∩ cin 3200   ⊆ wss 3201

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-in 3207  df-ss 3214

This theorem is referenced by:  inss2  3430  ssinss1  3438  unabs  3440  inssddif  3450  inv1  3533  disjdif  3569  inundifss  3574  relin1  4851  resss  5043  resmpt3  5068  cnvcnvss  5198  funin  5408  funimass2  5415  fnresin1  5454  fnres  5456  fresin  5523  ssimaex  5716  fneqeql2  5765  fnfvimad  5900  isoini2  5970  ofrfval  6253  ofvalg  6254  ofrval  6255  off  6257  ofres  6259  ofco  6263  smores  6501  smores2  6503  tfrlem5  6523  pmresg  6888  unfiin  7161  infidc  7176  sbthlem7  7205  peano5nnnn  8155  peano5nni  9188  rexanuz  11611  nninfdclemcl  13132  nninfdclemp1  13134  fvsetsid  13179  tgvalex  13409  tgval2  14845  eltg3  14851  tgcl  14858  tgdom  14866  tgidm  14868  epttop  14884  ntropn  14911  ntrin  14918  cnptopresti  15032  cnptoprest  15033  txcnmpt  15067  xmetres  15176  metres  15177  blin2  15226  metrest  15300  tgioo  15348  limcresi  15460  2sqlem8  15925  bj-charfun  16506  bj-charfundc  16507  bj-charfundcALT  16508