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

Theorem inss1 3465
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 3434 . . 3  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
21simplbi 446 . 2  |-  ( x  e.  ( A  i^i  B )  ->  x  e.  A )
32ssriv 3260 1  |-  ( A  i^i  B )  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1710    i^i cin 3227    C_ wss 3228
This theorem is referenced by:  inss2  3466  ssinss1  3473  unabs  3475  nssinpss  3477  dfin4  3485  inv1  3557  disjdif  3602  uniintsn  3980  epse  4458  wefrc  4469  ordtri3or  4506  onfr  4513  ordelinel  4573  relin1  4885  resss  5061  resmpt3  5083  cnvcnvss  5210  funin  5401  funimass2  5408  fnresin1  5440  fnres  5442  fresin  5493  fresaun  5495  fresaunres2  5496  nfvres  5640  ssimaex  5667  fneqeql2  5717  funiunfv  5861  isoini2  5923  ofrfval  6173  ofval  6174  ofrval  6175  off  6180  ofres  6181  ofco  6184  fparlem3  6307  fparlem4  6308  smores  6456  smores2  6458  pmresg  6883  sbthlem7  7065  sbthcl  7071  infi  7174  imafi  7238  ixpfi2  7244  unifpw  7248  f1opwfi  7249  fival  7256  fi0  7263  dffi2  7266  elfiun  7273  dffi3  7274  marypha1lem  7276  ordtypelem3  7325  ordtypelem4  7326  ordtypelem6  7328  ordtypelem7  7329  ordtypelem8  7330  wdomima2g  7390  epfrs  7503  tskwe  7673  r0weon  7730  fodomfi2  7777  infpwfien  7779  ackbij1lem6  7941  ackbij1lem9  7944  ackbij1lem10  7945  ackbij1lem11  7946  ackbij1lem15  7950  ackbij1lem16  7951  fin23lem24  8038  fin23lem26  8041  fin23lem23  8042  fin23lem22  8043  fin23lem19  8052  isfin1-3  8102  ttukeylem6  8231  brdom3  8243  brdom5  8244  brdom4  8245  imadomg  8249  fpwwe2lem12  8353  canthp1lem2  8365  wunin  8425  tskin  8471  gruima  8514  ingru  8527  gruina  8530  grur1a  8531  nqerf  8644  nqerrel  8646  hashun3  11459  hashdif  11471  rexanuz  11925  limsupgle  12047  rlimres  12128  lo1res  12129  lo1resb  12134  rlimresb  12135  o1resb  12136  lo1eq  12138  rlimeq  12139  o1of2  12182  o1rlimmul  12188  isercolllem2  12235  isercolllem3  12236  isercoll  12237  ackbijnn  12383  incexclem  12392  incexc  12393  bitsinvp1  12737  sadcaddlem  12745  sadadd2lem  12747  sadadd3  12749  sadaddlem  12754  sadasslem  12758  sadeq  12760  bitsres  12761  smuval2  12770  smupval  12776  smueqlem  12778  smumul  12781  prmreclem2  13061  ramub2  13158  ramub1lem2  13171  ressinbas  13301  ressress  13302  submre  13606  submrc  13629  isacs2  13654  isacs1i  13658  mreacs  13659  acsfn  13660  invss  13762  sscres  13799  coffth  13909  catcisolem  14037  catciso  14038  catcoppccl  14039  catcfuccl  14040  catcxpccl  14080  isdrs2  14172  isacs3lem  14368  isacs5lem  14371  acsfiindd  14379  psss  14422  psssdm2  14423  tsrss  14431  tsrdir  14459  resscntz  14906  sylow2a  15029  lsmmod  15083  frgpnabllem2  15261  gsumzres  15293  gsumzaddlem  15302  dprddisj2  15373  ablfac1eu  15407  ablfac2  15423  isunit  15538  lspextmo  15912  2idlval  16084  aspsubrg  16170  psrbagsn  16335  mplind  16342  zlpirlem2  16548  pjfval  16712  pjpm  16714  basdif0  16797  tgval2  16800  eltg3  16806  unitg  16811  tgcl  16813  tgdom  16822  tgidm  16824  ppttop  16850  epttop  16852  ntropn  16892  ntrin  16904  mretopd  16935  mreclatdemo  16939  restbas  16995  restfpw  17016  restcls  17017  ordtrest  17038  subbascn  17090  cncls  17109  cnpresti  17122  cnprest  17123  fincmp  17226  cmpsublem  17232  cmpsub  17233  fiuncmp  17237  indiscon  17250  connsub  17253  cnconn  17254  iunconlem  17259  clscon  17262  concompclo  17267  islly2  17316  cldllycmp  17327  kgentopon  17339  llycmpkgen2  17351  1stckgenlem  17354  ptbasfi  17382  txcls  17405  txcnp  17420  ptcnplem  17421  txcnmpt  17424  txcmplem2  17442  hausdiag  17445  txkgen  17452  xkopt  17455  xkococnlem  17459  txcon  17489  qtoptop2  17496  basqtop  17508  tgqtop  17509  kqnrmlem1  17540  kqnrmlem2  17541  nrmhmph  17591  fbssfi  17634  filin  17651  infil  17660  fbasrn  17681  fgtr  17687  ufprim  17706  flimrest  17780  hauspwpwf1  17784  txflf  17803  fclsrest  17821  alexsubALTlem3  17845  alexsubALTlem4  17846  ptcmplem5  17852  tsmsres  17928  tsmsxplem1  17937  xmetres  18030  metres  18031  blin2  18077  blbas  18078  blres  18079  setsmstopn  18126  met2ndci  18170  metrest  18172  ressxms  18173  tgioo  18404  xrsmopn  18420  zdis  18424  reconnlem1  18434  reconnlem2  18435  xrge0tsms  18442  cnheibor  18557  lebnum  18566  nmoleub2lem  18699  nmoleub2lem3  18700  nmoleub2lem2  18701  nmoleub3  18704  nmhmcn  18705  tchcph  18771  cfilresi  18825  cfilres  18826  caussi  18827  causs  18828  relcmpcmet  18846  minveclem4a  18898  minveclem4  18900  ismbl2  18990  cmmbl  18996  nulmbl2  18998  unmbl  18999  shftmbl  19000  volinun  19007  voliunlem1  19011  voliunlem2  19012  ioombl1lem4  19022  ioombl1  19023  ioorcl  19036  uniioombllem2  19042  uniioombllem3  19044  uniioombllem4  19045  uniioombllem5  19046  uniioombl  19048  volivth  19066  vitalilem3  19069  vitalilem4  19070  vitalilem5  19071  vitali  19072  mbfadd  19120  mbfsub  19121  i1fima2  19138  i1fd  19140  i1fadd  19154  itg1addlem2  19156  itg1addlem4  19158  itg1addlem5  19159  itg1climres  19173  mbfmul  19185  itg2splitlem  19207  itg2split  19208  limcresi  19339  limciun  19348  limcun  19349  dvreslem  19363  dvres2lem  19364  dvres  19365  dvres3a  19368  dvaddbr  19391  dvmulbr  19392  dvfsumle  19472  dvfsumabs  19474  ig1peu  19661  taylfvallem1  19840  tayl0  19845  pilem2  19935  pilem3  19936  rlimcnp2  20372  xrlimcnp  20374  ppisval  20453  ppifi  20455  ppiprm  20501  ppinprm  20502  chtprm  20503  chtnprm  20504  chtdif  20508  efchtdvds  20509  ppidif  20513  ppiltx  20527  prmorcht  20528  ppiub  20555  chtlepsi  20557  chtleppi  20561  pclogsum  20566  vmasum  20567  chpval2  20569  chpchtsum  20570  chpub  20571  2sqlem8  20723  chebbnd1lem1  20730  chtppilimlem1  20734  rplogsumlem2  20746  rpvmasum2  20773  dchrisum0re  20774  rplogsum  20788  dirith2  20789  opidon  21101  flddivrng  21194  phnv  21506  minvecolem2  21568  minvecolem3  21569  minvecolem5  21574  minvecolem6  21575  minvecolem7  21576  hlimcaui  21930  chdmm1i  22170  chabs1  22209  chabs2  22210  ledii  22229  lejdii  22231  pjoml4i  22280  cmbr3i  22293  cmbr4i  22294  cmm1i  22299  osumcor2i  22337  3oalem4  22358  pjssmii  22374  pjocini  22391  pjini  22392  mayete3i  22421  mayete3iOLD  22422  riesz4  22758  riesz1  22759  cnlnadjeui  22771  cnlnadjeu  22772  cnlnssadj  22774  nmopadjlei  22782  pjin1i  22886  pjclem1  22889  stji1i  22936  stm1i  22937  dmdbr2  22997  ssmd1  23005  mdslj2i  23014  mdsl2bi  23017  mdslmd1lem1  23019  mdslmd2i  23024  atomli  23076  atcvat4i  23091  sumdmdlem2  23113  dmdbr5ati  23116  dmdbr6ati  23117  dmdbr7ati  23118  disjin  23226  imadifxp  23241  off2  23258  xrge0tsmsd  23415  neiptoptop  23444  ustund  23526  trust  23533  utoptop  23538  restutop  23541  cfilucfil  23603  qqhnm  23647  qqhcn  23648  indf1ofs  23689  esumval  23707  esumel  23708  gsumesum  23717  esumlub  23718  esumcst  23721  esumfsup  23726  esumpcvgval  23734  esumcvg  23742  sigainb  23785  measunl  23834  measinb2  23841  ballotlemfelz  23997  ballotlemfp1  23998  conpcon  24170  iccllyscon  24185  cvmsss2  24209  cvmcov2  24210  cvmopnlem  24213  cvmliftmolem2  24217  cvmliftlem15  24233  cvmlift2lem12  24249  nepss  24476  dedekindle  24489  dfon2lem4  24700  predss  24731  wfrlem4  24817  frrlem4  24842  nofulllem5  24918  txpss3v  24976  fixssdm  25004  fixssrn  25005  ontopbas  25426  fneer  25612  fnessref  25617  neibastop1  25632  neibastop2lem  25633  filnetlem3  25653  sstotbnd2  25821  ssbnd  25835  heibor1lem  25856  heiborlem1  25858  heiborlem3  25860  heiborlem5  25862  heiborlem6  25863  heiborlem10  25867  heibor  25868  exidcl  25889  elrfi  26092  elrfirn  26093  elrfirn2  26094  ismrcd1  26096  istopclsd  26098  isnacs2  26104  mrefg3  26106  isnacs3  26108  diophrw  26161  diophin  26175  aomclem2  26475  islmodfg  26490  lsmfgcl  26495  lmhmfgima  26505  lmhmfgsplit  26507  lmhmlnmsplit  26508  frlmsplit2  26566  pwfi2f1o  26583  hbt  26657  acsfn1p  26830  onfrALTlem2  28056  onfrALTlem2VD  28427  bnj1292  28610  lshpinN  29248  lcvexchlem5  29297  pmodlem2  30105  pmod1i  30106  pmodN  30108  osumcllem7N  30220  pexmidlem4N  30231  pl42lem3N  30239  djaclN  31395  dihoml4c  31635  dochdmj1  31649  djhcl  31659  dochexmidlem4  31722  mapd1o  31907  mapdin  31921
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-v 2866  df-in 3235  df-ss 3242
  Copyright terms: Public domain W3C validator