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

Theorem inss1 3651
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 3616 . . 3  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
21simplbi 462 . 2  |-  ( x  e.  ( A  i^i  B )  ->  x  e.  A )
32ssriv 3435 1  |-  ( A  i^i  B )  C_  A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1886    i^i cin 3402    C_ wss 3403
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-v 3046  df-in 3410  df-ss 3417
This theorem is referenced by:  inss2  3652  ssinss1  3659  unabs  3672  nssinpss  3674  dfin4  3682  inv1  3760  disjdif  3838  uniintsn  4271  wefrc  4827  relin1  4950  resss  5127  resmpt3  5154  cnvcnvss  5289  predss  5386  ordtri3or  5454  onfr  5461  ordelinel  5520  funin  5648  funimass2  5655  fnresin1  5688  fnres  5690  fresin  5750  fresaun  5752  fresaunres2  5753  nfvres  5893  ssimaex  5928  fneqeql2  5989  funiunfv  6151  isoini2  6228  ofrfval  6536  ofval  6537  ofrval  6538  off  6543  ofres  6544  ofco  6548  fparlem3  6895  fparlem4  6896  wfrlem4  7036  smores  7068  smores2  7070  tfrlem5  7095  pmresg  7496  sbthlem7  7685  sbthcl  7691  infi  7792  imafi  7864  ixpfi2  7869  unifpw  7874  f1opwfi  7875  fival  7923  fi0  7931  dffi2  7934  elfiun  7941  dffi3  7942  marypha1lem  7944  ordtypelem3  8032  ordtypelem4  8033  ordtypelem6  8035  ordtypelem7  8036  ordtypelem8  8037  wdomima2g  8098  epfrs  8212  tskwe  8381  r0weon  8440  fodomfi2  8488  infpwfien  8490  ackbij1lem6  8652  ackbij1lem9  8655  ackbij1lem10  8656  ackbij1lem11  8657  ackbij1lem15  8661  ackbij1lem16  8662  fin23lem24  8749  fin23lem26  8752  fin23lem23  8753  fin23lem22  8754  fin23lem19  8763  isfin1-3  8813  ttukeylem6  8941  brdom3  8953  brdom5  8954  brdom4  8955  imadomg  8959  fpwwe2lem12  9063  canthp1lem2  9075  wunin  9135  tskin  9181  gruima  9224  ingru  9237  gruina  9240  grur1a  9241  nqerf  9352  nqerrel  9354  dedekindle  9795  hashun3  12560  hashin  12584  hashdif  12586  xptrrel  13037  rexanuz  13401  limsupgle  13528  rlimres  13615  lo1res  13616  lo1resb  13621  rlimresb  13622  o1resb  13623  lo1eq  13625  rlimeq  13626  o1of2  13669  o1rlimmul  13675  isercolllem2  13722  isercolllem3  13723  isercoll  13724  ackbijnn  13879  incexclem  13887  incexc  13888  bitsinvp1  14416  sadcaddlem  14424  sadadd2lem  14426  sadadd3  14428  sadaddlem  14433  sadasslem  14437  sadeq  14439  bitsres  14440  smuval2  14449  smupval  14455  smueqlem  14457  smumul  14460  prmreclem2  14854  ramub2  14964  ramub1lem2  14978  fvsetsid  15141  ressinbas  15178  ressress  15180  submre  15504  submrc  15527  isacs2  15552  isacs1i  15556  mreacs  15557  acsfn  15558  invss  15659  sscres  15721  coffth  15834  catcisolem  15994  catciso  15995  catcoppccl  15996  catcfuccl  15997  catcxpccl  16085  isdrs2  16177  isacs3lem  16405  isacs5lem  16408  acsfiindd  16416  psss  16453  psssdm2  16454  tsrss  16462  tsrdir  16477  resscntz  16978  sylow2a  17264  lsmmod  17318  frgpnabllem2  17503  gsumzres  17536  gsumzaddlem  17547  dprddisj2  17665  ablfac1eu  17699  ablfac2  17715  isunit  17878  lspextmo  18272  2idlval  18450  aspsubrg  18548  psrbagsn  18711  mplind  18718  zringlpirlem2OLD  19047  zringlpirlem2  19049  pjfval  19262  pjpm  19264  ofco2  19469  basdif0  19961  tgval2  19964  eltg3  19970  unitgOLD  19976  tgcl  19978  tgdom  19987  tgidm  19989  ppttop  20015  epttop  20017  ntropn  20057  ntrin  20069  mretopd  20101  mreclatdemoBAD  20105  neiptoptop  20140  restbas  20167  restfpw  20188  neitr  20189  restcls  20190  ordtrest  20211  subbascn  20263  cncls  20283  cnpresti  20297  cnprest  20298  fincmp  20401  cmpsublem  20407  cmpsub  20408  fiuncmp  20412  indiscon  20426  connsub  20429  cnconn  20430  iunconlem  20435  clscon  20438  concompclo  20443  islly2  20492  cldllycmp  20503  kgentopon  20546  llycmpkgen2  20558  1stckgenlem  20561  ptbasfi  20589  txcls  20612  txcnp  20628  ptcnplem  20629  txcnmpt  20632  txcmplem2  20650  hausdiag  20653  txkgen  20660  xkopt  20663  xkococnlem  20667  txcon  20697  qtoptop2  20707  basqtop  20719  tgqtop  20720  kqnrmlem1  20751  kqnrmlem2  20752  nrmhmph  20802  fbssfi  20845  filin  20862  infil  20871  fbasrn  20892  fgtr  20898  ufprim  20917  flimrest  20991  hauspwpwf1  20995  txflf  21014  fclsrest  21032  alexsubALTlem3  21057  alexsubALTlem4  21058  ptcmplem5  21064  tsmsres  21151  tsmsxplem1  21160  ustund  21229  trust  21237  utoptop  21242  restutop  21245  cfiluweak  21303  xmetres  21372  metres  21373  blin2  21437  blbas  21438  blres  21439  setsmstopn  21486  met2ndci  21530  metrest  21532  ressxms  21533  tgioo  21807  xrsmopn  21823  zdis  21827  reconnlem1  21837  reconnlem2  21838  xrge0tsms  21845  cnheibor  21976  lebnum  21988  nmoleub2lem  22121  nmoleub2lem3  22122  nmoleub2lem2  22123  nmoleub3  22126  nmhmcn  22127  tchcph  22204  cfilresi  22258  cfilres  22259  caussi  22260  causs  22261  relcmpcmet  22279  minveclem4a  22365  minveclem4  22367  minveclem4aOLD  22377  minveclem4OLD  22379  ismbl2  22474  cmmbl  22481  nulmbl2  22483  unmbl  22484  shftmbl  22485  volinun  22492  voliunlem1  22496  voliunlem2  22497  ioombl1lem4  22507  ioombl1  22508  ioorcl  22522  ioorclOLD  22527  uniioombllem2  22533  uniioombllem2OLD  22534  uniioombllem3  22536  uniioombllem4  22537  uniioombllem5  22538  uniioombl  22540  volivth  22558  vitalilem3  22561  vitalilem4  22562  vitalilem5  22563  vitali  22564  mbfadd  22610  mbfsub  22611  i1fima2  22630  i1fd  22632  i1fadd  22646  itg1addlem2  22648  itg1addlem4  22650  itg1addlem5  22651  itg1climres  22665  mbfmul  22677  itg2splitlem  22699  itg2split  22700  limcresi  22833  limciun  22842  limcun  22843  dvreslem  22857  dvres2lem  22858  dvres  22859  dvres3a  22862  dvaddbr  22885  dvmulbr  22886  dvfsumle  22966  dvfsumabs  22968  ig1peu  23115  ig1peuOLD  23116  taylfvallem1  23305  tayl0  23310  pilem2  23400  pilem2OLD  23401  pilem3  23402  pilem3OLD  23403  rlimcnp2  23885  xrlimcnp  23887  ppisval  24023  ppifi  24025  ppiprm  24071  ppinprm  24072  chtprm  24073  chtnprm  24074  chtdif  24078  efchtdvds  24079  ppidif  24083  ppiltx  24097  prmorcht  24098  ppiub  24125  chtlepsi  24127  chtleppi  24131  pclogsum  24136  vmasum  24137  chpval2  24139  chpchtsum  24140  chpub  24141  2sqlem8  24293  chebbnd1lem1  24300  chtppilimlem1  24304  rplogsumlem2  24316  rpvmasum2  24343  dchrisum0re  24344  rplogsum  24358  dirith2  24359  axtgcgrrflx  24503  axtgcgrid  24504  axtgsegcon  24505  axtg5seg  24506  axtgbtwnid  24507  axtgpasch  24508  axtgcont1  24509  perpcom  24751  perpneq  24752  ragperp  24755  opidonOLD  26043  flddivrng  26136  phnv  26448  minvecolem2  26510  minvecolem3  26511  minvecolem5  26516  minvecolem6  26517  minvecolem7  26518  minvecolem2OLD  26520  minvecolem3OLD  26521  minvecolem5OLD  26526  minvecolem6OLD  26527  minvecolem7OLD  26528  hlimcaui  26882  chdmm1i  27123  chabs1  27162  chabs2  27163  ledii  27182  lejdii  27184  pjoml4i  27233  cmbr3i  27246  cmbr4i  27247  cmm1i  27252  osumcor2i  27290  3oalem4  27311  pjssmii  27327  pjocini  27344  pjini  27345  mayete3i  27374  riesz4  27710  riesz1  27711  cnlnadjeui  27723  cnlnadjeu  27724  cnlnssadj  27726  nmopadjlei  27734  pjin1i  27838  pjclem1  27841  stji1i  27888  stm1i  27889  dmdbr2  27949  ssmd1  27957  mdslj2i  27966  mdsl2bi  27969  mdslmd1lem1  27971  mdslmd2i  27976  atomli  28028  atcvat4i  28043  sumdmdlem2  28065  dmdbr5ati  28068  dmdbr6ati  28069  dmdbr7ati  28070  disjin  28189  disjxpin  28191  imadifxp  28205  off2  28235  ffsrn  28307  gsummptres  28540  xrge0tsmsd  28541  ordtrestNEW  28720  qqhnm  28787  qqhcn  28788  rrhre  28818  indf1ofs  28840  esumval  28860  esumel  28861  gsumesum  28873  esumlub  28874  esumcst  28877  esumfsup  28884  esumpcvgval  28892  esumcvg  28900  sigainb  28951  ldgenpisyslem1  28978  measinb2  29038  sibfinima  29165  sibfof  29166  eulerpartlemelr  29183  eulerpartlem1  29193  eulerpartgbij  29198  eulerpartlemgvv  29202  eulerpartlemgu  29203  eulerpartlemgs2  29206  sseqf  29218  ballotlemfelz  29316  ballotlemfp1  29317  bnj1292  29620  conpcon  29951  iccllyscon  29966  cvmsss2  29990  cvmcov2  29991  cvmopnlem  29994  cvmliftmolem2  29998  cvmliftlem15  30014  cvmlift2lem12  30030  mvrsfpw  30137  msrf  30173  elmsta  30179  mthmpps  30213  nepss  30343  dfon2lem4  30425  frrlem4  30510  nofulllem5  30588  txpss3v  30638  fixssdm  30666  fixssrn  30667  limitssson  30671  fneer  31002  neibastop1  31008  neibastop2lem  31009  filnetlem3  31029  ontopbas  31081  bj-ablssgrp  31686  taupilemrplb  31714  taupilem2  31716  taupi  31717  ptrest  31932  poimirlem29  31962  mblfinlem3  31972  mblfinlem4  31973  ismblfin  31974  mbfposadd  31981  sstotbnd2  32099  ssbnd  32113  heibor1lem  32134  heiborlem1  32136  heiborlem3  32138  heiborlem5  32140  heiborlem6  32141  heiborlem10  32145  heibor  32146  exidcl  32167  lshpinN  32549  lcvexchlem5  32598  pmodlem2  33406  pmod1i  33407  pmodN  33409  osumcllem7N  33521  pexmidlem4N  33532  pl42lem3N  33540  djaclN  34698  dihoml4c  34938  dochdmj1  34952  djhcl  34962  dochexmidlem4  35025  mapd1o  35210  mapdin  35224  elrfi  35530  elrfirn  35531  elrfirn2  35532  ismrcd1  35534  istopclsd  35536  isnacs2  35542  mrefg3  35544  isnacs3  35546  diophrw  35595  diophin  35609  aomclem2  35907  islmodfg  35921  lsmfgcl  35926  lmhmfgima  35936  lmhmfgsplit  35938  lmhmlnmsplit  35939  pwfi2f1o  35948  hbt  35983  acsfn1p  36059  elinintrab  36177  trrelind  36251  rp-imass  36360  onfrALTlem2  36906  onfrALTlem2VD  37280  fsumiunss  37648  islptre  37693  sumnnodd  37704  limclner  37726  cncfuni  37758  fouriersw  38089  qndenserrnbllem  38157  salincl  38178  salgencntex  38196  sge0less  38228  sge0resplit  38242  sge0split  38245  sge0iunmptlemre  38251  carageniuncllem1  38336  carageniuncllem2  38337  caragenel2d  38347  hspmbllem3  38444  hspmbl  38445  rngcbas  39954  rngchomfval  39955  rngccofval  39959  dfrngc2  39961  rnghmsscmap2  39962  rnghmsscmap  39963  rngcsect  39969  funcrngcsetc  39987  ringcbas  40000  ringchomfval  40001  ringccofval  40005  dfringc2  40007  rhmsscmap2  40008  rhmsscmap  40009  rhmsscrnghm  40015  ringcsect  40020  funcringcsetc  40024  funcringcsetcALTV2lem9  40033  fldc  40072  fldhmsubc  40073  rngcrescrhm  40074  rhmsubclem1  40075  fldcALTV  40091  fldhmsubcALTV  40092  rngcrescrhmALTV  40093  rhmsubcALTVlem1  40094
  Copyright terms: Public domain W3C validator