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 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-in 3942  df-ss 3951
This theorem is referenced by:  difin0  4421  iunxdif3  5016  relin2  5685  relres  5881  idssxp  5915  ssrnres  6034  cnvrescnv  6051  ordin  6220  onfr  6229  ordelinel  6288  fnresin2  6472  fresaunres2  6549  ssimaex  6747  exfo  6870  ffvresb  6887  fnfvimad  6995  ofrfval  7416  ofval  7417  ofrval  7418  off  7423  ofres  7424  ofco  7428  fnwelem  7824  fnse  7826  tfrlem5  8015  pmresg  8433  nnfi  8710  ixpfi2  8821  elfiun  8893  marypha1lem  8896  ordtypelem6  8986  ordtypelem7  8987  hartogslem1  9005  unxpwdom  9052  epfrs  9172  tcmin  9182  bnd2  9321  tskwe  9378  r0weon  9437  infxpenlem  9438  djuinf  9613  ackbij1lem9  9649  ackbij1lem10  9650  ackbij1lem15  9655  ackbij1lem16  9656  ackbij1b  9660  sdom2en01  9723  fin23lem26  9746  fin23lem13  9753  isfin1-3  9807  fin56  9814  fin1a2lem9  9829  brdom3  9949  brdom5  9950  brdom4  9951  fpwwe2lem12  10062  fpwwe2  10064  canthwelem  10071  gruima  10223  ingru  10236  gruina  10239  grur1a  10240  ltrelpi  10310  ltrelnq  10347  nqerf  10351  fzfi  13339  xptrrel  14339  rexanuz  14704  limsupgord  14828  limsupcl  14829  limsupgf  14831  limsupgle  14833  o1of2  14968  o1rlimmul  14974  ackbijnn  15182  bitsinv1  15790  bitsinvp1  15797  sadcaddlem  15805  sadadd2lem  15807  sadadd3  15809  sadaddlem  15814  sadasslem  15818  sadeq  15820  smupval  15836  prmrec  16257  structcnvcnv  16496  ressbasss  16555  ressress  16561  restsspw  16704  submre  16875  isacs1i  16927  rescabs  17102  resscat  17121  funcres2c  17170  ressffth  17207  catccatid  17361  catcisolem  17365  catciso  17366  yoniso  17534  acsinfd  17789  acsdomd  17790  tsrss  17832  idresefmnd  18063  idrespermg  18538  mvdco  18572  sylow2a  18743  lsmmod  18800  acsfn1p  19577  lssacs  19738  asplss  20102  ressmplbas  20236  subrgmpl  20240  mplind  20281  ressply1bas  20396  pf1rcl  20511  zringlpirlem2  20631  zringlpirlem3  20632  ofco2  21059  basdif0  21560  eltg4i  21567  ntrss2  21664  ntrin  21668  isopn3  21673  resttopon  21768  restuni2  21774  restcld  21779  restfpw  21786  neitr  21787  cnrest2r  21894  cnpresti  21895  cnprest  21896  lmss  21905  cnrmi  21967  restcnrm  21969  resthauslem  21970  imacmp  22004  fiuncmp  22011  subislly  22088  islly2  22091  cldllycmp  22102  hauspwdom  22108  kgeni  22144  llycmpkgen2  22157  ptbasfi  22188  ptclsg  22222  ptcnplem  22228  txtube  22247  txcmplem2  22249  txkgen  22259  kqdisj  22339  fbasrn  22491  trfg  22498  isufil2  22515  fmfnfmlem4  22564  hauspwpwf1  22594  txflf  22613  alexsubALTlem4  22657  tmdgsum2  22703  tsmsres  22751  tsmsxplem1  22760  ustexsym  22823  ustund  22829  trust  22837  utoptop  22842  restutop  22845  metrest  23133  restmetu  23179  tgioo  23403  reconnlem2  23434  cphsqrtcl  23787  tcphcph  23839  cfilresi  23897  caussi  23899  causs  23900  ovolfioo  24067  ovolficc  24068  ovolficcss  24069  ovolfsf  24071  ovollb  24079  ovolicc2lem1  24117  ovolicc2lem2  24118  ovolicc2lem3  24119  ovolicc2lem4  24120  ovolicc2  24122  nulmbl  24135  voliunlem1  24150  ovolfs2  24171  uniiccdif  24178  uniioovol  24179  uniiccvol  24180  uniioombllem2  24183  uniioombllem3a  24184  uniioombllem3  24185  uniioombllem4  24186  uniioombllem5  24187  uniioombllem6  24188  uniioombl  24189  dyadmbllem  24199  dyadmbl  24200  opnmbllem  24201  volcn  24206  volivth  24207  mbfadd  24261  mbfsub  24262  i1fima  24278  i1fima2  24279  i1fd  24281  i1fadd  24295  i1fmul  24296  itg1addlem2  24297  itg1addlem4  24299  itg1addlem5  24300  i1fres  24305  mbfmul  24326  bddmulibl  24438  ellimc2  24474  ellimc3  24476  limcflf  24478  limcresi  24482  limciun  24491  dvreslem  24506  dvres2lem  24507  dvres3a  24511  cpnres  24533  dvaddbr  24534  dvmulbr  24535  dvmptres3  24552  lhop1lem  24609  rlimcnp2  25543  xrlimcnp  25545  chpchtsum  25794  2sqlem8  26001  2sqlem9  26002  rpvmasumlem  26062  rplogsum  26102  dirith2  26103  axtgsegcon  26249  axtg5seg  26250  axtgbtwnid  26251  axtgpasch  26252  axtgcont1  26253  tglng  26331  chdmm1i  29253  chm0i  29266  ledii  29312  lejdii  29314  pjoml2i  29361  pjoml4i  29363  cmcmlem  29367  cmbr4i  29377  osumcori  29419  pjssmii  29457  mayete3i  29504  riesz4  29840  riesz1  29841  cnlnadjeu  29854  nmopadjlei  29864  pjclem1  29971  pjci  29976  mdbr3  30073  mdbr4  30074  dmdbr2  30079  dmdbr5  30084  ssmd2  30088  mdslj1i  30095  mdslj2i  30096  mdsl1i  30097  mdsl2bi  30099  mdslmd1lem1  30101  mdslmd1lem2  30102  mdslmd2i  30106  csmdsymi  30110  cvexchlem  30144  atomli  30158  atcvat4i  30173  inindif  30277  difininv  30278  disjxpin  30337  imadifxp  30350  off2  30387  resspos  30646  resstos  30647  submomnd  30711  suborng  30888  ordtrestNEW  31164  pnfneige0  31194  lmxrge0  31195  qqhnm  31231  qqhcn  31232  rrhre  31262  indsumin  31281  indf1ofs  31285  gsumesum  31318  esumlub  31319  esumcst  31322  esumpcvgval  31337  hasheuni  31344  esumcvg  31345  sigainb  31395  carsgclctunlem2  31577  sibfinima  31597  sibfof  31598  eulerpartlemelr  31615  eulerpartlemgh  31636  eulerpartlemgf  31637  eulerpartlemgs2  31638  eulerpartlemn  31639  probmeasb  31688  cndprob01  31693  hashreprin  31891  reprfi2  31894  breprexpnat  31905  hgt750lemd  31919  hgt750lema  31928  tgoldbachgtde  31931  tgoldbachgtda  31932  tgoldbachgt  31934  bnj1293  32088  connpconn  32482  iccllysconn  32497  cvmsss2  32521  cvmcov2  32522  cvmopnlem  32525  cvmliftmolem2  32529  cvmlift2lem12  32561  mvrsfpw  32753  elmsta  32795  msubvrs  32807  mclsind  32817  nepss  32948  dfon2lem4  33031  fprlem1  33137  nosupbnd2  33216  trer  33664  neiin  33680  neibastop1  33707  neibastop2lem  33708  topmeet  33712  filnetlem3  33728  bj-disj2r  34340  bj-restpw  34382  bj-restb  34384  bj-restuni2  34388  bj-ablsscmn  34559  topdifinffinlem  34627  opnmbllem0  34927  mblfinlem4  34931  mbfposadd  34938  heibor1lem  35086  heiborlem1  35088  heiborlem3  35090  heiborlem10  35097  opidonOLD  35129  disjimin  35980  lshpinN  36124  lcvexchlem1  36169  lcvexchlem5  36173  pmod1i  36983  pmodN  36985  osumcllem7N  37097  pexmidlem4N  37108  dochdmj1  38525  dochexmidlem4  38598  lcfrlem25  38702  mapd1o  38783  mapdin  38797  elrfi  39291  elrfirn  39292  fnwe2lem2  39651  aomclem2  39655  lsmfgcl  39674  lmhmfgima  39684  lmhmfgsplit  39686  lmhmlnmsplit  39687  hbt  39730  trrelind  40010  iunrelexp0  40047  isotone2  40399  grumnudlem  40621  onfrALTlem3  40878  onfrALTlem2  40880  onfrALTlem3VD  41221  onfrALTlem2VD  41223  iunconnlem2  41269  restuni6  41388  disjinfi  41454  inmap  41472  dmresss  41501  fsumiunss  41856  islptre  41900  sumnnodd  41911  limcresiooub  41923  limcresioolb  41924  limcleqr  41925  limclner  41932  limclr  41936  limsuplesup  41980  limsuppnfdlem  41982  limsupres  41986  liminfgord  42035  liminfgf  42039  liminfcl  42044  limsupresxr  42047  liminfresxr  42048  liminfval2  42049  liminflelimsuplem  42056  liminfvalxr  42064  icccncfext  42170  fourierdlem20  42413  fourierdlem48  42440  fourierdlem49  42441  fourierdlem50  42442  fourierdlem76  42468  fourierdlem103  42495  fourierdlem104  42496  fourierdlem113  42505  fouriersw  42517  salgencntex  42627  sge0less  42675  sge0resplit  42689  sge0split  42692  sge0iunmptlemre  42698  sge0fodjrnlem  42699  caragencmpl  42818  ovolval2lem  42926  ovolval2  42927  ovolval3  42930  ovolval4lem2  42933  sssmf  43016  lidlssbas  44194  rnghmresfn  44235  rnghmsscmap  44246  rngchomrnghmresALTV  44268  rhmresfn  44281  rhmsscmap  44292  rhmsubclem4  44361
  Copyright terms: Public domain W3C validator