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

Theorem inss1 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
inss1 (𝐴𝐵) ⊆ 𝐴

Proof of Theorem inss1
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 elinel1 3757 . 2 (𝑥 ∈ (𝐴𝐵) → 𝑥𝐴)
21ssriv 3568 1 (𝐴𝐵) ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  cin 3535  wss 3536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
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 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-v 3171  df-in 3543  df-ss 3550
This theorem is referenced by:  inss2  3792  ssinss1  3799  unabs  3812  nssinpss  3814  dfin4  3822  inv1  3918  disjdif  3988  uniintsn  4440  wefrc  5019  relin1  5145  resss  5326  resmpt3  5354  cnvcnvss  5490  predss  5587  ordtri3or  5655  onfr  5663  ordelinel  5725  ordelinelOLD  5726  funin  5862  funimass2  5869  fnresin1  5902  fnres  5904  fresin  5968  fresaun  5970  fresaunres2  5971  nfvres  6116  ssimaex  6155  fneqeql2  6216  funiunfv  6385  isoini2  6464  ofrfval  6777  ofval  6778  ofrval  6779  off  6784  ofres  6785  ofco  6789  fparlem3  7140  fparlem4  7141  wfrlem4  7279  smores  7310  smores2  7312  tfrlem5  7337  pmresg  7745  sbthlem7  7935  sbthcl  7941  infi  8043  imafi  8116  ixpfi2  8121  unifpw  8126  f1opwfi  8127  fival  8175  fi0  8183  dffi2  8186  elfiun  8193  dffi3  8194  marypha1lem  8196  ordtypelem3  8282  ordtypelem4  8283  ordtypelem6  8285  ordtypelem7  8286  ordtypelem8  8287  wdomima2g  8348  epfrs  8464  tskwe  8633  r0weon  8692  fodomfi2  8740  infpwfien  8742  ackbij1lem6  8904  ackbij1lem9  8907  ackbij1lem10  8908  ackbij1lem11  8909  ackbij1lem15  8913  ackbij1lem16  8914  fin23lem24  9001  fin23lem26  9004  fin23lem23  9005  fin23lem22  9006  fin23lem19  9015  isfin1-3  9065  ttukeylem6  9193  brdom3  9205  brdom5  9206  brdom4  9207  imadomg  9211  fpwwe2lem12  9316  canthp1lem2  9328  wunin  9388  tskin  9434  gruima  9477  ingru  9490  gruina  9493  grur1a  9494  nqerf  9605  nqerrel  9607  dedekindle  10049  hashun3  12983  hashin  13009  hashdif  13011  xptrrel  13510  rexanuz  13876  limsupgle  13999  rlimres  14080  lo1res  14081  lo1resb  14086  rlimresb  14087  o1resb  14088  lo1eq  14090  rlimeq  14091  o1of2  14134  o1rlimmul  14140  isercolllem2  14187  isercolllem3  14188  isercoll  14189  ackbijnn  14342  incexclem  14350  incexc  14351  bitsinvp1  14952  sadcaddlem  14960  sadadd2lem  14962  sadadd3  14964  sadaddlem  14969  sadasslem  14973  sadeq  14975  bitsres  14976  smuval2  14985  smupval  14991  smueqlem  14993  smumul  14996  ramub2  15499  ramub1lem2  15512  fvsetsid  15665  ressinbas  15706  ressress  15708  submre  16031  submrc  16054  isacs2  16080  isacs1i  16084  mreacs  16085  acsfn  16086  invss  16187  sscres  16249  coffth  16362  catcisolem  16522  catciso  16523  catcoppccl  16524  catcfuccl  16525  catcxpccl  16613  isdrs2  16705  isacs3lem  16932  isacs5lem  16935  acsfiindd  16943  psss  16980  psssdm2  16981  tsrss  16989  tsrdir  17004  resscntz  17530  sylow2a  17800  lsmmod  17854  frgpnabllem2  18043  gsumzres  18076  gsumzaddlem  18087  dprddisj2  18204  ablfac1eu  18238  ablfac2  18254  isunit  18423  lspextmo  18820  2idlval  18997  aspsubrg  19095  psrbagsn  19259  mplind  19266  zringlpirlem2  19595  pjfval  19808  pjpm  19810  ofco2  20015  basdif0  20507  tgval2  20510  eltg3  20516  tgcl  20523  tgdom  20532  tgidm  20534  ppttop  20560  epttop  20562  ntropn  20602  ntrin  20614  mretopd  20645  mreclatdemoBAD  20649  neiptoptop  20684  restbas  20711  restfpw  20732  neitr  20733  restcls  20734  ordtrest  20755  subbascn  20807  cncls  20827  cnpresti  20841  cnprest  20842  fincmp  20945  cmpsublem  20951  cmpsub  20952  fiuncmp  20956  indiscon  20970  connsub  20973  cnconn  20974  iunconlem  20979  clscon  20982  concompclo  20987  islly2  21036  cldllycmp  21047  kgentopon  21090  llycmpkgen2  21102  1stckgenlem  21105  ptbasfi  21133  txcls  21156  txcnp  21172  ptcnplem  21173  txcnmpt  21176  txcmplem2  21194  hausdiag  21197  txkgen  21204  xkopt  21207  xkococnlem  21211  txcon  21241  qtoptop2  21251  basqtop  21263  tgqtop  21264  kqnrmlem1  21295  kqnrmlem2  21296  nrmhmph  21346  fbssfi  21390  filin  21407  infil  21416  fbasrn  21437  fgtr  21443  ufprim  21462  flimrest  21536  hauspwpwf1  21540  txflf  21559  fclsrest  21577  alexsubALTlem3  21602  alexsubALTlem4  21603  ptcmplem5  21609  tsmsres  21696  tsmsxplem1  21705  ustund  21774  trust  21782  utoptop  21787  restutop  21790  cfiluweak  21848  xmetres  21917  metres  21918  blin2  21982  blbas  21983  blres  21984  setsmstopn  22031  met2ndci  22075  metrest  22077  ressxms  22078  tgioo  22336  xrsmopn  22352  zdis  22356  reconnlem1  22366  reconnlem2  22367  xrge0tsms  22374  cnheibor  22490  lebnum  22499  nmoleub2lem  22650  nmoleub2lem2  22652  nmhmcn  22656  tchcph  22762  cfilresi  22816  cfilres  22817  caussi  22818  causs  22819  relcmpcmet  22837  minveclem4a  22923  minveclem4  22925  ismbl2  23016  cmmbl  23023  nulmbl2  23025  unmbl  23026  shftmbl  23027  volinun  23035  voliunlem1  23039  voliunlem2  23040  ioombl1lem4  23050  ioombl1  23051  ioorcl  23065  uniioombllem2  23071  uniioombllem3  23073  uniioombllem4  23074  uniioombllem5  23075  uniioombl  23077  volivth  23095  vitalilem3  23099  vitalilem4  23100  vitalilem5  23101  vitali  23102  mbfadd  23148  mbfsub  23149  i1fima2  23166  i1fd  23168  i1fadd  23182  itg1addlem2  23184  itg1addlem4  23186  itg1addlem5  23187  itg1climres  23201  mbfmul  23213  itg2splitlem  23235  itg2split  23236  limcresi  23369  limciun  23378  limcun  23379  dvreslem  23393  dvres2lem  23394  dvres  23395  dvres3a  23398  dvaddbr  23421  dvmulbr  23422  dvfsumle  23502  dvfsumabs  23504  ig1peu  23649  taylfvallem1  23829  tayl0  23834  pilem2  23924  pilem3  23925  rlimcnp2  24407  xrlimcnp  24409  ppisval  24544  ppifi  24546  ppiprm  24591  ppinprm  24592  chtprm  24593  chtnprm  24594  chtdif  24598  efchtdvds  24599  ppidif  24603  ppiltx  24617  prmorcht  24618  ppiub  24643  chtlepsi  24645  chtleppi  24649  pclogsum  24654  vmasum  24655  chpval2  24657  chpchtsum  24658  chpub  24659  2sqlem8  24865  chebbnd1lem1  24872  chtppilimlem1  24876  rplogsumlem2  24888  rpvmasum2  24915  dchrisum0re  24916  rplogsum  24930  dirith2  24931  axtgcgrrflx  25075  axtgcgrid  25076  axtgsegcon  25077  axtg5seg  25078  axtgbtwnid  25079  axtgpasch  25080  axtgcont1  25081  perpcom  25323  perpneq  25324  ragperp  25327  phnv  26856  minvecolem2  26918  minvecolem3  26919  minvecolem5  26924  minvecolem6  26925  minvecolem7  26926  hlimcaui  27280  chdmm1i  27523  chabs1  27562  chabs2  27563  ledii  27582  lejdii  27584  pjoml4i  27633  cmbr3i  27646  cmbr4i  27647  cmm1i  27652  osumcor2i  27690  3oalem4  27711  pjssmii  27727  pjocini  27744  pjini  27745  mayete3i  27774  riesz4  28110  riesz1  28111  cnlnadjeui  28123  cnlnadjeu  28124  cnlnssadj  28126  nmopadjlei  28134  pjin1i  28238  pjclem1  28241  stji1i  28288  stm1i  28289  dmdbr2  28349  ssmd1  28357  mdslj2i  28366  mdsl2bi  28369  mdslmd1lem1  28371  mdslmd2i  28376  atomli  28428  atcvat4i  28443  sumdmdlem2  28465  dmdbr5ati  28468  dmdbr6ati  28469  dmdbr7ati  28470  disjin  28584  disjxpin  28586  imadifxp  28599  off2  28626  ffsrn  28695  gsummptres  28918  xrge0tsmsd  28919  ordtrestNEW  29098  qqhnm  29165  qqhcn  29166  rrhre  29196  indf1ofs  29218  esumval  29238  esumel  29239  gsumesum  29251  esumlub  29252  esumcst  29255  esumfsup  29262  esumpcvgval  29270  esumcvg  29278  sigainb  29329  ldgenpisyslem1  29356  measinb2  29416  sibfinima  29531  sibfof  29532  eulerpartlemelr  29549  eulerpartlem1  29559  eulerpartgbij  29564  eulerpartlemgvv  29568  eulerpartlemgu  29569  eulerpartlemgs2  29572  sseqf  29584  ballotlemfelz  29682  ballotlemfp1  29683  bnj1292  29943  conpcon  30274  iccllyscon  30289  cvmsss2  30313  cvmcov2  30314  cvmopnlem  30317  cvmliftmolem2  30321  cvmliftlem15  30337  cvmlift2lem12  30353  mvrsfpw  30460  msrf  30496  elmsta  30502  mthmpps  30536  nepss  30657  dfon2lem4  30738  frrlem4  30830  nofulllem5  30908  txpss3v  30958  fixssdm  30986  fixssrn  30987  limitssson  30991  fneer  31321  neibastop1  31327  neibastop2lem  31328  filnetlem3  31348  ontopbas  31400  bj-restpw  32026  bj-ablssgrp  32115  taupilemrplb  32143  taupilem2  32145  taupi  32146  ptrest  32378  poimirlem29  32408  mblfinlem3  32418  mblfinlem4  32419  ismblfin  32420  mbfposadd  32427  sstotbnd2  32543  ssbnd  32557  heibor1lem  32578  heiborlem1  32580  heiborlem3  32582  heiborlem5  32584  heiborlem6  32585  heiborlem10  32589  heibor  32590  opidonOLD  32621  exidcl  32645  flddivrng  32768  lshpinN  33094  lcvexchlem5  33143  pmodlem2  33951  pmod1i  33952  pmodN  33954  osumcllem7N  34066  pexmidlem4N  34077  pl42lem3N  34085  djaclN  35243  dihoml4c  35483  dochdmj1  35497  djhcl  35507  dochexmidlem4  35570  mapd1o  35755  mapdin  35769  elrfi  36075  elrfirn  36076  elrfirn2  36077  ismrcd1  36079  istopclsd  36081  isnacs2  36087  mrefg3  36089  isnacs3  36091  diophrw  36140  diophin  36154  aomclem2  36443  islmodfg  36457  lsmfgcl  36462  lmhmfgima  36472  lmhmfgsplit  36474  lmhmlnmsplit  36475  pwfi2f1o  36484  hbt  36519  acsfn1p  36588  elinintrab  36702  trrelind  36776  rp-imass  36885  clsk3nimkb  37158  isotone2  37167  onfrALTlem2  37582  onfrALTlem2VD  37947  unirestss  38139  inmap  38196  fsumiunss  38443  islptre  38487  sumnnodd  38498  limclner  38519  cncfuni  38573  ismbl3  38680  ismbl4  38687  fouriersw  38925  qndenserrnbllem  38991  salincl  39020  salgencntex  39038  sge0less  39086  sge0resplit  39100  sge0split  39103  sge0iunmptlemre  39109  carageniuncllem1  39212  carageniuncllem2  39213  caragenel2d  39223  hspmbllem3  39319  hspmbl  39320  ovolval2lem  39334  sssmf  39426  smfaddlem1  39450  smflimlem2  39459  smflimlem3  39460  smflimlem4  39461  smfres  39476  smfmullem4  39480  rngcbas  41756  rngchomfval  41757  rngccofval  41761  dfrngc2  41763  rnghmsscmap2  41764  rnghmsscmap  41765  rngcsect  41771  funcrngcsetc  41789  ringcbas  41802  ringchomfval  41803  ringccofval  41807  dfringc2  41809  rhmsscmap2  41810  rhmsscmap  41811  rhmsscrnghm  41817  ringcsect  41822  funcringcsetc  41826  funcringcsetcALTV2lem9  41835  fldc  41874  fldhmsubc  41875  rngcrescrhm  41876  rhmsubclem1  41877  fldcALTV  41893  fldhmsubcALTV  41894  rngcrescrhmALTV  41895  rhmsubcALTVlem1  41896
  Copyright terms: Public domain W3C validator