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

Theorem inss1 3558
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 3527 . . 3  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
21simplbi 457 . 2  |-  ( x  e.  ( A  i^i  B )  ->  x  e.  A )
32ssriv 3348 1  |-  ( A  i^i  B )  C_  A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1755    i^i cin 3315    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-in 3323  df-ss 3330
This theorem is referenced by:  inss2  3559  ssinss1  3566  unabs  3568  nssinpss  3570  dfin4  3578  inv1  3652  disjdif  3739  uniintsn  4153  wefrc  4701  ordtri3or  4738  onfr  4745  ordelinel  4804  relin1  4944  resss  5122  resmpt3  5145  cnvcnvss  5280  funin  5473  funimass2  5480  fnresin1  5513  fnres  5515  fresin  5568  fresaun  5570  fresaunres2  5571  nfvres  5708  ssimaex  5744  fneqeql2  5800  funiunfv  5952  isoini2  6017  ofrfval  6317  ofval  6318  ofrval  6319  off  6323  ofres  6324  ofco  6329  fparlem3  6663  fparlem4  6664  smores  6799  smores2  6801  tfrlem5  6825  pmresg  7228  sbthlem7  7415  sbthcl  7421  infi  7524  imafi  7592  ixpfi2  7597  unifpw  7602  f1opwfi  7603  fival  7650  fi0  7658  dffi2  7661  elfiun  7668  dffi3  7669  marypha1lem  7671  ordtypelem3  7722  ordtypelem4  7723  ordtypelem6  7725  ordtypelem7  7726  ordtypelem8  7727  wdomima2g  7789  epfrs  7939  tskwe  8108  r0weon  8167  fodomfi2  8218  infpwfien  8220  ackbij1lem6  8382  ackbij1lem9  8385  ackbij1lem10  8386  ackbij1lem11  8387  ackbij1lem15  8391  ackbij1lem16  8392  fin23lem24  8479  fin23lem26  8482  fin23lem23  8483  fin23lem22  8484  fin23lem19  8493  isfin1-3  8543  ttukeylem6  8671  brdom3  8683  brdom5  8684  brdom4  8685  imadomg  8689  fpwwe2lem12  8796  canthp1lem2  8808  wunin  8868  tskin  8914  gruima  8957  ingru  8970  gruina  8973  grur1a  8974  nqerf  9087  nqerrel  9089  dedekindle  9522  hashun3  12131  hashdif  12152  rexanuz  12817  limsupgle  12939  rlimres  13020  lo1res  13021  lo1resb  13026  rlimresb  13027  o1resb  13028  lo1eq  13030  rlimeq  13031  o1of2  13074  o1rlimmul  13080  isercolllem2  13127  isercolllem3  13128  isercoll  13129  ackbijnn  13274  incexclem  13282  incexc  13283  bitsinvp1  13628  sadcaddlem  13636  sadadd2lem  13638  sadadd3  13640  sadaddlem  13645  sadasslem  13649  sadeq  13651  bitsres  13652  smuval2  13661  smupval  13667  smueqlem  13669  smumul  13672  prmreclem2  13961  ramub2  14058  ramub1lem2  14071  fvsetsid  14182  ressinbas  14217  ressress  14218  submre  14526  submrc  14549  isacs2  14574  isacs1i  14578  mreacs  14579  acsfn  14580  invss  14682  sscres  14719  coffth  14829  catcisolem  14957  catciso  14958  catcoppccl  14959  catcfuccl  14960  catcxpccl  15000  isdrs2  15092  isacs3lem  15319  isacs5lem  15322  acsfiindd  15330  psss  15367  psssdm2  15368  tsrss  15376  tsrdir  15391  resscntz  15829  sylow2a  16098  lsmmod  16152  frgpnabllem2  16332  gsumzres  16368  gsumzresOLD  16372  gsumzaddlem  16388  gsumzaddlemOLD  16390  dprddisj2  16511  dprddisj2OLD  16512  ablfac1eu  16548  ablfac2  16564  isunit  16683  lspextmo  17059  2idlval  17237  aspsubrg  17324  psrbagsn  17509  mplind  17516  zringlpirlem2  17746  zlpirlem2  17751  pjfval  17973  pjpm  17975  ofco2  18174  basdif0  18400  tgval2  18403  eltg3  18409  unitg  18414  tgcl  18416  tgdom  18425  tgidm  18427  ppttop  18453  epttop  18455  ntropn  18495  ntrin  18507  mretopd  18538  mreclatdemoBAD  18542  neiptoptop  18577  restbas  18604  restfpw  18625  neitr  18626  restcls  18627  ordtrest  18648  subbascn  18700  cncls  18720  cnpresti  18734  cnprest  18735  fincmp  18838  cmpsublem  18844  cmpsub  18845  fiuncmp  18849  indiscon  18864  connsub  18867  cnconn  18868  iunconlem  18873  clscon  18876  concompclo  18881  islly2  18930  cldllycmp  18941  kgentopon  18953  llycmpkgen2  18965  1stckgenlem  18968  ptbasfi  18996  txcls  19019  txcnp  19035  ptcnplem  19036  txcnmpt  19039  txcmplem2  19057  hausdiag  19060  txkgen  19067  xkopt  19070  xkococnlem  19074  txcon  19104  qtoptop2  19114  basqtop  19126  tgqtop  19127  kqnrmlem1  19158  kqnrmlem2  19159  nrmhmph  19209  fbssfi  19252  filin  19269  infil  19278  fbasrn  19299  fgtr  19305  ufprim  19324  flimrest  19398  hauspwpwf1  19402  txflf  19421  fclsrest  19439  alexsubALTlem3  19463  alexsubALTlem4  19464  ptcmplem5  19470  tsmsresOLD  19559  tsmsres  19560  tsmsxplem1  19569  ustund  19638  trust  19646  utoptop  19651  restutop  19654  cfiluweak  19712  xmetres  19781  metres  19782  blin2  19846  blbas  19847  blres  19848  setsmstopn  19895  met2ndci  19939  metrest  19941  ressxms  19942  tgioo  20215  xrsmopn  20231  zdis  20235  reconnlem1  20245  reconnlem2  20246  xrge0tsms  20253  cnheibor  20369  lebnum  20378  nmoleub2lem  20511  nmoleub2lem3  20512  nmoleub2lem2  20513  nmoleub3  20516  nmhmcn  20517  tchcph  20594  cfilresi  20648  cfilres  20649  caussi  20650  causs  20651  relcmpcmet  20669  minveclem4a  20759  minveclem4  20761  ismbl2  20852  cmmbl  20858  nulmbl2  20860  unmbl  20861  shftmbl  20862  volinun  20869  voliunlem1  20873  voliunlem2  20874  ioombl1lem4  20884  ioombl1  20885  ioorcl  20899  uniioombllem2  20905  uniioombllem3  20907  uniioombllem4  20908  uniioombllem5  20909  uniioombl  20911  volivth  20929  vitalilem3  20932  vitalilem4  20933  vitalilem5  20934  vitali  20935  mbfadd  20981  mbfsub  20982  i1fima2  20999  i1fd  21001  i1fadd  21015  itg1addlem2  21017  itg1addlem4  21019  itg1addlem5  21020  itg1climres  21034  mbfmul  21046  itg2splitlem  21068  itg2split  21069  limcresi  21202  limciun  21211  limcun  21212  dvreslem  21226  dvres2lem  21227  dvres  21228  dvres3a  21231  dvaddbr  21254  dvmulbr  21255  dvfsumle  21335  dvfsumabs  21337  ig1peu  21528  taylfvallem1  21707  tayl0  21712  pilem2  21802  pilem3  21803  rlimcnp2  22245  xrlimcnp  22247  ppisval  22326  ppifi  22328  ppiprm  22374  ppinprm  22375  chtprm  22376  chtnprm  22377  chtdif  22381  efchtdvds  22382  ppidif  22386  ppiltx  22400  prmorcht  22401  ppiub  22428  chtlepsi  22430  chtleppi  22434  pclogsum  22439  vmasum  22440  chpval2  22442  chpchtsum  22443  chpub  22444  2sqlem8  22596  chebbnd1lem1  22603  chtppilimlem1  22607  rplogsumlem2  22619  rpvmasum2  22646  dchrisum0re  22647  rplogsum  22661  dirith2  22662  axtgcgrrflx  22808  axtgcgrid  22809  axtgsegcon  22810  axtg5seg  22811  axtgbtwnid  22812  axtgpasch  22813  axtgcont1  22814  opidon  23632  flddivrng  23725  phnv  24037  minvecolem2  24099  minvecolem3  24100  minvecolem5  24105  minvecolem6  24106  minvecolem7  24107  hlimcaui  24462  chdmm1i  24703  chabs1  24742  chabs2  24743  ledii  24762  lejdii  24764  pjoml4i  24813  cmbr3i  24826  cmbr4i  24827  cmm1i  24832  osumcor2i  24870  3oalem4  24891  pjssmii  24907  pjocini  24924  pjini  24925  mayete3i  24954  mayete3iOLD  24955  riesz4  25291  riesz1  25292  cnlnadjeui  25304  cnlnadjeu  25305  cnlnssadj  25307  nmopadjlei  25315  pjin1i  25419  pjclem1  25422  stji1i  25469  stm1i  25470  dmdbr2  25530  ssmd1  25538  mdslj2i  25547  mdsl2bi  25550  mdslmd1lem1  25552  mdslmd2i  25557  atomli  25609  atcvat4i  25624  sumdmdlem2  25646  dmdbr5ati  25649  dmdbr6ati  25650  dmdbr7ati  25651  disjin  25753  disjxpin  25754  imadifxp  25763  off2  25783  ffsrn  25854  gsumle  26098  xrge0tsmsd  26106  ordtrestNEW  26205  qqhnm  26273  qqhcn  26274  rrhre  26301  indf1ofs  26336  esumval  26354  esumel  26355  gsumesum  26364  esumlub  26365  esumcst  26368  esumfsup  26373  esumpcvgval  26381  esumcvg  26389  sigainb  26433  measunl  26484  measinb2  26491  sibfinima  26573  sibfof  26574  eulerpartlemelr  26588  eulerpartlem1  26598  eulerpartgbij  26603  eulerpartlemgvv  26607  eulerpartlemgu  26608  eulerpartlemgs2  26611  sseqf  26623  ballotlemfelz  26721  ballotlemfp1  26722  conpcon  26972  iccllyscon  26987  cvmsss2  27011  cvmcov2  27012  cvmopnlem  27015  cvmliftmolem2  27019  cvmliftlem15  27035  cvmlift2lem12  27051  nepss  27221  dfon2lem4  27446  predss  27479  wfrlem4  27574  frrlem4  27618  nofulllem5  27694  txpss3v  27756  fixssdm  27784  fixssrn  27785  limitssson  27789  ontopbas  28122  ptrest  28269  mblfinlem3  28274  mblfinlem4  28275  ismblfin  28276  mbfposadd  28283  fneer  28404  fnessref  28409  neibastop1  28424  neibastop2lem  28425  filnetlem3  28445  sstotbnd2  28517  ssbnd  28531  heibor1lem  28552  heiborlem1  28554  heiborlem3  28556  heiborlem5  28558  heiborlem6  28559  heiborlem10  28563  heibor  28564  exidcl  28585  elrfi  28875  elrfirn  28876  elrfirn2  28877  ismrcd1  28879  istopclsd  28881  isnacs2  28887  mrefg3  28889  isnacs3  28891  diophrw  28942  diophin  28956  aomclem2  29253  islmodfg  29267  lsmfgcl  29272  lmhmfgima  29282  lmhmfgsplit  29284  lmhmlnmsplit  29285  pwfi2f1o  29296  hbt  29331  acsfn1p  29401  onfrALTlem2  30955  onfrALTlem2VD  31327  bnj1292  31511  lshpinN  32207  lcvexchlem5  32256  pmodlem2  33064  pmod1i  33065  pmodN  33067  osumcllem7N  33179  pexmidlem4N  33190  pl42lem3N  33198  djaclN  34354  dihoml4c  34594  dochdmj1  34608  djhcl  34618  dochexmidlem4  34681  mapd1o  34866  mapdin  34880  taupilemrplb  35187  taupilem2  35189  taupi  35190
  Copyright terms: Public domain W3C validator