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

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

Proof of Theorem inss1
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 elin 3646 . . 3  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
21simplbi 461 . 2  |-  ( x  e.  ( A  i^i  B )  ->  x  e.  A )
32ssriv 3465 1  |-  ( A  i^i  B )  C_  A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1867    i^i cin 3432    C_ wss 3433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-v 3080  df-in 3440  df-ss 3447
This theorem is referenced by:  inss2  3680  ssinss1  3687  unabs  3700  nssinpss  3702  dfin4  3710  inv1  3786  disjdif  3864  uniintsn  4287  wefrc  4840  relin1  4963  resss  5140  resmpt3  5167  cnvcnvss  5302  predss  5398  ordtri3or  5466  onfr  5473  ordelinel  5532  funin  5660  funimass2  5667  fnresin1  5700  fnres  5702  fresin  5761  fresaun  5763  fresaunres2  5764  nfvres  5903  ssimaex  5938  fneqeql2  5998  funiunfv  6160  isoini2  6237  ofrfval  6545  ofval  6546  ofrval  6547  off  6552  ofres  6553  ofco  6557  fparlem3  6901  fparlem4  6902  wfrlem4  7039  smores  7071  smores2  7073  tfrlem5  7098  pmresg  7499  sbthlem7  7686  sbthcl  7692  infi  7793  imafi  7865  ixpfi2  7870  unifpw  7875  f1opwfi  7876  fival  7924  fi0  7932  dffi2  7935  elfiun  7942  dffi3  7943  marypha1lem  7945  ordtypelem3  8033  ordtypelem4  8034  ordtypelem6  8036  ordtypelem7  8037  ordtypelem8  8038  wdomima2g  8099  epfrs  8212  tskwe  8381  r0weon  8440  fodomfi2  8487  infpwfien  8489  ackbij1lem6  8651  ackbij1lem9  8654  ackbij1lem10  8655  ackbij1lem11  8656  ackbij1lem15  8660  ackbij1lem16  8661  fin23lem24  8748  fin23lem26  8751  fin23lem23  8752  fin23lem22  8753  fin23lem19  8762  isfin1-3  8812  ttukeylem6  8940  brdom3  8952  brdom5  8953  brdom4  8954  imadomg  8958  fpwwe2lem12  9062  canthp1lem2  9074  wunin  9134  tskin  9180  gruima  9223  ingru  9236  gruina  9239  grur1a  9240  nqerf  9351  nqerrel  9353  dedekindle  9794  hashun3  12556  hashdif  12581  xptrrel  13023  rexanuz  13387  limsupgle  13513  rlimres  13600  lo1res  13601  lo1resb  13606  rlimresb  13607  o1resb  13608  lo1eq  13610  rlimeq  13611  o1of2  13654  o1rlimmul  13660  isercolllem2  13707  isercolllem3  13708  isercoll  13709  ackbijnn  13864  incexclem  13872  incexc  13873  bitsinvp1  14401  sadcaddlem  14409  sadadd2lem  14411  sadadd3  14413  sadaddlem  14418  sadasslem  14422  sadeq  14424  bitsres  14425  smuval2  14434  smupval  14440  smueqlem  14442  smumul  14445  prmreclem2  14839  ramub2  14949  ramub1lem2  14963  fvsetsid  15126  ressinbas  15163  ressress  15165  submre  15489  submrc  15512  isacs2  15537  isacs1i  15541  mreacs  15542  acsfn  15543  invss  15644  sscres  15706  coffth  15819  catcisolem  15979  catciso  15980  catcoppccl  15981  catcfuccl  15982  catcxpccl  16070  isdrs2  16162  isacs3lem  16390  isacs5lem  16393  acsfiindd  16401  psss  16438  psssdm2  16439  tsrss  16447  tsrdir  16462  resscntz  16963  sylow2a  17249  lsmmod  17303  frgpnabllem2  17488  gsumzres  17521  gsumzaddlem  17532  dprddisj2  17650  ablfac1eu  17684  ablfac2  17700  isunit  17863  lspextmo  18257  2idlval  18435  aspsubrg  18533  psrbagsn  18696  mplind  18703  zringlpirlem2OLD  19031  zringlpirlem2  19033  pjfval  19246  pjpm  19248  ofco2  19453  basdif0  19945  tgval2  19948  eltg3  19954  unitgOLD  19960  tgcl  19962  tgdom  19971  tgidm  19973  ppttop  19999  epttop  20001  ntropn  20041  ntrin  20053  mretopd  20085  mreclatdemoBAD  20089  neiptoptop  20124  restbas  20151  restfpw  20172  neitr  20173  restcls  20174  ordtrest  20195  subbascn  20247  cncls  20267  cnpresti  20281  cnprest  20282  fincmp  20385  cmpsublem  20391  cmpsub  20392  fiuncmp  20396  indiscon  20410  connsub  20413  cnconn  20414  iunconlem  20419  clscon  20422  concompclo  20427  islly2  20476  cldllycmp  20487  kgentopon  20530  llycmpkgen2  20542  1stckgenlem  20545  ptbasfi  20573  txcls  20596  txcnp  20612  ptcnplem  20613  txcnmpt  20616  txcmplem2  20634  hausdiag  20637  txkgen  20644  xkopt  20647  xkococnlem  20651  txcon  20681  qtoptop2  20691  basqtop  20703  tgqtop  20704  kqnrmlem1  20735  kqnrmlem2  20736  nrmhmph  20786  fbssfi  20829  filin  20846  infil  20855  fbasrn  20876  fgtr  20882  ufprim  20901  flimrest  20975  hauspwpwf1  20979  txflf  20998  fclsrest  21016  alexsubALTlem3  21041  alexsubALTlem4  21042  ptcmplem5  21048  tsmsres  21135  tsmsxplem1  21144  ustund  21213  trust  21221  utoptop  21226  restutop  21229  cfiluweak  21287  xmetres  21356  metres  21357  blin2  21421  blbas  21422  blres  21423  setsmstopn  21470  met2ndci  21514  metrest  21516  ressxms  21517  tgioo  21791  xrsmopn  21807  zdis  21811  reconnlem1  21821  reconnlem2  21822  xrge0tsms  21829  cnheibor  21960  lebnum  21972  nmoleub2lem  22105  nmoleub2lem3  22106  nmoleub2lem2  22107  nmoleub3  22110  nmhmcn  22111  tchcph  22188  cfilresi  22242  cfilres  22243  caussi  22244  causs  22245  relcmpcmet  22263  minveclem4a  22349  minveclem4  22351  minveclem4aOLD  22361  minveclem4OLD  22363  ismbl2  22458  cmmbl  22465  nulmbl2  22467  unmbl  22468  shftmbl  22469  volinun  22476  voliunlem1  22480  voliunlem2  22481  ioombl1lem4  22491  ioombl1  22492  ioorcl  22506  ioorclOLD  22511  uniioombllem2  22517  uniioombllem2OLD  22518  uniioombllem3  22520  uniioombllem4  22521  uniioombllem5  22522  uniioombl  22524  volivth  22542  vitalilem3  22545  vitalilem4  22546  vitalilem5  22547  vitali  22548  mbfadd  22594  mbfsub  22595  i1fima2  22614  i1fd  22616  i1fadd  22630  itg1addlem2  22632  itg1addlem4  22634  itg1addlem5  22635  itg1climres  22649  mbfmul  22661  itg2splitlem  22683  itg2split  22684  limcresi  22817  limciun  22826  limcun  22827  dvreslem  22841  dvres2lem  22842  dvres  22843  dvres3a  22846  dvaddbr  22869  dvmulbr  22870  dvfsumle  22950  dvfsumabs  22952  ig1peu  23099  ig1peuOLD  23100  taylfvallem1  23289  tayl0  23294  pilem2  23384  pilem2OLD  23385  pilem3  23386  pilem3OLD  23387  rlimcnp2  23869  xrlimcnp  23871  ppisval  24007  ppifi  24009  ppiprm  24055  ppinprm  24056  chtprm  24057  chtnprm  24058  chtdif  24062  efchtdvds  24063  ppidif  24067  ppiltx  24081  prmorcht  24082  ppiub  24109  chtlepsi  24111  chtleppi  24115  pclogsum  24120  vmasum  24121  chpval2  24123  chpchtsum  24124  chpub  24125  2sqlem8  24277  chebbnd1lem1  24284  chtppilimlem1  24288  rplogsumlem2  24300  rpvmasum2  24327  dchrisum0re  24328  rplogsum  24342  dirith2  24343  axtgcgrrflx  24487  axtgcgrid  24488  axtgsegcon  24489  axtg5seg  24490  axtgbtwnid  24491  axtgpasch  24492  axtgcont1  24493  perpcom  24735  perpneq  24736  ragperp  24739  opidonOLD  26026  flddivrng  26119  phnv  26431  minvecolem2  26493  minvecolem3  26494  minvecolem5  26499  minvecolem6  26500  minvecolem7  26501  minvecolem2OLD  26503  minvecolem3OLD  26504  minvecolem5OLD  26509  minvecolem6OLD  26510  minvecolem7OLD  26511  hlimcaui  26865  chdmm1i  27106  chabs1  27145  chabs2  27146  ledii  27165  lejdii  27167  pjoml4i  27216  cmbr3i  27229  cmbr4i  27230  cmm1i  27235  osumcor2i  27273  3oalem4  27294  pjssmii  27310  pjocini  27327  pjini  27328  mayete3i  27357  riesz4  27693  riesz1  27694  cnlnadjeui  27706  cnlnadjeu  27707  cnlnssadj  27709  nmopadjlei  27717  pjin1i  27821  pjclem1  27824  stji1i  27871  stm1i  27872  dmdbr2  27932  ssmd1  27940  mdslj2i  27949  mdsl2bi  27952  mdslmd1lem1  27954  mdslmd2i  27959  atomli  28011  atcvat4i  28026  sumdmdlem2  28048  dmdbr5ati  28051  dmdbr6ati  28052  dmdbr7ati  28053  disjin  28176  disjxpin  28178  imadifxp  28192  off2  28223  ffsrn  28299  gsummptres  28536  xrge0tsmsd  28537  ordtrestNEW  28716  qqhnm  28783  qqhcn  28784  rrhre  28814  indf1ofs  28836  esumval  28856  esumel  28857  gsumesum  28869  esumlub  28870  esumcst  28873  esumfsup  28880  esumpcvgval  28888  esumcvg  28896  sigainb  28947  ldgenpisyslem1  28974  measinb2  29034  sibfinima  29161  sibfof  29162  eulerpartlemelr  29179  eulerpartlem1  29189  eulerpartgbij  29194  eulerpartlemgvv  29198  eulerpartlemgu  29199  eulerpartlemgs2  29202  sseqf  29214  ballotlemfelz  29312  ballotlemfp1  29313  bnj1292  29616  conpcon  29947  iccllyscon  29962  cvmsss2  29986  cvmcov2  29987  cvmopnlem  29990  cvmliftmolem2  29994  cvmliftlem15  30010  cvmlift2lem12  30026  mvrsfpw  30133  msrf  30169  elmsta  30175  mthmpps  30209  nepss  30339  dfon2lem4  30420  frrlem4  30505  nofulllem5  30581  txpss3v  30631  fixssdm  30659  fixssrn  30660  limitssson  30664  fneer  30995  neibastop1  31001  neibastop2lem  31002  filnetlem3  31022  ontopbas  31074  bj-ablssgrp  31639  taupilemrplb  31667  taupilem2  31669  taupi  31670  ptrest  31847  poimirlem29  31877  mblfinlem3  31887  mblfinlem4  31888  ismblfin  31889  mbfposadd  31896  sstotbnd2  32014  ssbnd  32028  heibor1lem  32049  heiborlem1  32051  heiborlem3  32053  heiborlem5  32055  heiborlem6  32056  heiborlem10  32060  heibor  32061  exidcl  32082  lshpinN  32468  lcvexchlem5  32517  pmodlem2  33325  pmod1i  33326  pmodN  33328  osumcllem7N  33440  pexmidlem4N  33451  pl42lem3N  33459  djaclN  34617  dihoml4c  34857  dochdmj1  34871  djhcl  34881  dochexmidlem4  34944  mapd1o  35129  mapdin  35143  elrfi  35449  elrfirn  35450  elrfirn2  35451  ismrcd1  35453  istopclsd  35455  isnacs2  35461  mrefg3  35463  isnacs3  35465  diophrw  35514  diophin  35528  aomclem2  35827  islmodfg  35841  lsmfgcl  35846  lmhmfgima  35856  lmhmfgsplit  35858  lmhmlnmsplit  35859  pwfi2f1o  35868  hbt  35903  acsfn1p  35979  fiinfi  36091  trrelind  36111  rp-imass  36218  onfrALTlem2  36764  onfrALTlem2VD  37141  fsumiunss  37444  islptre  37486  sumnnodd  37497  limclner  37519  cncfuni  37551  fouriersw  37882  salincl  37952  sge0less  37989  sge0resplit  38003  sge0split  38006  sge0iunmptlemre  38012  carageniuncllem1  38072  carageniuncllem2  38073  rngcbas  39029  rngchomfval  39030  rngccofval  39034  dfrngc2  39036  rnghmsscmap2  39037  rnghmsscmap  39038  rngcsect  39044  funcrngcsetc  39062  ringcbas  39075  ringchomfval  39076  ringccofval  39080  dfringc2  39082  rhmsscmap2  39083  rhmsscmap  39084  rhmsscrnghm  39090  ringcsect  39095  funcringcsetc  39099  funcringcsetcALTV2lem9  39108  fldc  39147  fldhmsubc  39148  rngcrescrhm  39149  rhmsubclem1  39150  fldcALTV  39166  fldhmsubcALTV  39167  rngcrescrhmALTV  39168  rhmsubcALTVlem1  39169
  Copyright terms: Public domain W3C validator