ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  inss2 GIF version

Theorem inss2 3348
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
inss2 (𝐴𝐵) ⊆ 𝐵

Proof of Theorem inss2
StepHypRef Expression
1 incom 3319 . 2 (𝐵𝐴) = (𝐴𝐵)
2 inss1 3347 . 2 (𝐵𝐴) ⊆ 𝐵
31, 2eqsstrri 3180 1 (𝐴𝐵) ⊆ 𝐵
Colors of variables: wff set class
Syntax hints:  cin 3120  wss 3121
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-in 3127  df-ss 3134
This theorem is referenced by:  difin0  3487  bnd2  4157  ordin  4368  relin2  4728  relres  4917  ssrnres  5051  cnvcnv  5061  funinsn  5245  funimaexg  5280  fnresin2  5311  ssimaex  5555  ffvresb  5657  ofrfval  6067  ofvalg  6068  ofrval  6069  off  6071  ofres  6073  ofco  6077  offres  6112  tpostpos  6241  smores3  6270  tfrlem5  6291  tfrexlem  6311  erinxp  6584  pmresg  6651  unfiin  6900  ltrelpi  7275  peano5nnnn  7843  peano5nni  8870  rexanuz  10941  structcnvcnv  12421  restsspw  12578  eltg4i  12810  ntrss2  12876  ntrin  12879  isopn3  12880  resttopon  12926  restuni2  12932  cnrest2r  12992  cnptopresti  12993  cnptoprest  12994  lmss  13001  metrest  13261  tgioo  13301  2sqlem8  13714  2sqlem9  13715  peano5set  13937
  Copyright terms: Public domain W3C validator