Theorem inss1 3393

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

Syntax hints:   ∈ wcel 2176   ∩ cin 3165   ⊆ wss 3166

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-in 3172  df-ss 3179

This theorem is referenced by:  inss2  3394  ssinss1  3402  unabs  3404  inssddif  3414  inv1  3497  disjdif  3533  inundifss  3538  relin1  4793  resss  4983  resmpt3  5008  cnvcnvss  5137  funin  5345  funimass2  5352  fnresin1  5390  fnres  5392  fresin  5454  ssimaex  5640  fneqeql2  5689  isoini2  5888  ofrfval  6167  ofvalg  6168  ofrval  6169  off  6171  ofres  6173  ofco  6177  smores  6378  smores2  6380  tfrlem5  6400  pmresg  6763  unfiin  7023  infidc  7036  sbthlem7  7065  peano5nnnn  8005  peano5nni  9039  rexanuz  11299  nninfdclemcl  12819  nninfdclemp1  12821  fvsetsid  12866  tgvalex  13095  tgval2  14523  eltg3  14529  tgcl  14536  tgdom  14544  tgidm  14546  epttop  14562  ntropn  14589  ntrin  14596  cnptopresti  14710  cnptoprest  14711  txcnmpt  14745  xmetres  14854  metres  14855  blin2  14904  metrest  14978  tgioo  15026  limcresi  15138  2sqlem8  15600  bj-charfun  15743  bj-charfundc  15744  bj-charfundcALT  15745