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

Theorem inss1 4029
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 3998 . 2 (𝑥 ∈ (𝐴𝐵) → 𝑥𝐴)
21ssriv 3802 1 (𝐴𝐵) ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  cin 3768  wss 3769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393  df-in 3776  df-ss 3783
This theorem is referenced by:  inss2  4030  ssinss1  4038  unabs  4056  nssinpss  4058  dfin4  4069  inv1  4168  disjdif  4236  uniintsn  4706  wefrc  5305  relin1  5437  resss  5625  resmpt3  5655  cnvcnvss  5800  predss  5900  ordtri3or  5968  onfr  5976  ordelinel  6038  ordelinelOLD  6039  funin  6176  funimass2  6183  fnresin1  6216  fnres  6218  fresin  6288  fresaun  6290  fresaunres2  6291  nfvres  6444  ssimaex  6484  fneqeql2  6548  funiunfv  6730  isoini2  6813  ofrfval  7135  ofval  7136  ofrval  7137  off  7142  ofres  7143  ofco  7147  fparlem3  7513  fparlem4  7514  wfrlem4OLD  7654  smores  7685  smores2  7687  tfrlem5  7712  pmresg  8120  sbthlem7  8315  sbthcl  8321  infi  8423  imafi  8498  ixpfi2  8503  unifpw  8508  f1opwfi  8509  fival  8557  fi0  8565  dffi2  8568  elfiun  8575  dffi3  8576  marypha1lem  8578  ordtypelem3  8664  ordtypelem4  8665  ordtypelem6  8667  ordtypelem7  8668  ordtypelem8  8669  wdomima2g  8730  epfrs  8854  tskwe  9059  r0weon  9118  fodomfi2  9166  infpwfien  9168  ackbij1lem6  9332  ackbij1lem9  9335  ackbij1lem10  9336  ackbij1lem11  9337  ackbij1lem15  9341  ackbij1lem16  9342  fin23lem24  9429  fin23lem26  9432  fin23lem23  9433  fin23lem22  9434  fin23lem19  9443  isfin1-3  9493  ttukeylem6  9621  brdom3  9635  brdom5  9636  brdom4  9637  imadomg  9641  fpwwe2lem12  9748  canthp1lem2  9760  wunin  9820  tskin  9866  gruima  9909  ingru  9922  gruina  9925  grur1a  9926  nqerf  10037  nqerrel  10039  dedekindle  10486  hashun3  13391  hashin  13416  hashdif  13418  xptrrel  13944  rexanuz  14308  limsupgle  14431  rlimres  14512  lo1res  14513  lo1resb  14518  rlimresb  14519  o1resb  14520  lo1eq  14522  rlimeq  14523  o1of2  14566  o1rlimmul  14572  isercolllem2  14619  isercolllem3  14620  isercoll  14621  ackbijnn  14782  incexclem  14790  incexc  14791  bitsinvp1  15390  sadcaddlem  15398  sadadd2lem  15400  sadadd3  15402  sadaddlem  15407  sadasslem  15411  sadeq  15413  bitsres  15414  smuval2  15423  smupval  15429  smueqlem  15431  smumul  15434  ramub2  15935  ramub1lem2  15948  fvsetsid  16101  ressinbas  16147  ressress  16150  submre  16470  submrc  16493  isacs2  16518  isacs1i  16522  mreacs  16523  acsfn  16524  invss  16625  sscres  16687  coffth  16800  catcisolem  16960  catciso  16961  catcoppccl  16962  catcfuccl  16963  catcxpccl  17052  isdrs2  17144  isacs3lem  17371  isacs5lem  17374  acsfiindd  17382  psss  17419  tsrss  17428  tsrdir  17443  resscntz  17965  sylow2a  18235  lsmmod  18289  frgpnabllem2  18478  gsumzres  18511  gsumzaddlem  18522  dprddisj2  18640  ablfac1eu  18674  ablfac2  18690  isunit  18859  lspextmo  19263  2idlval  19442  aspsubrg  19540  psrbagsn  19703  mplind  19710  zringlpirlem2  20041  pjfval  20260  pjpm  20262  ofco2  20468  basdif0  20971  tgval2  20974  eltg3  20980  tgcl  20987  tgdom  20996  tgidm  20998  ppttop  21025  epttop  21027  ntropn  21067  ntrin  21079  mretopd  21110  mreclatdemoBAD  21114  neiptoptop  21149  restbas  21176  restfpw  21197  neitr  21198  restcls  21199  ordtrest  21220  subbascn  21272  cncls  21292  cnpresti  21306  cnprest  21307  fincmp  21410  cmpsublem  21416  cmpsub  21417  fiuncmp  21421  indisconn  21435  connsub  21438  cnconn  21439  iunconnlem  21444  clsconn  21447  conncompclo  21452  islly2  21501  cldllycmp  21512  kgentopon  21555  llycmpkgen2  21567  1stckgenlem  21570  ptbasfi  21598  txcls  21621  txcnp  21637  ptcnplem  21638  txcnmpt  21641  txcmplem2  21659  hausdiag  21662  txkgen  21669  xkopt  21672  xkococnlem  21676  txconn  21706  qtoptop2  21716  basqtop  21728  tgqtop  21729  kqnrmlem1  21760  kqnrmlem2  21761  nrmhmph  21811  fbssfi  21854  filin  21871  infil  21880  fbasrn  21901  fgtr  21907  ufprim  21926  flimrest  22000  hauspwpwf1  22004  txflf  22023  fclsrest  22041  alexsubALTlem3  22066  alexsubALTlem4  22067  ptcmplem5  22073  tsmsres  22160  tsmsxplem1  22169  ustund  22238  trust  22246  utoptop  22251  restutop  22254  cfiluweak  22312  xmetres  22382  metres  22383  blin2  22447  blbas  22448  blres  22449  setsmstopn  22496  met2ndci  22540  metrest  22542  ressxms  22543  tgioo  22812  xrsmopn  22828  zdis  22832  reconnlem1  22842  reconnlem2  22843  xrge0tsms  22850  cnheibor  22967  lebnum  22976  nmoleub2lem  23126  nmoleub2lem2  23128  nmhmcn  23132  tchcph  23248  cfilresi  23305  cfilres  23306  caussi  23307  causs  23308  relcmpcmet  23327  minveclem4a  23413  minveclem4  23415  ismbl2  23508  cmmbl  23515  nulmbl2  23517  unmbl  23518  shftmbl  23519  volinun  23527  voliunlem1  23531  voliunlem2  23532  ioombl1lem4  23542  ioombl1  23543  ioorcl  23558  uniioombllem2  23564  uniioombllem3  23566  uniioombllem4  23567  uniioombllem5  23568  uniioombl  23570  volivth  23588  vitalilem3  23591  vitalilem4  23592  vitalilem5  23593  vitali  23594  mbfadd  23642  mbfsub  23643  i1fima2  23660  i1fd  23662  i1fadd  23676  itg1addlem2  23678  itg1addlem4  23680  itg1addlem5  23681  itg1climres  23695  mbfmul  23707  itg2splitlem  23729  itg2split  23730  limcresi  23863  limciun  23872  limcun  23873  dvreslem  23887  dvres2lem  23888  dvres  23889  dvres3a  23892  dvaddbr  23915  dvmulbr  23916  dvfsumle  23998  dvfsumabs  24000  ig1peu  24145  taylfvallem1  24325  pilem2  24420  pilem3  24421  pilem3OLD  24422  rlimcnp2  24907  xrlimcnp  24909  ppisval  25044  ppifi  25046  ppiprm  25091  ppinprm  25092  chtprm  25093  chtnprm  25094  chtdif  25098  efchtdvds  25099  ppidif  25103  ppiltx  25117  prmorcht  25118  ppiub  25143  chtlepsi  25145  chtleppi  25149  pclogsum  25154  vmasum  25155  chpval2  25157  chpchtsum  25158  chpub  25159  2sqlem8  25365  chebbnd1lem1  25372  chtppilimlem1  25376  rplogsumlem2  25388  rpvmasum2  25415  dchrisum0re  25416  rplogsum  25430  dirith2  25431  axtgcgrrflx  25575  axtgcgrid  25576  axtgsegcon  25577  axtg5seg  25578  axtgbtwnid  25579  axtgpasch  25580  axtgcont1  25581  perpcom  25822  perpneq  25823  ragperp  25826  phnv  27997  minvecolem2  28059  minvecolem3  28060  minvecolem5  28065  minvecolem6  28066  minvecolem7  28067  hlimcaui  28421  chdmm1i  28664  chabs1  28703  chabs2  28704  ledii  28723  lejdii  28725  pjoml4i  28774  cmbr3i  28787  cmbr4i  28788  cmm1i  28793  osumcor2i  28831  3oalem4  28852  pjssmii  28868  pjocini  28885  pjini  28886  mayete3i  28915  riesz4  29251  riesz1  29252  cnlnadjeui  29264  cnlnadjeu  29265  cnlnssadj  29267  nmopadjlei  29275  pjin1i  29379  pjclem1  29382  stji1i  29429  stm1i  29430  dmdbr2  29490  ssmd1  29498  mdslj2i  29507  mdsl2bi  29510  mdslmd1lem1  29512  mdslmd2i  29517  atomli  29569  atcvat4i  29584  sumdmdlem2  29606  dmdbr5ati  29609  dmdbr6ati  29610  dmdbr7ati  29611  disjxpin  29726  imadifxp  29739  off2  29770  ffsrn  29831  gsummptres  30109  xrge0tsmsd  30110  ordtrestNEW  30292  qqhnm  30359  qqhcn  30360  rrhre  30390  indsumin  30409  indf1ofs  30413  esumval  30433  esumel  30434  gsumesum  30446  esumlub  30447  esumcst  30450  esumfsup  30457  esumpcvgval  30465  esumcvg  30473  sigainb  30524  ldgenpisyslem1  30551  measinb2  30611  sibfinima  30726  sibfof  30727  eulerpartlemelr  30744  eulerpartlem1  30754  eulerpartgbij  30759  eulerpartlemgu  30764  eulerpartlemgs2  30767  sseqf  30779  ballotlemfelz  30877  ballotlemfp1  30878  reprinrn  31021  reprinfz1  31025  hgt750lemd  31051  bnj1292  31209  connpconn  31540  iccllysconn  31555  cvmsss2  31579  cvmcov2  31580  cvmopnlem  31583  cvmliftmolem2  31587  cvmliftlem15  31603  cvmlift2lem12  31619  mvrsfpw  31726  msrf  31762  elmsta  31768  mthmpps  31802  nepss  31921  dfon2lem4  32011  frrlem4  32104  nosupbnd1lem1  32175  nosupbnd2  32183  txpss3v  32306  fixssdm  32334  fixssrn  32335  limitssson  32339  fneer  32669  neibastop1  32675  neibastop2lem  32676  filnetlem3  32696  ontopbas  32744  bj-disj2r  33323  bj-restpw  33356  bj-discrmoore  33377  bj-ablssgrp  33455  taupilemrplb  33483  taupilem2  33485  taupi  33486  ptrest  33721  poimirlem29  33751  mblfinlem3  33761  mblfinlem4  33762  ismblfin  33763  mbfposadd  33769  sstotbnd2  33884  ssbnd  33898  heibor1lem  33919  heiborlem1  33921  heiborlem3  33923  heiborlem5  33925  heiborlem6  33926  heiborlem10  33930  heibor  33931  opidonOLD  33962  exidcl  33986  flddivrng  34109  iss2  34425  xrnss3v  34447  lshpinN  34769  lcvexchlem5  34818  pmodlem2  35627  pmod1i  35628  pmodN  35630  osumcllem7N  35742  pexmidlem4N  35753  pl42lem3N  35761  djaclN  36917  dihoml4c  37157  dochdmj1  37171  djhcl  37181  dochexmidlem4  37244  mapd1o  37429  mapdin  37443  elrfi  37759  elrfirn  37760  elrfirn2  37761  ismrcd1  37763  istopclsd  37765  isnacs2  37771  mrefg3  37773  isnacs3  37775  diophrw  37824  diophin  37838  aomclem2  38126  islmodfg  38140  lsmfgcl  38145  lmhmfgima  38155  lmhmfgsplit  38157  lmhmlnmsplit  38158  pwfi2f1o  38167  hbt  38201  acsfn1p  38270  elinintrab  38383  trrelind  38457  rp-imass  38565  clsk3nimkb  38838  isotone2  38847  onfrALTlem2  39259  onfrALTlem2VD  39619  unirestss  39799  inmap  39888  fnfvimad  39943  fnfvima2  39961  fsumiunss  40287  islptre  40331  sumnnodd  40342  limclner  40363  liminfval4  40501  liminfval3  40502  cnrefiisplem  40535  cncfuni  40579  ismbl3  40682  ismbl4  40689  fouriersw  40927  qndenserrnbllem  40993  salincl  41022  salgencntex  41040  sge0less  41088  sge0resplit  41102  sge0split  41105  sge0iunmptlemre  41111  carageniuncllem1  41217  carageniuncllem2  41218  caragenel2d  41228  hspmbllem3  41324  hspmbl  41325  ovolval2lem  41339  sssmf  41429  smfaddlem1  41453  smflimlem2  41462  smflimlem3  41463  smflimlem4  41464  smfres  41479  smfmullem4  41483  smfsuplem1  41499  rngcbas  42533  rngchomfval  42534  rngccofval  42538  dfrngc2  42540  rnghmsscmap2  42541  rnghmsscmap  42542  rngcsect  42548  funcrngcsetc  42566  ringcbas  42579  ringchomfval  42580  ringccofval  42584  dfringc2  42586  rhmsscmap2  42587  rhmsscmap  42588  rhmsscrnghm  42594  ringcsect  42599  funcringcsetc  42603  funcringcsetcALTV2lem9  42612  fldc  42651  fldhmsubc  42652  rngcrescrhm  42653  rhmsubclem1  42654  fldcALTV  42669  fldhmsubcALTV  42670  rngcrescrhmALTV  42671  rhmsubcALTVlem1  42672  setrec2fun  43007  setrec2lem1  43008
  Copyright terms: Public domain W3C validator