MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  inss2 Structured version   Visualization version   GIF version

Theorem inss2 4205
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 4177 . 2 (𝐵𝐴) = (𝐴𝐵)
2 inss1 4204 . 2 (𝐵𝐴) ⊆ 𝐵
31, 2eqsstrri 4001 1 (𝐴𝐵) ⊆ 𝐵
Colors of variables: wff setvar class
Syntax hints:  cin 3934  wss 3935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-in 3942  df-ss 3951
This theorem is referenced by:  difin0  4420  iunxdif3  5009  relin2  5680  relres  5876  idssxp  5910  ssrnres  6029  cnvrescnv  6046  ordin  6215  onfr  6224  ordelinel  6283  fnresin2  6467  fresaunres2  6544  ssimaex  6742  exfo  6864  ffvresb  6881  fnfvimad  6987  ofrfval  7406  ofval  7407  ofrval  7408  off  7413  ofres  7414  ofco  7418  fnwelem  7816  fnse  7818  tfrlem5  8007  pmresg  8424  nnfi  8700  ixpfi2  8811  elfiun  8883  marypha1lem  8886  ordtypelem6  8976  ordtypelem7  8977  hartogslem1  8995  unxpwdom  9042  epfrs  9162  tcmin  9172  bnd2  9311  tskwe  9368  r0weon  9427  infxpenlem  9428  djuinf  9603  ackbij1lem9  9639  ackbij1lem10  9640  ackbij1lem15  9645  ackbij1lem16  9646  ackbij1b  9650  sdom2en01  9713  fin23lem26  9736  fin23lem13  9743  isfin1-3  9797  fin56  9804  fin1a2lem9  9819  brdom3  9939  brdom5  9940  brdom4  9941  fpwwe2lem12  10052  fpwwe2  10054  canthwelem  10061  gruima  10213  ingru  10226  gruina  10229  grur1a  10230  ltrelpi  10300  ltrelnq  10337  nqerf  10341  fzfi  13330  xptrrel  14330  rexanuz  14695  limsupgord  14819  limsupcl  14820  limsupgf  14822  limsupgle  14824  o1of2  14959  o1rlimmul  14965  ackbijnn  15173  bitsinv1  15781  bitsinvp1  15788  sadcaddlem  15796  sadadd2lem  15798  sadadd3  15800  sadaddlem  15805  sadasslem  15809  sadeq  15811  smupval  15827  prmrec  16248  structcnvcnv  16487  ressbasss  16546  ressress  16552  restsspw  16695  submre  16866  isacs1i  16918  rescabs  17093  resscat  17112  funcres2c  17161  ressffth  17198  catccatid  17352  catcisolem  17356  catciso  17357  yoniso  17525  acsinfd  17780  acsdomd  17781  tsrss  17823  idrespermg  18470  mvdco  18504  sylow2a  18675  lsmmod  18732  acsfn1p  19509  lssacs  19670  asplss  20033  ressmplbas  20167  subrgmpl  20171  mplind  20212  ressply1bas  20327  pf1rcl  20442  zringlpirlem2  20562  zringlpirlem3  20563  ofco2  20990  basdif0  21491  eltg4i  21498  ntrss2  21595  ntrin  21599  isopn3  21604  resttopon  21699  restuni2  21705  restcld  21710  restfpw  21717  neitr  21718  cnrest2r  21825  cnpresti  21826  cnprest  21827  lmss  21836  cnrmi  21898  restcnrm  21900  resthauslem  21901  imacmp  21935  fiuncmp  21942  subislly  22019  islly2  22022  cldllycmp  22033  hauspwdom  22039  kgeni  22075  llycmpkgen2  22088  ptbasfi  22119  ptclsg  22153  ptcnplem  22159  txtube  22178  txcmplem2  22180  txkgen  22190  kqdisj  22270  fbasrn  22422  trfg  22429  isufil2  22446  fmfnfmlem4  22495  hauspwpwf1  22525  txflf  22544  alexsubALTlem4  22588  tmdgsum2  22634  tsmsres  22681  tsmsxplem1  22690  ustexsym  22753  ustund  22759  trust  22767  utoptop  22772  restutop  22775  metrest  23063  restmetu  23109  tgioo  23333  reconnlem2  23364  cphsqrtcl  23717  tcphcph  23769  cfilresi  23827  caussi  23829  causs  23830  ovolfioo  23997  ovolficc  23998  ovolficcss  23999  ovolfsf  24001  ovollb  24009  ovolicc2lem1  24047  ovolicc2lem2  24048  ovolicc2lem3  24049  ovolicc2lem4  24050  ovolicc2  24052  nulmbl  24065  voliunlem1  24080  ovolfs2  24101  uniiccdif  24108  uniioovol  24109  uniiccvol  24110  uniioombllem2  24113  uniioombllem3a  24114  uniioombllem3  24115  uniioombllem4  24116  uniioombllem5  24117  uniioombllem6  24118  uniioombl  24119  dyadmbllem  24129  dyadmbl  24130  opnmbllem  24131  volcn  24136  volivth  24137  mbfadd  24191  mbfsub  24192  i1fima  24208  i1fima2  24209  i1fd  24211  i1fadd  24225  i1fmul  24226  itg1addlem2  24227  itg1addlem4  24229  itg1addlem5  24230  i1fres  24235  mbfmul  24256  bddmulibl  24368  ellimc2  24404  ellimc3  24406  limcflf  24408  limcresi  24412  limciun  24421  dvreslem  24436  dvres2lem  24437  dvres3a  24441  cpnres  24463  dvaddbr  24464  dvmulbr  24465  dvmptres3  24482  lhop1lem  24539  rlimcnp2  25472  xrlimcnp  25474  chpchtsum  25723  2sqlem8  25930  2sqlem9  25931  rpvmasumlem  25991  rplogsum  26031  dirith2  26032  axtgsegcon  26178  axtg5seg  26179  axtgbtwnid  26180  axtgpasch  26181  axtgcont1  26182  tglng  26260  chdmm1i  29182  chm0i  29195  ledii  29241  lejdii  29243  pjoml2i  29290  pjoml4i  29292  cmcmlem  29296  cmbr4i  29306  osumcori  29348  pjssmii  29386  mayete3i  29433  riesz4  29769  riesz1  29770  cnlnadjeu  29783  nmopadjlei  29793  pjclem1  29900  pjci  29905  mdbr3  30002  mdbr4  30003  dmdbr2  30008  dmdbr5  30013  ssmd2  30017  mdslj1i  30024  mdslj2i  30025  mdsl1i  30026  mdsl2bi  30028  mdslmd1lem1  30030  mdslmd1lem2  30031  mdslmd2i  30035  csmdsymi  30039  cvexchlem  30073  atomli  30087  atcvat4i  30102  inindif  30206  difininv  30207  disjxpin  30267  imadifxp  30280  off2  30317  resspos  30574  resstos  30575  submomnd  30639  suborng  30816  ordtrestNEW  31064  pnfneige0  31094  lmxrge0  31095  qqhnm  31131  qqhcn  31132  rrhre  31162  indsumin  31181  indf1ofs  31185  gsumesum  31218  esumlub  31219  esumcst  31222  esumpcvgval  31237  hasheuni  31244  esumcvg  31245  sigainb  31295  carsgclctunlem2  31477  sibfinima  31497  sibfof  31498  eulerpartlemelr  31515  eulerpartlemgh  31536  eulerpartlemgf  31537  eulerpartlemgs2  31538  eulerpartlemn  31539  probmeasb  31588  cndprob01  31593  hashreprin  31791  reprfi2  31794  breprexpnat  31805  hgt750lemd  31819  hgt750lema  31828  tgoldbachgtde  31831  tgoldbachgtda  31832  tgoldbachgt  31834  bnj1293  31988  connpconn  32380  iccllysconn  32395  cvmsss2  32419  cvmcov2  32420  cvmopnlem  32423  cvmliftmolem2  32427  cvmlift2lem12  32459  mvrsfpw  32651  elmsta  32693  msubvrs  32705  mclsind  32715  nepss  32846  dfon2lem4  32929  fprlem1  33035  nosupbnd2  33114  trer  33562  neiin  33578  neibastop1  33605  neibastop2lem  33606  topmeet  33610  filnetlem3  33626  bj-disj2r  34238  bj-restpw  34278  bj-restb  34280  bj-restuni2  34284  bj-ablsscmn  34449  topdifinffinlem  34511  opnmbllem0  34810  mblfinlem4  34814  mbfposadd  34821  heibor1lem  34970  heiborlem1  34972  heiborlem3  34974  heiborlem10  34981  opidonOLD  35013  disjimin  35863  lshpinN  36007  lcvexchlem1  36052  lcvexchlem5  36056  pmod1i  36866  pmodN  36868  osumcllem7N  36980  pexmidlem4N  36991  dochdmj1  38408  dochexmidlem4  38481  lcfrlem25  38585  mapd1o  38666  mapdin  38680  elrfi  39171  elrfirn  39172  fnwe2lem2  39531  aomclem2  39535  lsmfgcl  39554  lmhmfgima  39564  lmhmfgsplit  39566  lmhmlnmsplit  39567  hbt  39610  trrelind  39890  iunrelexp0  39927  isotone2  40279  grumnudlem  40501  onfrALTlem3  40758  onfrALTlem2  40760  onfrALTlem3VD  41101  onfrALTlem2VD  41103  iunconnlem2  41149  restuni6  41269  disjinfi  41334  inmap  41352  dmresss  41381  fsumiunss  41736  islptre  41780  sumnnodd  41791  limcresiooub  41803  limcresioolb  41804  limcleqr  41805  limclner  41812  limclr  41816  limsuplesup  41860  limsuppnfdlem  41862  limsupres  41866  liminfgord  41915  liminfgf  41919  liminfcl  41924  limsupresxr  41927  liminfresxr  41928  liminfval2  41929  liminflelimsuplem  41936  liminfvalxr  41944  icccncfext  42050  fourierdlem20  42293  fourierdlem48  42320  fourierdlem49  42321  fourierdlem50  42322  fourierdlem76  42348  fourierdlem103  42375  fourierdlem104  42376  fourierdlem113  42385  fouriersw  42397  salgencntex  42507  sge0less  42555  sge0resplit  42569  sge0split  42572  sge0iunmptlemre  42578  sge0fodjrnlem  42579  caragencmpl  42698  ovolval2lem  42806  ovolval2  42807  ovolval3  42810  ovolval4lem2  42813  sssmf  42896  idresefmnd  43969  lidlssbas  44091  rnghmresfn  44132  rnghmsscmap  44143  rngchomrnghmresALTV  44165  rhmresfn  44178  rhmsscmap  44189  rhmsubclem4  44258
  Copyright terms: Public domain W3C validator