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

Theorem inss2 3554
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  |-  ( A  i^i  B )  C_  B

Proof of Theorem inss2
StepHypRef Expression
1 incom 3525 . 2  |-  ( B  i^i  A )  =  ( A  i^i  B
)
2 inss1 3553 . 2  |-  ( B  i^i  A )  C_  B
31, 2eqsstr3i 3371 1  |-  ( A  i^i  B )  C_  B
Colors of variables: wff set class
Syntax hints:    i^i cin 3311    C_ wss 3312
This theorem is referenced by:  difin0  3693  ordin  4603  onfr  4612  ordelinel  4672  relin2  4985  relres  5166  ssrnres  5301  cnvcnv  5315  fnresin2  5552  fresaunres2  5607  ssimaex  5780  exfo  5879  ffvresb  5892  ofrfval  6305  ofval  6306  ofrval  6307  offres  6311  off  6312  ofres  6313  ofco  6316  fnwelem  6453  fnse  6455  tpostpos  6491  smores3  6607  erinxp  6970  pmresg  7033  nnfi  7291  ixpfi2  7397  f1opwfi  7402  dffi2  7420  elfiun  7427  marypha1lem  7430  ordtypelem3  7481  ordtypelem6  7484  ordtypelem7  7485  hartogslem1  7503  unxpwdom  7549  epfrs  7659  tcmin  7672  bnd2  7809  tskwe  7829  r0weon  7886  infxpenlem  7887  fodomfi2  7933  infpwfien  7935  cdainf  8064  ackbij1lem6  8097  ackbij1lem9  8100  ackbij1lem10  8101  ackbij1lem11  8102  ackbij1lem15  8106  ackbij1lem16  8107  ackbij1lem18  8109  ackbij1b  8111  sdom2en01  8174  fin23lem26  8197  fin23lem13  8204  isfin1-3  8258  fin56  8265  fin1a2lem9  8280  ttukeylem6  8386  brdom3  8398  brdom5  8399  brdom4  8400  fpwwe2lem8  8504  fpwwe2lem9  8505  fpwwe2lem12  8508  fpwwe2  8510  canthwelem  8517  gruima  8669  ingru  8682  gruina  8685  grur1a  8686  ltrelpi  8758  ltrelnq  8795  nqerf  8799  fzfi  11303  rexanuz  12141  limsupgord  12258  limsupcl  12259  limsupgf  12261  limsupgle  12263  rlimres  12344  lo1res  12345  o1of2  12398  o1rlimmul  12404  ackbijnn  12599  bitsinv1  12946  bitsinvp1  12953  sadcaddlem  12961  sadadd2lem  12963  sadadd3  12965  sadaddlem  12970  sadasslem  12974  sadeq  12976  smuval2  12986  smupval  12992  smueqlem  12994  prmrec  13282  isstruct2  13470  structcnvcnv  13472  ressbasss  13513  ressress  13518  restsspw  13651  pwsle  13706  submre  13822  isacs2  13870  isacs1i  13874  sscres  14015  rescabs  14025  resscat  14041  funcres2c  14090  coffth  14125  rescfth  14126  ressffth  14127  catccatid  14249  catcisolem  14253  catciso  14254  catcoppccl  14255  catcfuccl  14256  catcxpccl  14296  yoniso  14374  isdrs2  14388  isacs3lem  14584  acsinfd  14598  acsdomd  14599  psssdm2  14639  tsrss  14647  sylow2a  15245  lsmmod  15299  frgpnabllem2  15477  subrgpropd  15894  lssacs  16035  sralmod  16250  asplss  16380  ressmplbas  16511  subrgmpl  16515  opsrtoslem2  16537  mplind  16554  ressply1bas  16615  zlpirlem2  16761  zlpirlem3  16762  basdif0  17010  eltg4i  17017  ntrss2  17113  ntrin  17117  isopn3  17122  mreclatdemo  17152  neiptoptop  17187  restbas  17214  resttopon  17217  restuni2  17223  restcld  17228  restfpw  17235  neitr  17236  ordtrest  17258  subbascn  17310  cnrest2r  17343  cnpresti  17344  cnprest  17345  lmss  17354  cnrmi  17416  restcnrm  17418  resthauslem  17419  fincmp  17448  imacmp  17452  fiuncmp  17459  cmpfi  17463  cnconn  17477  iuncon  17483  clscon  17485  concompclo  17490  1stcrest  17508  subislly  17536  islly2  17539  cldllycmp  17550  hauspwdom  17556  kgeni  17561  llycmpkgen2  17574  1stckgenlem  17577  ptbasfi  17605  txcls  17628  ptclsg  17639  txcnp  17644  ptcnplem  17645  txtube  17664  txcmplem1  17665  txcmplem2  17666  txkgen  17676  xkopt  17679  xkococnlem  17683  txcon  17713  basqtop  17735  tgqtop  17736  kqdisj  17756  kqnrmlem1  17767  kqnrmlem2  17768  nrmhmph  17818  infil  17887  fbasrn  17908  trfg  17915  uzrest  17921  isufil2  17932  fmfnfmlem4  17981  hauspwpwf1  18011  txflf  18030  alexsubALTlem3  18072  alexsubALTlem4  18073  ptcmplem2  18076  tmdgsum2  18118  tsmsres  18165  tsmsxplem1  18174  ustexsym  18237  ustund  18243  trust  18251  utoptop  18256  restutop  18259  blres  18453  met2ndci  18544  metrest  18546  restmetu  18609  tgioo  18819  zdis  18839  reconnlem2  18850  reconn  18851  cnheibor  18972  lebnum  18981  nmoleub2lem3  19115  nmoleub3  19119  cphsqrcl  19139  tchcph  19186  cfilresi  19240  cfilres  19241  caussi  19242  causs  19243  minveclem4b  19324  minveclem4  19325  ovolfcl  19355  ovolfioo  19356  ovolficc  19357  ovolficcss  19358  ovolfsval  19359  ovolfsf  19360  ovollb  19367  ovoliunlem1  19390  ovolicc2lem1  19405  ovolicc2lem2  19406  ovolicc2lem3  19407  ovolicc2lem4  19408  ovolicc2lem5  19409  ovolicc2  19410  nulmbl  19422  voliunlem1  19436  ioombl1lem4  19447  ovolfs2  19455  uniiccdif  19462  uniioovol  19463  uniiccvol  19464  uniioombllem2a  19466  uniioombllem2  19467  uniioombllem3a  19468  uniioombllem3  19469  uniioombllem4  19470  uniioombllem5  19471  uniioombllem6  19472  uniioombl  19473  dyadmbllem  19483  dyadmbl  19484  opnmbllem  19485  volcn  19490  volivth  19491  vitalilem2  19493  vitalilem4  19495  mbfadd  19545  mbfsub  19546  i1fima  19562  i1fima2  19563  i1fd  19565  i1fadd  19579  i1fmul  19580  itg1addlem2  19581  itg1addlem4  19583  itg1addlem5  19584  i1fres  19589  mbfmul  19610  itg2cnlem2  19646  bddmulibl  19722  ellimc2  19756  ellimc3  19758  limcflf  19760  limcresi  19764  limciun  19773  dvreslem  19788  dvres2lem  19789  dvres3a  19793  cpnres  19815  dvaddbr  19816  dvmulbr  19817  dvmptres3  19834  lhop1lem  19889  pf1rcl  19961  ig1peu  20086  taylfvallem1  20265  tayl0  20270  rlimcnp2  20797  xrlimcnp  20799  ppisval  20878  chtf  20883  efchtcl  20886  chtge0  20887  ppinprm  20927  chtprm  20928  chtnprm  20929  chtwordi  20931  chtdif  20933  efchtdvds  20934  chtlepsi  20982  chtleppi  20986  pclogsum  20991  chpval2  20994  chpchtsum  20995  chpub  20996  2sqlem8  21148  2sqlem9  21149  chebbnd1lem1  21155  chtppilimlem1  21159  rplogsumlem2  21171  rpvmasumlem  21173  rplogsum  21213  dirith2  21214  issubgo  21883  opidon  21902  chdmm1i  22971  chm0i  22984  ledii  23030  lejdii  23032  pjoml2i  23079  pjoml4i  23081  cmcmlem  23085  cmbr4i  23095  osumcori  23137  pjssmii  23175  mayete3i  23222  mayete3iOLD  23223  riesz4  23559  riesz1  23560  cnlnadjeu  23573  nmopadjlei  23583  pjclem1  23690  pjci  23695  mdbr3  23792  mdbr4  23793  dmdbr2  23798  dmdbr5  23803  ssmd2  23807  mdslj1i  23814  mdslj2i  23815  mdsl1i  23816  mdsl2bi  23818  mdslmd1lem1  23820  mdslmd1lem2  23821  mdslmd2i  23825  csmdsymi  23829  cvexchlem  23863  atomli  23877  atcvat4i  23892  disjxpin  24020  imadifxp  24030  suppss2f  24041  off2  24046  partfun  24079  resspos  24179  resstos  24180  subofld  24237  pnfneige0  24328  lmxrge0  24329  qqhnm  24366  qqhcn  24367  rrhre  24379  indf1ofs  24415  gsumesum  24443  esumlub  24444  esumcst  24447  esumpcvgval  24460  hasheuni  24467  esumcvg  24468  sigainb  24511  measunl  24562  sibfof  24646  probdif  24670  probmeasb  24680  cndprob01  24685  conpcon  24914  iccllyscon  24929  cvmsss2  24953  cvmcov2  24954  cvmopnlem  24957  cvmliftmolem2  24961  cvmlift2lem12  24993  nepss  25167  dedekindle  25180  elrn3  25378  dfon2lem4  25405  wfrlem4  25533  frrlem4  25577  mblfinlem3  26236  mbfposadd  26244  trer  26310  neiin  26326  neibastop1  26379  neibastop2lem  26380  topmeet  26384  filnetlem3  26400  heibor1lem  26509  heiborlem1  26511  heiborlem3  26513  heiborlem10  26520  elrfi  26739  elrfirn  26740  fnwe2lem2  27117  aomclem2  27121  lsmfgcl  27140  lmhmfgima  27150  lmhmfgsplit  27152  lmhmlnmsplit  27153  uvcff  27208  hbt  27302  mvdco  27356  acsfn1p  27475  onfrALTlem3  28567  onfrALTlem2  28569  onfrALTlem3VD  28936  onfrALTlem2VD  28938  iunconlem2  28984  bnj1293  29125  lshpinN  29724  lcvexchlem1  29769  lcvexchlem5  29773  pmod1i  30582  pmodN  30584  osumcllem7N  30696  pexmidlem4N  30707  dochdmj1  32125  dochexmidlem4  32198  lcfrlem25  32302  mapd1o  32383  mapdin  32397
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator