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

Theorem inss1 3553
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 3522 . . 3  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
21simplbi 447 . 2  |-  ( x  e.  ( A  i^i  B )  ->  x  e.  A )
32ssriv 3344 1  |-  ( A  i^i  B )  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1725    i^i cin 3311    C_ wss 3312
This theorem is referenced by:  inss2  3554  ssinss1  3561  unabs  3563  nssinpss  3565  dfin4  3573  inv1  3646  disjdif  3692  uniintsn  4079  wefrc  4568  ordtri3or  4605  onfr  4612  ordelinel  4671  relin1  4983  resss  5161  resmpt3  5183  cnvcnvss  5316  funin  5511  funimass2  5518  fnresin1  5550  fnres  5552  fresin  5603  fresaun  5605  fresaunres2  5606  nfvres  5751  ssimaex  5779  fneqeql2  5830  funiunfv  5986  isoini2  6050  ofrfval  6304  ofval  6305  ofrval  6306  off  6311  ofres  6312  ofco  6315  fparlem3  6439  fparlem4  6440  smores  6605  smores2  6607  pmresg  7032  sbthlem7  7214  sbthcl  7220  infi  7323  imafi  7390  ixpfi2  7396  unifpw  7400  f1opwfi  7401  fival  7408  fi0  7416  dffi2  7419  elfiun  7426  dffi3  7427  marypha1lem  7429  ordtypelem3  7478  ordtypelem4  7479  ordtypelem6  7481  ordtypelem7  7482  ordtypelem8  7483  wdomima2g  7543  epfrs  7656  tskwe  7826  r0weon  7883  fodomfi2  7930  infpwfien  7932  ackbij1lem6  8094  ackbij1lem9  8097  ackbij1lem10  8098  ackbij1lem11  8099  ackbij1lem15  8103  ackbij1lem16  8104  fin23lem24  8191  fin23lem26  8194  fin23lem23  8195  fin23lem22  8196  fin23lem19  8205  isfin1-3  8255  ttukeylem6  8383  brdom3  8395  brdom5  8396  brdom4  8397  imadomg  8401  fpwwe2lem12  8505  canthp1lem2  8517  wunin  8577  tskin  8623  gruima  8666  ingru  8679  gruina  8682  grur1a  8683  nqerf  8796  nqerrel  8798  hashun3  11646  hashdif  11666  rexanuz  12137  limsupgle  12259  rlimres  12340  lo1res  12341  lo1resb  12346  rlimresb  12347  o1resb  12348  lo1eq  12350  rlimeq  12351  o1of2  12394  o1rlimmul  12400  isercolllem2  12447  isercolllem3  12448  isercoll  12449  ackbijnn  12595  incexclem  12604  incexc  12605  bitsinvp1  12949  sadcaddlem  12957  sadadd2lem  12959  sadadd3  12961  sadaddlem  12966  sadasslem  12970  sadeq  12972  bitsres  12973  smuval2  12982  smupval  12988  smueqlem  12990  smumul  12993  prmreclem2  13273  ramub2  13370  ramub1lem2  13383  ressinbas  13513  ressress  13514  submre  13818  submrc  13841  isacs2  13866  isacs1i  13870  mreacs  13871  acsfn  13872  invss  13974  sscres  14011  coffth  14121  catcisolem  14249  catciso  14250  catcoppccl  14251  catcfuccl  14252  catcxpccl  14292  isdrs2  14384  isacs3lem  14580  isacs5lem  14583  acsfiindd  14591  psss  14634  psssdm2  14635  tsrss  14643  tsrdir  14671  resscntz  15118  sylow2a  15241  lsmmod  15295  frgpnabllem2  15473  gsumzres  15505  gsumzaddlem  15514  dprddisj2  15585  ablfac1eu  15619  ablfac2  15635  isunit  15750  lspextmo  16120  2idlval  16292  aspsubrg  16378  psrbagsn  16543  mplind  16550  zlpirlem2  16757  pjfval  16921  pjpm  16923  basdif0  17006  tgval2  17009  eltg3  17015  unitg  17020  tgcl  17022  tgdom  17031  tgidm  17033  ppttop  17059  epttop  17061  ntropn  17101  ntrin  17113  mretopd  17144  mreclatdemo  17148  neiptoptop  17183  restbas  17210  restfpw  17231  neitr  17232  restcls  17233  ordtrest  17254  subbascn  17306  cncls  17326  cnpresti  17340  cnprest  17341  fincmp  17444  cmpsublem  17450  cmpsub  17451  fiuncmp  17455  indiscon  17469  connsub  17472  cnconn  17473  iunconlem  17478  clscon  17481  concompclo  17486  islly2  17535  cldllycmp  17546  kgentopon  17558  llycmpkgen2  17570  1stckgenlem  17573  ptbasfi  17601  txcls  17624  txcnp  17640  ptcnplem  17641  txcnmpt  17644  txcmplem2  17662  hausdiag  17665  txkgen  17672  xkopt  17675  xkococnlem  17679  txcon  17709  qtoptop2  17719  basqtop  17731  tgqtop  17732  kqnrmlem1  17763  kqnrmlem2  17764  nrmhmph  17814  fbssfi  17857  filin  17874  infil  17883  fbasrn  17904  fgtr  17910  ufprim  17929  flimrest  18003  hauspwpwf1  18007  txflf  18026  fclsrest  18044  alexsubALTlem3  18068  alexsubALTlem4  18069  ptcmplem5  18075  tsmsres  18161  tsmsxplem1  18170  ustund  18239  trust  18247  utoptop  18252  restutop  18255  cfiluweak  18313  xmetres  18382  metres  18383  blin2  18447  blbas  18448  blres  18449  setsmstopn  18496  met2ndci  18540  metrest  18542  ressxms  18543  tgioo  18815  xrsmopn  18831  zdis  18835  reconnlem1  18845  reconnlem2  18846  xrge0tsms  18853  cnheibor  18968  lebnum  18977  nmoleub2lem  19110  nmoleub2lem3  19111  nmoleub2lem2  19112  nmoleub3  19115  nmhmcn  19116  tchcph  19182  cfilresi  19236  cfilres  19237  caussi  19238  causs  19239  relcmpcmet  19257  minveclem4a  19319  minveclem4  19321  ismbl2  19411  cmmbl  19417  nulmbl2  19419  unmbl  19420  shftmbl  19421  volinun  19428  voliunlem1  19432  voliunlem2  19433  ioombl1lem4  19443  ioombl1  19444  ioorcl  19457  uniioombllem2  19463  uniioombllem3  19465  uniioombllem4  19466  uniioombllem5  19467  uniioombl  19469  volivth  19487  vitalilem3  19490  vitalilem4  19491  vitalilem5  19492  vitali  19493  mbfadd  19541  mbfsub  19542  i1fima2  19559  i1fd  19561  i1fadd  19575  itg1addlem2  19577  itg1addlem4  19579  itg1addlem5  19580  itg1climres  19594  mbfmul  19606  itg2splitlem  19628  itg2split  19629  limcresi  19760  limciun  19769  limcun  19770  dvreslem  19784  dvres2lem  19785  dvres  19786  dvres3a  19789  dvaddbr  19812  dvmulbr  19813  dvfsumle  19893  dvfsumabs  19895  ig1peu  20082  taylfvallem1  20261  tayl0  20266  pilem2  20356  pilem3  20357  rlimcnp2  20793  xrlimcnp  20795  ppisval  20874  ppifi  20876  ppiprm  20922  ppinprm  20923  chtprm  20924  chtnprm  20925  chtdif  20929  efchtdvds  20930  ppidif  20934  ppiltx  20948  prmorcht  20949  ppiub  20976  chtlepsi  20978  chtleppi  20982  pclogsum  20987  vmasum  20988  chpval2  20990  chpchtsum  20991  chpub  20992  2sqlem8  21144  chebbnd1lem1  21151  chtppilimlem1  21155  rplogsumlem2  21167  rpvmasum2  21194  dchrisum0re  21195  rplogsum  21209  dirith2  21210  opidon  21898  flddivrng  21991  phnv  22303  minvecolem2  22365  minvecolem3  22366  minvecolem5  22371  minvecolem6  22372  minvecolem7  22373  hlimcaui  22727  chdmm1i  22967  chabs1  23006  chabs2  23007  ledii  23026  lejdii  23028  pjoml4i  23077  cmbr3i  23090  cmbr4i  23091  cmm1i  23096  osumcor2i  23134  3oalem4  23155  pjssmii  23171  pjocini  23188  pjini  23189  mayete3i  23218  mayete3iOLD  23219  riesz4  23555  riesz1  23556  cnlnadjeui  23568  cnlnadjeu  23569  cnlnssadj  23571  nmopadjlei  23579  pjin1i  23683  pjclem1  23686  stji1i  23733  stm1i  23734  dmdbr2  23794  ssmd1  23802  mdslj2i  23811  mdsl2bi  23814  mdslmd1lem1  23816  mdslmd2i  23821  atomli  23873  atcvat4i  23888  sumdmdlem2  23910  dmdbr5ati  23913  dmdbr6ati  23914  dmdbr7ati  23915  disjin  24015  disjxpin  24016  imadifxp  24026  off2  24042  xrge0tsmsd  24211  qqhnm  24362  qqhcn  24363  rrhre  24375  indf1ofs  24411  esumval  24429  esumel  24430  gsumesum  24439  esumlub  24440  esumcst  24443  esumfsup  24448  esumpcvgval  24456  esumcvg  24464  sigainb  24507  measunl  24558  measinb2  24565  sibfof  24642  ballotlemfelz  24736  ballotlemfp1  24737  conpcon  24910  iccllyscon  24925  cvmsss2  24949  cvmcov2  24950  cvmopnlem  24953  cvmliftmolem2  24957  cvmliftlem15  24973  cvmlift2lem12  24989  nepss  25163  dedekindle  25176  dfon2lem4  25397  predss  25428  wfrlem4  25514  frrlem4  25539  nofulllem5  25615  txpss3v  25673  fixssdm  25701  fixssrn  25702  ontopbas  26126  mblfinlem2  26191  mblfinlem3  26192  ismblfin  26193  mbfposadd  26200  fneer  26305  fnessref  26310  neibastop1  26325  neibastop2lem  26326  filnetlem3  26346  sstotbnd2  26420  ssbnd  26434  heibor1lem  26455  heiborlem1  26457  heiborlem3  26459  heiborlem5  26461  heiborlem6  26462  heiborlem10  26466  heibor  26467  exidcl  26488  elrfi  26685  elrfirn  26686  elrfirn2  26687  ismrcd1  26689  istopclsd  26691  isnacs2  26697  mrefg3  26699  isnacs3  26701  diophrw  26754  diophin  26768  aomclem2  27067  islmodfg  27082  lsmfgcl  27087  lmhmfgima  27097  lmhmfgsplit  27099  lmhmlnmsplit  27100  frlmsplit2  27158  pwfi2f1o  27175  hbt  27249  acsfn1p  27422  onfrALTlem2  28487  onfrALTlem2VD  28855  bnj1292  29041  lshpinN  29626  lcvexchlem5  29675  pmodlem2  30483  pmod1i  30484  pmodN  30486  osumcllem7N  30598  pexmidlem4N  30609  pl42lem3N  30617  djaclN  31773  dihoml4c  32013  dochdmj1  32027  djhcl  32037  dochexmidlem4  32100  mapd1o  32285  mapdin  32299
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator