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

Theorem inss2 3826
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 3797 . 2 (𝐵𝐴) = (𝐴𝐵)
2 inss1 3825 . 2 (𝐵𝐴) ⊆ 𝐵
31, 2eqsstr3i 3628 1 (𝐴𝐵) ⊆ 𝐵
Colors of variables: wff setvar class
Syntax hints:  cin 3566  wss 3567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-in 3574  df-ss 3581
This theorem is referenced by:  difin0  4032  iunxdif3  4597  relin2  5227  relres  5414  ssrnres  5560  cnvcnv  5574  cnvcnvOLD  5575  ordin  5741  onfr  5751  ordelinel  5813  ordelinelOLD  5814  fnresin2  5994  fresaunres2  6063  ssimaex  6250  exfo  6363  ffvresb  6380  ofrfval  6890  ofval  6891  ofrval  6892  off  6897  ofres  6898  ofco  6902  offres  7148  fnwelem  7277  fnse  7279  tpostpos  7357  wfrlem4  7403  smores3  7435  tfrlem5  7461  erinxp  7806  pmresg  7870  nnfi  8138  ixpfi2  8249  f1opwfi  8255  dffi2  8314  elfiun  8321  marypha1lem  8324  ordtypelem3  8410  ordtypelem6  8413  ordtypelem7  8414  hartogslem1  8432  unxpwdom  8479  epfrs  8592  tcmin  8602  bnd2  8741  tskwe  8761  r0weon  8820  infxpenlem  8821  fodomfi2  8868  infpwfien  8870  cdainf  8999  ackbij1lem6  9032  ackbij1lem9  9035  ackbij1lem10  9036  ackbij1lem11  9037  ackbij1lem15  9041  ackbij1lem16  9042  ackbij1lem18  9044  ackbij1b  9046  sdom2en01  9109  fin23lem26  9132  fin23lem13  9139  isfin1-3  9193  fin56  9200  fin1a2lem9  9215  ttukeylem6  9321  brdom3  9335  brdom5  9336  brdom4  9337  fpwwe2lem8  9444  fpwwe2lem9  9445  fpwwe2lem12  9448  fpwwe2  9450  canthwelem  9457  gruima  9609  ingru  9622  gruina  9625  grur1a  9626  ltrelpi  9696  ltrelnq  9733  nqerf  9737  dedekindle  10186  fzfi  12754  xptrrel  13700  rexanuz  14066  limsupgord  14184  limsupcl  14185  limsupgf  14187  limsupgle  14189  rlimres  14270  lo1res  14271  o1of2  14324  o1rlimmul  14330  ackbijnn  14541  bitsinv1  15145  bitsinvp1  15152  sadcaddlem  15160  sadadd2lem  15162  sadadd3  15164  sadaddlem  15169  sadasslem  15173  sadeq  15175  smuval2  15185  smupval  15191  smueqlem  15193  prmrec  15607  isstruct2  15848  structcnvcnv  15852  ressbasss  15913  ressress  15919  restsspw  16073  pwsle  16133  submre  16246  isacs2  16295  isacs1i  16299  sscres  16464  rescabs  16474  resscat  16493  funcres2c  16542  coffth  16577  rescfth  16578  ressffth  16579  catccatid  16733  catcisolem  16737  catciso  16738  catcoppccl  16739  catcfuccl  16740  catcxpccl  16828  yoniso  16906  isdrs2  16920  isacs3lem  17147  acsinfd  17161  acsdomd  17162  psssdm2  17196  tsrss  17204  idrespermg  17812  mvdco  17846  sylow2a  18015  lsmmod  18069  frgpnabllem2  18258  subrgpropd  18795  lssacs  18948  sralmod  19168  asplss  19310  ressmplbas  19437  subrgmpl  19441  opsrtoslem2  19466  mplind  19483  ressply1bas  19580  pf1rcl  19694  zringlpirlem2  19814  zringlpirlem3  19815  ofco2  20238  basdif0  20738  eltg4i  20745  ntrss2  20842  ntrin  20846  isopn3  20851  mreclatdemoBAD  20881  neiptoptop  20916  restbas  20943  resttopon  20946  restuni2  20952  restcld  20957  restfpw  20964  neitr  20965  ordtrest  20987  subbascn  21039  cnrest2r  21072  cnpresti  21073  cnprest  21074  lmss  21083  cnrmi  21145  restcnrm  21147  resthauslem  21148  fincmp  21177  imacmp  21181  fiuncmp  21188  cmpfi  21192  bwth  21194  cnconn  21206  iunconn  21212  clsconn  21214  conncompclo  21219  1stcrest  21237  subislly  21265  islly2  21268  cldllycmp  21279  hauspwdom  21285  kgeni  21321  llycmpkgen2  21334  1stckgenlem  21337  ptbasfi  21365  txcls  21388  ptclsg  21399  txcnp  21404  ptcnplem  21405  txtube  21424  txcmplem1  21425  txcmplem2  21426  txkgen  21436  xkopt  21439  xkococnlem  21443  txconn  21473  basqtop  21495  tgqtop  21496  kqdisj  21516  kqnrmlem1  21527  kqnrmlem2  21528  nrmhmph  21578  infil  21648  fbasrn  21669  trfg  21676  uzrest  21682  isufil2  21693  fmfnfmlem4  21742  hauspwpwf1  21772  txflf  21791  alexsubALTlem3  21834  alexsubALTlem4  21835  ptcmplem2  21838  tmdgsum2  21881  tsmsres  21928  tsmsxplem1  21937  ustexsym  22000  ustund  22006  trust  22014  utoptop  22019  restutop  22022  blres  22217  met2ndci  22308  metrest  22310  restmetu  22356  tgioo  22580  zdis  22600  reconnlem2  22611  reconn  22612  cnheibor  22735  lebnum  22744  cphsqrtcl  22965  tchcph  23017  cfilresi  23074  cfilres  23075  caussi  23076  causs  23077  minveclem4b  23183  minveclem4  23184  ovolfcl  23216  ovolfioo  23217  ovolficc  23218  ovolficcss  23219  ovolfsval  23220  ovolfsf  23221  ovollb  23228  ovoliunlem1  23251  ovolicc2lem1  23266  ovolicc2lem2  23267  ovolicc2lem3  23268  ovolicc2lem4  23269  ovolicc2lem5  23270  ovolicc2  23271  nulmbl  23284  voliunlem1  23299  ioombl1lem4  23310  ovolfs2  23320  uniiccdif  23327  uniioovol  23328  uniiccvol  23329  uniioombllem2a  23331  uniioombllem2  23332  uniioombllem3a  23333  uniioombllem3  23334  uniioombllem4  23335  uniioombllem5  23336  uniioombllem6  23337  uniioombl  23338  dyadmbllem  23348  dyadmbl  23349  opnmbllem  23350  volcn  23355  volivth  23356  vitalilem2  23359  vitalilem4  23361  mbfadd  23409  mbfsub  23410  i1fima  23426  i1fima2  23427  i1fd  23429  i1fadd  23443  i1fmul  23444  itg1addlem2  23445  itg1addlem4  23447  itg1addlem5  23448  i1fres  23453  mbfmul  23474  bddmulibl  23586  ellimc2  23622  ellimc3  23624  limcflf  23626  limcresi  23630  limciun  23639  dvreslem  23654  dvres2lem  23655  dvres3a  23659  cpnres  23681  dvaddbr  23682  dvmulbr  23683  dvmptres3  23700  lhop1lem  23757  ig1peu  23912  taylfvallem1  24092  rlimcnp2  24674  xrlimcnp  24676  ppisval  24811  chtf  24815  efchtcl  24818  chtge0  24819  ppinprm  24859  chtprm  24860  chtnprm  24861  chtwordi  24863  chtdif  24865  efchtdvds  24866  chtlepsi  24912  chtleppi  24916  pclogsum  24921  chpval2  24924  chpchtsum  24925  chpub  24926  2sqlem8  25132  2sqlem9  25133  chebbnd1lem1  25139  chtppilimlem1  25143  rplogsumlem2  25155  rpvmasumlem  25157  rplogsum  25197  dirith2  25198  axtgsegcon  25344  axtg5seg  25345  axtgbtwnid  25346  axtgpasch  25347  axtgcont1  25348  tglng  25422  perpneq  25590  ragperp  25593  chdmm1i  28306  chm0i  28319  ledii  28365  lejdii  28367  pjoml2i  28414  pjoml4i  28416  cmcmlem  28420  cmbr4i  28430  osumcori  28472  pjssmii  28510  mayete3i  28557  riesz4  28893  riesz1  28894  cnlnadjeu  28907  nmopadjlei  28917  pjclem1  29024  pjci  29029  mdbr3  29126  mdbr4  29127  dmdbr2  29132  dmdbr5  29137  ssmd2  29141  mdslj1i  29148  mdslj2i  29149  mdsl1i  29150  mdsl2bi  29152  mdslmd1lem1  29154  mdslmd1lem2  29155  mdslmd2i  29159  csmdsymi  29163  cvexchlem  29197  atomli  29211  atcvat4i  29226  inindif  29325  difininv  29326  disjxpin  29373  imadifxp  29386  off2  29416  resspos  29633  resstos  29634  submomnd  29684  suborng  29789  prsdm  29934  prsrn  29935  ordtrestNEW  29941  pnfneige0  29971  lmxrge0  29972  qqhnm  30008  qqhcn  30009  rrhre  30039  indsumin  30058  indf1ofs  30062  gsumesum  30095  esumlub  30096  esumcst  30099  esumpcvgval  30114  hasheuni  30121  esumcvg  30122  sigainb  30173  carsgclctunlem2  30355  sibfinima  30375  sibfof  30376  eulerpartlemelr  30393  eulerpartlemgh  30414  eulerpartlemgf  30415  eulerpartlemgs2  30416  eulerpartlemn  30417  probmeasb  30466  cndprob01  30471  hashreprin  30672  reprfi2  30675  breprexpnat  30686  hgt750lemd  30700  hgt750lema  30709  tgoldbachgtde  30712  tgoldbachgtda  30713  tgoldbachgt  30715  bnj1293  30861  connpconn  31191  iccllysconn  31206  cvmsss2  31230  cvmcov2  31231  cvmopnlem  31234  cvmliftmolem2  31238  cvmlift2lem12  31270  mvrsfpw  31377  elmsta  31419  msubvrs  31431  mclsind  31441  nepss  31574  elrn3  31628  dfon2lem4  31665  frrlem4  31757  nosupbnd2  31836  trer  32285  neiin  32302  neibastop1  32329  neibastop2lem  32330  topmeet  32334  filnetlem3  32350  bj-disj2r  32988  bj-restpw  33020  bj-restb  33022  bj-restuni2  33026  bj-ablsscmn  33111  topdifinffinlem  33166  opnmbllem0  33416  mblfinlem4  33420  mbfposadd  33428  heibor1lem  33579  heiborlem1  33581  heiborlem3  33583  heiborlem10  33590  opidonOLD  33622  lshpinN  34095  lcvexchlem1  34140  lcvexchlem5  34144  pmod1i  34953  pmodN  34955  osumcllem7N  35067  pexmidlem4N  35078  dochdmj1  36498  dochexmidlem4  36571  lcfrlem25  36675  mapd1o  36756  mapdin  36770  elrfi  37076  elrfirn  37077  fnwe2lem2  37440  aomclem2  37444  lsmfgcl  37463  lmhmfgima  37473  lmhmfgsplit  37475  lmhmlnmsplit  37476  hbt  37519  acsfn1p  37588  trrelind  37776  iunrelexp0  37813  isotone2  38167  onfrALTlem3  38579  onfrALTlem2  38581  onfrALTlem3VD  38943  onfrALTlem2VD  38945  iunconnlem2  38991  restuni6  39125  disjinfi  39196  inmap  39217  dmresss  39252  fnfvimad  39275  fnfvima2  39294  fsumiunss  39607  islptre  39651  sumnnodd  39662  limcresiooub  39674  limcresioolb  39675  limcleqr  39676  limclner  39683  limclr  39687  limsuplesup  39731  limsuppnfdlem  39733  limsupres  39737  liminfgord  39780  liminfgf  39784  liminfcl  39789  limsupresxr  39792  liminfresxr  39793  liminfval2  39794  liminflelimsuplem  39801  liminfvalxr  39809  icccncfext  39863  fourierdlem20  40107  fourierdlem48  40134  fourierdlem49  40135  fourierdlem50  40136  fourierdlem76  40162  fourierdlem103  40189  fourierdlem104  40190  fourierdlem113  40199  fouriersw  40211  salgencntex  40324  sge0less  40372  sge0resplit  40386  sge0split  40389  sge0iunmptlemre  40395  sge0fodjrnlem  40396  caragencmpl  40512  ovolval2lem  40620  ovolval2  40621  ovolval3  40624  ovolval4lem2  40627  sssmf  40710  lidlssbas  41687  rnghmresfn  41728  rnghmsscmap  41739  rngchomrnghmresALTV  41761  rhmresfn  41774  rhmsscmap  41785  rhmsubclem4  41854
  Copyright terms: Public domain W3C validator