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

Theorem inss2 3186
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 3157 . 2 (𝐵𝐴) = (𝐴𝐵)
2 inss1 3185 . 2 (𝐵𝐴) ⊆ 𝐵
31, 2eqsstr3i 3004 1 (𝐴𝐵) ⊆ 𝐵
Colors of variables: wff set class
Syntax hints:  cin 2944  wss 2945
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-v 2576  df-in 2952  df-ss 2959
This theorem is referenced by:  difin0  3325  bnd2  3954  ordin  4150  relin2  4484  relres  4667  ssrnres  4791  cnvcnv  4801  funimaexg  5011  fnresin2  5042  ssimaex  5262  ffvresb  5356  ofrfval  5748  fnofval  5749  ofrval  5750  off  5752  ofres  5753  ofco  5757  offres  5790  tpostpos  5910  smores3  5939  tfrlem5  5961  tfrexlem  5979  erinxp  6211  ltrelpi  6480  peano5nnnn  7024  peano5nni  7993  rexanuz  9815  peano5set  10451  peano5setOLD  10452
  Copyright terms: Public domain W3C validator