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

Theorem inss2 3992
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 3966 . 2 (𝐵𝐴) = (𝐴𝐵)
2 inss1 3991 . 2 (𝐵𝐴) ⊆ 𝐵
31, 2eqsstr3i 3795 1 (𝐴𝐵) ⊆ 𝐵
Colors of variables: wff setvar class
Syntax hints:  cin 3730  wss 3731
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2742
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-v 3351  df-in 3738  df-ss 3745
This theorem is referenced by:  difin0  4200  iunxdif3  4762  relin2  5404  relres  5600  idssxp  5637  ssrnres  5754  cnvcnv  5768  cnvcnvOLD  5769  ordin  5937  onfr  5946  ordelinel  6005  fnresin2  6183  fresaunres2  6257  ssimaex  6451  exfo  6566  ffvresb  6583  ofrfval  7102  ofval  7103  ofrval  7104  off  7109  ofres  7110  ofco  7114  offres  7360  fnwelem  7493  fnse  7495  tpostpos  7574  wfrlem4OLD  7621  smores3  7653  tfrlem5  7679  pmresg  8087  nnfi  8359  ixpfi2  8470  f1opwfi  8476  dffi2  8535  elfiun  8542  marypha1lem  8545  ordtypelem3  8631  ordtypelem6  8634  ordtypelem7  8635  hartogslem1  8653  unxpwdom  8700  epfrs  8821  tcmin  8831  bnd2  8970  tskwe  9026  r0weon  9085  infxpenlem  9086  fodomfi2  9133  infpwfien  9135  cdainf  9266  ackbij1lem6  9299  ackbij1lem9  9302  ackbij1lem10  9303  ackbij1lem11  9304  ackbij1lem15  9308  ackbij1lem16  9309  ackbij1lem18  9311  ackbij1b  9313  sdom2en01  9376  fin23lem26  9399  fin23lem13  9406  isfin1-3  9460  fin56  9467  fin1a2lem9  9482  ttukeylem6  9588  brdom3  9602  brdom5  9603  brdom4  9604  fpwwe2lem12  9715  fpwwe2  9717  canthwelem  9724  gruima  9876  ingru  9889  gruina  9892  grur1a  9893  ltrelpi  9963  ltrelnq  10000  nqerf  10004  dedekindle  10454  fzfi  12978  xptrrel  14007  rexanuz  14371  limsupgord  14489  limsupcl  14490  limsupgf  14492  limsupgle  14494  rlimres  14575  lo1res  14576  o1of2  14629  o1rlimmul  14635  ackbijnn  14845  bitsinv1  15446  bitsinvp1  15453  sadcaddlem  15461  sadadd2lem  15463  sadadd3  15465  sadaddlem  15470  sadasslem  15474  sadeq  15476  smuval2  15486  smupval  15492  smueqlem  15494  prmrec  15906  isstruct2  16141  structcnvcnv  16145  ressbasss  16205  ressress  16212  restsspw  16359  submre  16532  isacs2  16580  isacs1i  16584  sscres  16749  rescabs  16759  resscat  16778  funcres2c  16827  coffth  16862  rescfth  16863  ressffth  16864  catccatid  17018  catcisolem  17022  catciso  17023  catcoppccl  17024  catcfuccl  17025  catcxpccl  17114  yoniso  17192  isdrs2  17206  isacs3lem  17433  acsinfd  17447  acsdomd  17448  tsrss  17490  idrespermg  18095  mvdco  18129  sylow2a  18299  lsmmod  18353  frgpnabllem2  18542  subrgpropd  19082  lssacs  19238  sralmod  19460  asplss  19602  ressmplbas  19729  subrgmpl  19733  opsrtoslem2  19757  mplind  19774  ressply1bas  19871  pf1rcl  19985  zringlpirlem2  20105  zringlpirlem3  20106  ofco2  20533  basdif0  21036  eltg4i  21043  ntrss2  21140  ntrin  21144  isopn3  21149  mreclatdemoBAD  21179  neiptoptop  21214  restbas  21241  resttopon  21244  restuni2  21250  restcld  21255  restfpw  21262  neitr  21263  ordtrest  21285  subbascn  21337  cnrest2r  21370  cnpresti  21371  cnprest  21372  lmss  21381  cnrmi  21443  restcnrm  21445  resthauslem  21446  fincmp  21475  imacmp  21479  fiuncmp  21486  cmpfi  21490  bwth  21492  cnconn  21504  iunconn  21510  clsconn  21512  conncompclo  21517  1stcrest  21535  subislly  21563  islly2  21566  cldllycmp  21577  hauspwdom  21583  kgeni  21619  llycmpkgen2  21632  1stckgenlem  21635  ptbasfi  21663  txcls  21686  ptclsg  21697  txcnp  21702  ptcnplem  21703  txtube  21722  txcmplem1  21723  txcmplem2  21724  txkgen  21734  xkopt  21737  xkococnlem  21741  txconn  21771  basqtop  21793  tgqtop  21794  kqdisj  21814  kqnrmlem1  21825  kqnrmlem2  21826  nrmhmph  21876  infil  21945  fbasrn  21966  trfg  21973  uzrest  21979  isufil2  21990  fmfnfmlem4  22039  hauspwpwf1  22069  txflf  22088  alexsubALTlem3  22131  alexsubALTlem4  22132  ptcmplem2  22135  tmdgsum2  22178  tsmsres  22225  tsmsxplem1  22234  ustexsym  22297  ustund  22303  trust  22311  utoptop  22316  restutop  22319  blres  22514  met2ndci  22605  metrest  22607  restmetu  22653  tgioo  22877  zdis  22897  reconnlem2  22908  reconn  22909  cnheibor  23032  lebnum  23041  cphsqrtcl  23261  tcphcph  23313  cfilresi  23371  cfilres  23372  caussi  23373  causs  23374  minveclem4b  23490  minveclem4  23491  ovolfcl  23523  ovolfioo  23524  ovolficc  23525  ovolficcss  23526  ovolfsval  23527  ovolfsf  23528  ovollb  23536  ovolicc2lem1  23574  ovolicc2lem2  23575  ovolicc2lem3  23576  ovolicc2lem4  23577  ovolicc2lem5  23578  ovolicc2  23579  nulmbl  23592  voliunlem1  23607  ioombl1lem4  23618  ovolfs2  23628  uniiccdif  23635  uniioovol  23636  uniiccvol  23637  uniioombllem2a  23639  uniioombllem2  23640  uniioombllem3a  23641  uniioombllem3  23642  uniioombllem4  23643  uniioombllem5  23644  uniioombllem6  23645  uniioombl  23646  dyadmbllem  23656  dyadmbl  23657  opnmbllem  23658  volcn  23663  volivth  23664  vitalilem2  23666  vitalilem4  23668  mbfadd  23718  mbfsub  23719  i1fima  23735  i1fima2  23736  i1fd  23738  i1fadd  23752  i1fmul  23753  itg1addlem2  23754  itg1addlem4  23756  itg1addlem5  23757  i1fres  23762  mbfmul  23783  bddmulibl  23895  ellimc2  23931  ellimc3  23933  limcflf  23935  limcresi  23939  limciun  23948  dvreslem  23963  dvres2lem  23964  dvres3a  23968  cpnres  23990  dvaddbr  23991  dvmulbr  23992  dvmptres3  24009  lhop1lem  24066  ig1peu  24221  taylfvallem1  24401  rlimcnp2  24983  xrlimcnp  24985  ppisval  25120  chtf  25124  efchtcl  25127  chtge0  25128  ppinprm  25168  chtprm  25169  chtnprm  25170  chtwordi  25172  chtdif  25174  efchtdvds  25175  chtlepsi  25221  chtleppi  25225  pclogsum  25230  chpval2  25233  chpchtsum  25234  chpub  25235  2sqlem8  25441  2sqlem9  25442  chebbnd1lem1  25448  chtppilimlem1  25452  rplogsumlem2  25464  rpvmasumlem  25466  rplogsum  25506  dirith2  25507  axtgsegcon  25653  axtg5seg  25654  axtgbtwnid  25655  axtgpasch  25656  axtgcont1  25657  tglng  25731  perpneq  25899  ragperp  25902  chdmm1i  28726  chm0i  28739  ledii  28785  lejdii  28787  pjoml2i  28834  pjoml4i  28836  cmcmlem  28840  cmbr4i  28850  osumcori  28892  pjssmii  28930  mayete3i  28977  riesz4  29313  riesz1  29314  cnlnadjeu  29327  nmopadjlei  29337  pjclem1  29444  pjci  29449  mdbr3  29546  mdbr4  29547  dmdbr2  29552  dmdbr5  29557  ssmd2  29561  mdslj1i  29568  mdslj2i  29569  mdsl1i  29570  mdsl2bi  29572  mdslmd1lem1  29574  mdslmd1lem2  29575  mdslmd2i  29579  csmdsymi  29583  cvexchlem  29617  atomli  29631  atcvat4i  29646  inindif  29736  difininv  29737  disjxpin  29783  imadifxp  29796  off2  29827  resspos  30040  resstos  30041  submomnd  30091  suborng  30196  prsdm  30341  prsrn  30342  ordtrestNEW  30348  pnfneige0  30378  lmxrge0  30379  qqhnm  30415  qqhcn  30416  rrhre  30446  indsumin  30465  indf1ofs  30469  gsumesum  30502  esumlub  30503  esumcst  30506  esumpcvgval  30521  hasheuni  30528  esumcvg  30529  sigainb  30580  carsgclctunlem2  30762  sibfinima  30782  sibfof  30783  eulerpartlemelr  30800  eulerpartlemgh  30821  eulerpartlemgf  30822  eulerpartlemgs2  30823  eulerpartlemn  30824  probmeasb  30874  cndprob01  30879  hashreprin  31080  reprfi2  31083  breprexpnat  31094  hgt750lemd  31108  hgt750lema  31117  tgoldbachgtde  31120  tgoldbachgtda  31121  tgoldbachgt  31123  bnj1293  31266  connpconn  31596  iccllysconn  31611  cvmsss2  31635  cvmcov2  31636  cvmopnlem  31639  cvmliftmolem2  31643  cvmlift2lem12  31675  mvrsfpw  31782  elmsta  31824  msubvrs  31836  mclsind  31846  nepss  31976  elrn3  32028  dfon2lem4  32065  nosupbnd2  32237  trer  32685  neiin  32701  neibastop1  32728  neibastop2lem  32729  topmeet  32733  filnetlem3  32749  bj-disj2r  33372  bj-restpw  33405  bj-restb  33407  bj-restuni2  33411  bj-ablsscmn  33506  topdifinffinlem  33560  opnmbllem0  33801  mblfinlem4  33805  mbfposadd  33812  heibor1lem  33962  heiborlem1  33964  heiborlem3  33966  heiborlem10  33973  opidonOLD  34005  lshpinN  34877  lcvexchlem1  34922  lcvexchlem5  34926  pmod1i  35736  pmodN  35738  osumcllem7N  35850  pexmidlem4N  35861  dochdmj1  37278  dochexmidlem4  37351  lcfrlem25  37455  mapd1o  37536  mapdin  37550  elrfi  37867  elrfirn  37868  fnwe2lem2  38230  aomclem2  38234  lsmfgcl  38253  lmhmfgima  38263  lmhmfgsplit  38265  lmhmlnmsplit  38266  hbt  38309  acsfn1p  38378  trrelind  38564  iunrelexp0  38601  isotone2  38953  onfrALTlem3  39354  onfrALTlem2  39356  onfrALTlem3VD  39707  onfrALTlem2VD  39709  iunconnlem2  39755  restuni6  39887  disjinfi  39959  inmap  39978  dmresss  40010  fnfvimad  40033  fnfvima2  40051  fsumiunss  40377  islptre  40421  sumnnodd  40432  limcresiooub  40444  limcresioolb  40445  limcleqr  40446  limclner  40453  limclr  40457  limsuplesup  40501  limsuppnfdlem  40503  limsupres  40507  liminfgord  40556  liminfgf  40560  liminfcl  40565  limsupresxr  40568  liminfresxr  40569  liminfval2  40570  liminflelimsuplem  40577  liminfvalxr  40585  icccncfext  40670  fourierdlem20  40913  fourierdlem48  40940  fourierdlem49  40941  fourierdlem50  40942  fourierdlem76  40968  fourierdlem103  40995  fourierdlem104  40996  fourierdlem113  41005  fouriersw  41017  salgencntex  41130  sge0less  41178  sge0resplit  41192  sge0split  41195  sge0iunmptlemre  41201  sge0fodjrnlem  41202  caragencmpl  41321  ovolval2lem  41429  ovolval2  41430  ovolval3  41433  ovolval4lem2  41436  sssmf  41519  lidlssbas  42523  rnghmresfn  42564  rnghmsscmap  42575  rngchomrnghmresALTV  42597  rhmresfn  42610  rhmsscmap  42621  rhmsubclem4  42690
  Copyright terms: Public domain W3C validator