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

Theorem inss2 3867
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 3838 . 2 (𝐵𝐴) = (𝐴𝐵)
2 inss1 3866 . 2 (𝐵𝐴) ⊆ 𝐵
31, 2eqsstr3i 3669 1 (𝐴𝐵) ⊆ 𝐵
Colors of variables: wff setvar class
Syntax hints:  cin 3606  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614  df-ss 3621
This theorem is referenced by:  difin0  4074  iunxdif3  4638  relin2  5270  relres  5461  ssrnres  5607  cnvcnv  5621  cnvcnvOLD  5622  ordin  5791  onfr  5801  ordelinel  5863  ordelinelOLD  5864  fnresin2  6044  fresaunres2  6114  ssimaex  6302  exfo  6417  ffvresb  6434  ofrfval  6947  ofval  6948  ofrval  6949  off  6954  ofres  6955  ofco  6959  offres  7205  fnwelem  7337  fnse  7339  tpostpos  7417  wfrlem4  7463  smores3  7495  tfrlem5  7521  erinxp  7864  pmresg  7927  nnfi  8194  ixpfi2  8305  f1opwfi  8311  dffi2  8370  elfiun  8377  marypha1lem  8380  ordtypelem3  8466  ordtypelem6  8469  ordtypelem7  8470  hartogslem1  8488  unxpwdom  8535  epfrs  8645  tcmin  8655  bnd2  8794  tskwe  8814  r0weon  8873  infxpenlem  8874  fodomfi2  8921  infpwfien  8923  cdainf  9052  ackbij1lem6  9085  ackbij1lem9  9088  ackbij1lem10  9089  ackbij1lem11  9090  ackbij1lem15  9094  ackbij1lem16  9095  ackbij1lem18  9097  ackbij1b  9099  sdom2en01  9162  fin23lem26  9185  fin23lem13  9192  isfin1-3  9246  fin56  9253  fin1a2lem9  9268  ttukeylem6  9374  brdom3  9388  brdom5  9389  brdom4  9390  fpwwe2lem8  9497  fpwwe2lem9  9498  fpwwe2lem12  9501  fpwwe2  9503  canthwelem  9510  gruima  9662  ingru  9675  gruina  9678  grur1a  9679  ltrelpi  9749  ltrelnq  9786  nqerf  9790  dedekindle  10239  fzfi  12811  xptrrel  13765  rexanuz  14129  limsupgord  14247  limsupcl  14248  limsupgf  14250  limsupgle  14252  rlimres  14333  lo1res  14334  o1of2  14387  o1rlimmul  14393  ackbijnn  14604  bitsinv1  15211  bitsinvp1  15218  sadcaddlem  15226  sadadd2lem  15228  sadadd3  15230  sadaddlem  15235  sadasslem  15239  sadeq  15241  smuval2  15251  smupval  15257  smueqlem  15259  prmrec  15673  isstruct2  15914  structcnvcnv  15918  ressbasss  15979  ressress  15985  restsspw  16139  pwsle  16199  submre  16312  isacs2  16361  isacs1i  16365  sscres  16530  rescabs  16540  resscat  16559  funcres2c  16608  coffth  16643  rescfth  16644  ressffth  16645  catccatid  16799  catcisolem  16803  catciso  16804  catcoppccl  16805  catcfuccl  16806  catcxpccl  16894  yoniso  16972  isdrs2  16986  isacs3lem  17213  acsinfd  17227  acsdomd  17228  psssdm2  17262  tsrss  17270  idrespermg  17877  mvdco  17911  sylow2a  18080  lsmmod  18134  frgpnabllem2  18323  subrgpropd  18862  lssacs  19015  sralmod  19235  asplss  19377  ressmplbas  19504  subrgmpl  19508  opsrtoslem2  19533  mplind  19550  ressply1bas  19647  pf1rcl  19761  zringlpirlem2  19881  zringlpirlem3  19882  ofco2  20305  basdif0  20805  eltg4i  20812  ntrss2  20909  ntrin  20913  isopn3  20918  mreclatdemoBAD  20948  neiptoptop  20983  restbas  21010  resttopon  21013  restuni2  21019  restcld  21024  restfpw  21031  neitr  21032  ordtrest  21054  subbascn  21106  cnrest2r  21139  cnpresti  21140  cnprest  21141  lmss  21150  cnrmi  21212  restcnrm  21214  resthauslem  21215  fincmp  21244  imacmp  21248  fiuncmp  21255  cmpfi  21259  bwth  21261  cnconn  21273  iunconn  21279  clsconn  21281  conncompclo  21286  1stcrest  21304  subislly  21332  islly2  21335  cldllycmp  21346  hauspwdom  21352  kgeni  21388  llycmpkgen2  21401  1stckgenlem  21404  ptbasfi  21432  txcls  21455  ptclsg  21466  txcnp  21471  ptcnplem  21472  txtube  21491  txcmplem1  21492  txcmplem2  21493  txkgen  21503  xkopt  21506  xkococnlem  21510  txconn  21540  basqtop  21562  tgqtop  21563  kqdisj  21583  kqnrmlem1  21594  kqnrmlem2  21595  nrmhmph  21645  infil  21714  fbasrn  21735  trfg  21742  uzrest  21748  isufil2  21759  fmfnfmlem4  21808  hauspwpwf1  21838  txflf  21857  alexsubALTlem3  21900  alexsubALTlem4  21901  ptcmplem2  21904  tmdgsum2  21947  tsmsres  21994  tsmsxplem1  22003  ustexsym  22066  ustund  22072  trust  22080  utoptop  22085  restutop  22088  blres  22283  met2ndci  22374  metrest  22376  restmetu  22422  tgioo  22646  zdis  22666  reconnlem2  22677  reconn  22678  cnheibor  22801  lebnum  22810  cphsqrtcl  23030  tchcph  23082  cfilresi  23139  cfilres  23140  caussi  23141  causs  23142  minveclem4b  23248  minveclem4  23249  ovolfcl  23281  ovolfioo  23282  ovolficc  23283  ovolficcss  23284  ovolfsval  23285  ovolfsf  23286  ovollb  23293  ovoliunlem1  23316  ovolicc2lem1  23331  ovolicc2lem2  23332  ovolicc2lem3  23333  ovolicc2lem4  23334  ovolicc2lem5  23335  ovolicc2  23336  nulmbl  23349  voliunlem1  23364  ioombl1lem4  23375  ovolfs2  23385  uniiccdif  23392  uniioovol  23393  uniiccvol  23394  uniioombllem2a  23396  uniioombllem2  23397  uniioombllem3a  23398  uniioombllem3  23399  uniioombllem4  23400  uniioombllem5  23401  uniioombllem6  23402  uniioombl  23403  dyadmbllem  23413  dyadmbl  23414  opnmbllem  23415  volcn  23420  volivth  23421  vitalilem2  23423  vitalilem4  23425  mbfadd  23473  mbfsub  23474  i1fima  23490  i1fima2  23491  i1fd  23493  i1fadd  23507  i1fmul  23508  itg1addlem2  23509  itg1addlem4  23511  itg1addlem5  23512  i1fres  23517  mbfmul  23538  bddmulibl  23650  ellimc2  23686  ellimc3  23688  limcflf  23690  limcresi  23694  limciun  23703  dvreslem  23718  dvres2lem  23719  dvres3a  23723  cpnres  23745  dvaddbr  23746  dvmulbr  23747  dvmptres3  23764  lhop1lem  23821  ig1peu  23976  taylfvallem1  24156  rlimcnp2  24738  xrlimcnp  24740  ppisval  24875  chtf  24879  efchtcl  24882  chtge0  24883  ppinprm  24923  chtprm  24924  chtnprm  24925  chtwordi  24927  chtdif  24929  efchtdvds  24930  chtlepsi  24976  chtleppi  24980  pclogsum  24985  chpval2  24988  chpchtsum  24989  chpub  24990  2sqlem8  25196  2sqlem9  25197  chebbnd1lem1  25203  chtppilimlem1  25207  rplogsumlem2  25219  rpvmasumlem  25221  rplogsum  25261  dirith2  25262  axtgsegcon  25408  axtg5seg  25409  axtgbtwnid  25410  axtgpasch  25411  axtgcont1  25412  tglng  25486  perpneq  25654  ragperp  25657  chdmm1i  28464  chm0i  28477  ledii  28523  lejdii  28525  pjoml2i  28572  pjoml4i  28574  cmcmlem  28578  cmbr4i  28588  osumcori  28630  pjssmii  28668  mayete3i  28715  riesz4  29051  riesz1  29052  cnlnadjeu  29065  nmopadjlei  29075  pjclem1  29182  pjci  29187  mdbr3  29284  mdbr4  29285  dmdbr2  29290  dmdbr5  29295  ssmd2  29299  mdslj1i  29306  mdslj2i  29307  mdsl1i  29308  mdsl2bi  29310  mdslmd1lem1  29312  mdslmd1lem2  29313  mdslmd2i  29317  csmdsymi  29321  cvexchlem  29355  atomli  29369  atcvat4i  29384  inindif  29479  difininv  29480  disjxpin  29527  imadifxp  29540  off2  29571  resspos  29787  resstos  29788  submomnd  29838  suborng  29943  prsdm  30088  prsrn  30089  ordtrestNEW  30095  pnfneige0  30125  lmxrge0  30126  qqhnm  30162  qqhcn  30163  rrhre  30193  indsumin  30212  indf1ofs  30216  gsumesum  30249  esumlub  30250  esumcst  30253  esumpcvgval  30268  hasheuni  30275  esumcvg  30276  sigainb  30327  carsgclctunlem2  30509  sibfinima  30529  sibfof  30530  eulerpartlemelr  30547  eulerpartlemgh  30568  eulerpartlemgf  30569  eulerpartlemgs2  30570  eulerpartlemn  30571  probmeasb  30620  cndprob01  30625  hashreprin  30826  reprfi2  30829  breprexpnat  30840  hgt750lemd  30854  hgt750lema  30863  tgoldbachgtde  30866  tgoldbachgtda  30867  tgoldbachgt  30869  bnj1293  31013  connpconn  31343  iccllysconn  31358  cvmsss2  31382  cvmcov2  31383  cvmopnlem  31386  cvmliftmolem2  31390  cvmlift2lem12  31422  mvrsfpw  31529  elmsta  31571  msubvrs  31583  mclsind  31593  nepss  31725  elrn3  31778  dfon2lem4  31815  nosupbnd2  31987  trer  32435  neiin  32452  neibastop1  32479  neibastop2lem  32480  topmeet  32484  filnetlem3  32500  bj-disj2r  33138  bj-restpw  33170  bj-restb  33172  bj-restuni2  33176  bj-ablsscmn  33270  topdifinffinlem  33325  opnmbllem0  33575  mblfinlem4  33579  mbfposadd  33587  heibor1lem  33738  heiborlem1  33740  heiborlem3  33742  heiborlem10  33749  opidonOLD  33781  lshpinN  34594  lcvexchlem1  34639  lcvexchlem5  34643  pmod1i  35452  pmodN  35454  osumcllem7N  35566  pexmidlem4N  35577  dochdmj1  36996  dochexmidlem4  37069  lcfrlem25  37173  mapd1o  37254  mapdin  37268  elrfi  37574  elrfirn  37575  fnwe2lem2  37938  aomclem2  37942  lsmfgcl  37961  lmhmfgima  37971  lmhmfgsplit  37973  lmhmlnmsplit  37974  hbt  38017  acsfn1p  38086  trrelind  38274  iunrelexp0  38311  isotone2  38664  onfrALTlem3  39076  onfrALTlem2  39078  onfrALTlem3VD  39437  onfrALTlem2VD  39439  iunconnlem2  39485  restuni6  39619  disjinfi  39694  inmap  39715  dmresss  39750  fnfvimad  39773  fnfvima2  39792  fsumiunss  40125  islptre  40169  sumnnodd  40180  limcresiooub  40192  limcresioolb  40193  limcleqr  40194  limclner  40201  limclr  40205  limsuplesup  40249  limsuppnfdlem  40251  limsupres  40255  liminfgord  40304  liminfgf  40308  liminfcl  40313  limsupresxr  40316  liminfresxr  40317  liminfval2  40318  liminflelimsuplem  40325  liminfvalxr  40333  icccncfext  40418  fourierdlem20  40662  fourierdlem48  40689  fourierdlem49  40690  fourierdlem50  40691  fourierdlem76  40717  fourierdlem103  40744  fourierdlem104  40745  fourierdlem113  40754  fouriersw  40766  salgencntex  40879  sge0less  40927  sge0resplit  40941  sge0split  40944  sge0iunmptlemre  40950  sge0fodjrnlem  40951  caragencmpl  41070  ovolval2lem  41178  ovolval2  41179  ovolval3  41182  ovolval4lem2  41185  sssmf  41268  lidlssbas  42247  rnghmresfn  42288  rnghmsscmap  42299  rngchomrnghmresALTV  42321  rhmresfn  42334  rhmsscmap  42345  rhmsubclem4  42414
  Copyright terms: Public domain W3C validator