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

Theorem inss2 3791
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 3762 . 2 (𝐵𝐴) = (𝐴𝐵)
2 inss1 3790 . 2 (𝐵𝐴) ⊆ 𝐵
31, 2eqsstr3i 3594 1 (𝐴𝐵) ⊆ 𝐵
Colors of variables: wff setvar class
Syntax hints:  cin 3534  wss 3535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-v 3170  df-in 3542  df-ss 3549
This theorem is referenced by:  difin0  3988  iunxdif3  4532  relin2  5145  relres  5329  ssrnres  5473  cnvcnv  5487  ordin  5652  onfr  5662  ordelinel  5724  ordelinelOLD  5725  fnresin2  5902  fresaunres2  5970  ssimaex  6154  exfo  6266  ffvresb  6282  ofrfval  6776  ofval  6777  ofrval  6778  off  6783  ofres  6784  ofco  6788  offres  7027  fnwelem  7152  fnse  7154  tpostpos  7232  wfrlem4  7278  smores3  7310  tfrlem5  7336  erinxp  7681  pmresg  7744  nnfi  8011  ixpfi2  8120  f1opwfi  8126  dffi2  8185  elfiun  8192  marypha1lem  8195  ordtypelem3  8281  ordtypelem6  8284  ordtypelem7  8285  hartogslem1  8303  unxpwdom  8350  epfrs  8463  tcmin  8473  bnd2  8612  tskwe  8632  r0weon  8691  infxpenlem  8692  fodomfi2  8739  infpwfien  8741  cdainf  8870  ackbij1lem6  8903  ackbij1lem9  8906  ackbij1lem10  8907  ackbij1lem11  8908  ackbij1lem15  8912  ackbij1lem16  8913  ackbij1lem18  8915  ackbij1b  8917  sdom2en01  8980  fin23lem26  9003  fin23lem13  9010  isfin1-3  9064  fin56  9071  fin1a2lem9  9086  ttukeylem6  9192  brdom3  9204  brdom5  9205  brdom4  9206  fpwwe2lem8  9311  fpwwe2lem9  9312  fpwwe2lem12  9315  fpwwe2  9317  canthwelem  9324  gruima  9476  ingru  9489  gruina  9492  grur1a  9493  ltrelpi  9563  ltrelnq  9600  nqerf  9604  dedekindle  10048  fzfi  12584  xptrrel  13509  rexanuz  13875  limsupgord  13993  limsupcl  13994  limsupgf  13996  limsupgle  13998  rlimres  14079  lo1res  14080  o1of2  14133  o1rlimmul  14139  ackbijnn  14341  bitsinv1  14944  bitsinvp1  14951  sadcaddlem  14959  sadadd2lem  14961  sadadd3  14963  sadaddlem  14968  sadasslem  14972  sadeq  14974  smuval2  14984  smupval  14990  smueqlem  14992  prmrec  15406  isstruct2  15646  structcnvcnv  15648  ressbasss  15701  ressress  15707  restsspw  15857  pwsle  15917  submre  16030  isacs2  16079  isacs1i  16083  sscres  16248  rescabs  16258  resscat  16277  funcres2c  16326  coffth  16361  rescfth  16362  ressffth  16363  catccatid  16517  catcisolem  16521  catciso  16522  catcoppccl  16523  catcfuccl  16524  catcxpccl  16612  yoniso  16690  isdrs2  16704  isacs3lem  16931  acsinfd  16945  acsdomd  16946  psssdm2  16980  tsrss  16988  idrespermg  17596  mvdco  17630  sylow2a  17799  lsmmod  17853  frgpnabllem2  18042  subrgpropd  18579  lssacs  18730  sralmod  18950  asplss  19092  ressmplbas  19219  subrgmpl  19223  opsrtoslem2  19248  mplind  19265  ressply1bas  19362  pf1rcl  19476  zringlpirlem2  19594  zringlpirlem3  19595  ofco2  20014  basdif0  20506  eltg4i  20513  ntrss2  20609  ntrin  20613  isopn3  20618  mreclatdemoBAD  20648  neiptoptop  20683  restbas  20710  resttopon  20713  restuni2  20719  restcld  20724  restfpw  20731  neitr  20732  ordtrest  20754  subbascn  20806  cnrest2r  20839  cnpresti  20840  cnprest  20841  lmss  20850  cnrmi  20912  restcnrm  20914  resthauslem  20915  fincmp  20944  imacmp  20948  fiuncmp  20955  cmpfi  20959  bwth  20961  cnconn  20973  iuncon  20979  clscon  20981  concompclo  20986  1stcrest  21004  subislly  21032  islly2  21035  cldllycmp  21046  hauspwdom  21052  kgeni  21088  llycmpkgen2  21101  1stckgenlem  21104  ptbasfi  21132  txcls  21155  ptclsg  21166  txcnp  21171  ptcnplem  21172  txtube  21191  txcmplem1  21192  txcmplem2  21193  txkgen  21203  xkopt  21206  xkococnlem  21210  txcon  21240  basqtop  21262  tgqtop  21263  kqdisj  21283  kqnrmlem1  21294  kqnrmlem2  21295  nrmhmph  21345  infil  21415  fbasrn  21436  trfg  21443  uzrest  21449  isufil2  21460  fmfnfmlem4  21509  hauspwpwf1  21539  txflf  21558  alexsubALTlem3  21601  alexsubALTlem4  21602  ptcmplem2  21605  tmdgsum2  21648  tsmsres  21695  tsmsxplem1  21704  ustexsym  21767  ustund  21773  trust  21781  utoptop  21786  restutop  21789  blres  21983  met2ndci  22074  metrest  22076  restmetu  22122  tgioo  22335  zdis  22355  reconnlem2  22366  reconn  22367  cnheibor  22489  lebnum  22498  cphsqrtcl  22712  tchcph  22761  cfilresi  22815  cfilres  22816  caussi  22817  causs  22818  minveclem4b  22923  minveclem4  22924  ovolfcl  22955  ovolfioo  22956  ovolficc  22957  ovolficcss  22958  ovolfsval  22959  ovolfsf  22960  ovollb  22967  ovoliunlem1  22990  ovolicc2lem1  23005  ovolicc2lem2  23006  ovolicc2lem3  23007  ovolicc2lem4  23008  ovolicc2lem5  23009  ovolicc2  23010  nulmbl  23023  voliunlem1  23038  ioombl1lem4  23049  ovolfs2  23058  uniiccdif  23065  uniioovol  23066  uniiccvol  23067  uniioombllem2a  23069  uniioombllem2  23070  uniioombllem3a  23071  uniioombllem3  23072  uniioombllem4  23073  uniioombllem5  23074  uniioombllem6  23075  uniioombl  23076  dyadmbllem  23086  dyadmbl  23087  opnmbllem  23088  volcn  23093  volivth  23094  vitalilem2  23097  vitalilem4  23099  mbfadd  23147  mbfsub  23148  i1fima  23164  i1fima2  23165  i1fd  23167  i1fadd  23181  i1fmul  23182  itg1addlem2  23183  itg1addlem4  23185  itg1addlem5  23186  i1fres  23191  mbfmul  23212  bddmulibl  23324  ellimc2  23360  ellimc3  23362  limcflf  23364  limcresi  23368  limciun  23377  dvreslem  23392  dvres2lem  23393  dvres3a  23397  cpnres  23419  dvaddbr  23420  dvmulbr  23421  dvmptres3  23438  lhop1lem  23493  ig1peu  23648  taylfvallem1  23828  tayl0  23833  rlimcnp2  24406  xrlimcnp  24408  ppisval  24543  chtf  24547  efchtcl  24550  chtge0  24551  ppinprm  24591  chtprm  24592  chtnprm  24593  chtwordi  24595  chtdif  24597  efchtdvds  24598  chtlepsi  24644  chtleppi  24648  pclogsum  24653  chpval2  24656  chpchtsum  24657  chpub  24658  2sqlem8  24864  2sqlem9  24865  chebbnd1lem1  24871  chtppilimlem1  24875  rplogsumlem2  24887  rpvmasumlem  24889  rplogsum  24929  dirith2  24930  axtgsegcon  25076  axtg5seg  25077  axtgbtwnid  25078  axtgpasch  25079  axtgcont1  25080  tglng  25155  perpneq  25323  ragperp  25326  chdmm1i  27522  chm0i  27535  ledii  27581  lejdii  27583  pjoml2i  27630  pjoml4i  27632  cmcmlem  27636  cmbr4i  27646  osumcori  27688  pjssmii  27726  mayete3i  27773  riesz4  28109  riesz1  28110  cnlnadjeu  28123  nmopadjlei  28133  pjclem1  28240  pjci  28245  mdbr3  28342  mdbr4  28343  dmdbr2  28348  dmdbr5  28353  ssmd2  28357  mdslj1i  28364  mdslj2i  28365  mdsl1i  28366  mdsl2bi  28368  mdslmd1lem1  28370  mdslmd1lem2  28371  mdslmd2i  28375  csmdsymi  28379  cvexchlem  28413  atomli  28427  atcvat4i  28442  inindif  28540  disjin2  28584  disjxpin  28585  imadifxp  28598  off2  28625  partfun  28660  resspos  28792  resstos  28793  submomnd  28843  suborng  28948  prsdm  29090  prsrn  29091  ordtrestNEW  29097  pnfneige0  29127  lmxrge0  29128  qqhnm  29164  qqhcn  29165  rrhre  29195  indf1ofs  29217  gsumesum  29250  esumlub  29251  esumcst  29254  esumpcvgval  29269  hasheuni  29276  esumcvg  29277  sigainb  29328  carsgclctunlem2  29510  sibfinima  29530  sibfof  29531  eulerpartlemelr  29548  eulerpartlemgh  29569  eulerpartlemgf  29570  eulerpartlemgs2  29571  eulerpartlemn  29572  probmeasb  29621  cndprob01  29626  bnj1293  29943  conpcon  30273  iccllyscon  30288  cvmsss2  30312  cvmcov2  30313  cvmopnlem  30316  cvmliftmolem2  30320  cvmlift2lem12  30352  mvrsfpw  30459  elmsta  30501  msubvrs  30513  mclsind  30523  nepss  30656  elrn3  30708  dfon2lem4  30737  frrlem4  30829  trer  31282  neiin  31299  neibastop1  31326  neibastop2lem  31327  topmeet  31331  filnetlem3  31347  bj-restpw  32025  bj-restb  32027  bj-restuni2  32031  bj-ablsscmn  32116  topdifinffinlem  32170  opnmbllem0  32414  mblfinlem4  32418  mbfposadd  32426  heibor1lem  32577  heiborlem1  32579  heiborlem3  32581  heiborlem10  32588  opidonOLD  32620  lshpinN  33093  lcvexchlem1  33138  lcvexchlem5  33142  pmod1i  33951  pmodN  33953  osumcllem7N  34065  pexmidlem4N  34076  dochdmj1  35496  dochexmidlem4  35569  lcfrlem25  35673  mapd1o  35754  mapdin  35768  elrfi  36074  elrfirn  36075  fnwe2lem2  36438  aomclem2  36442  lsmfgcl  36461  lmhmfgima  36471  lmhmfgsplit  36473  lmhmlnmsplit  36474  hbt  36518  acsfn1p  36587  trrelind  36775  iunrelexp0  36812  isotone2  37166  onfrALTlem3  37579  onfrALTlem2  37581  onfrALTlem3VD  37944  onfrALTlem2VD  37946  iunconlem2  37992  restuni6  38136  disjinfi  38174  inmap  38195  fsumiunss  38442  islptre  38486  sumnnodd  38497  limcresiooub  38509  limcresioolb  38510  limcleqr  38511  limclner  38518  limclr  38522  icccncfext  38573  fourierdlem20  38820  fourierdlem48  38847  fourierdlem49  38848  fourierdlem50  38849  fourierdlem76  38875  fourierdlem103  38902  fourierdlem104  38903  fourierdlem113  38912  fouriersw  38924  salgencntex  39037  sge0less  39085  sge0resplit  39099  sge0split  39102  sge0iunmptlemre  39108  sge0fodjrnlem  39109  caragencmpl  39225  ovolval2lem  39333  ovolval2  39334  ovolval3  39337  ovolval4lem2  39340  sssmf  39425  lidlssbas  41710  rnghmresfn  41753  rnghmsscmap  41764  rngchomrnghmresALTV  41786  rhmresfn  41799  rhmsscmap  41810  rhmsubclem4  41879
  Copyright terms: Public domain W3C validator