Theorem inss1 2282

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 2259	. . 3 ⊢ (x ∈ (A ∩ B) ↔ (x ∈ A ⋀ x ∈ B))
2	1	pm3.26bi 320	. 2 ⊢ (x ∈ (A ∩ B) → x ∈ A)
3	2	ssriv 2121	1 ⊢ (A ∩ B) ⊆ A

Syntax hints:   ∈ wcel 994   ∩ cin 2098   ⊆ wss 2099

This theorem is referenced by:  inss2 2283  ssin 2284  ssinss1 2289  unabs 2290  nssinpss 2292  dfin4 2300  inv1 2352  difdisj 2390  wefrc 2970  ordtri3or 3007  onfr 3014  relin1 3351  resss 3473  cnvcnvss 3572  funimass2 3678  fnresin1 3707  ssimaex 3879  fparlem3 4201  fparlem4 4202  sbthlem7 4598  zfregs 4793  brdom3 4947  brdom5 4948  brdom4 4949  imadomg 4952  tgval2 7829  unitg 7835  cnsscnp 7982  bcthlem14 8223  bcthlem16 8225  phnv 8729  minveceu 8843  minvecle 8846  chm1i 9655  chdmm1i 9676  chabs1 9715  chabs2 9716  ledii 9735  lejdii 9737  pjoml4i 9806  cmbr3i 9819  cmbr4i 9820  cmm1i 9825  osumcor2i 9868  3oalem4 9888  pjssmii 9904  pjocini 9921  pjini 9922  mayete3i 9951  mayete3OLDi 9952  riesz4 10276  riesz1 10277  cnlnadjeui 10289  cnlnadjeu 10290  cnlnssadj 10292  nmopadjlei 10300  pjin1i 10401  pjclem1 10404  stji1i 10450  stm1i 10451  dmdbr2 10511  ssmd1 10519  mdslj2i 10528  mdsl2bi 10531  mdslmd1lem1 10533  mdslmd2i 10538  atomli 10591  atcvat4i 10606  sumdmdlem2 10628  dmdbr5ati 10631  dmdbr6ati 10632  dmdbr7ati 10633  toplat 10884  opidon 10898  clsint 11010  fintopcomp 11115  elfiun 11421  ntrin 11463  elsubsp 11477  subcls 11481  compsublem 11487  compsub 11488  alexsublem4 11499  connsub 11502  subtopmetlem 11505  reconnlem3 11509  reconnlem4 11510  reconnlem5 11511  fnessref 11564  locfincomp 11575  neibastop1 11579  fbunfip 11631  filrn 11643  filfinnfr 11646  filcon 11665  tosdir 11755  filnetlem3 11765  metsstop 11909  sstotbnd 11992  totbndss 11993  heiborlem28 12038  rrntotbnd 12078

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-in 2103  df-ss 2105

Copyright terms: Public domain