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

Theorem inss1 3593
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

Proof of Theorem inss1
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 elin 3563 . . 3
21simplbi 448 . 2
32ssriv 3385 1
Colors of variables: wff set class
Syntax hints:  e.wcel 1724  i^icin 3352  C_wss 3353
This theorem is referenced by:  inss2  3594  ssinss1  3601  unabs  3603  nssinpss  3605  dfin4  3613  inv1  3686  disjdif  3773  uniintsn  4175  wefrc  4717  ordtri3or  4754  onfr  4761  ordelinel  4821  relin1  4961  resss  5139  resmpt3  5160  cnvcnvss  5291  funin  5482  funimass2  5489  fnresin1  5522  fnres  5524  fresin  5576  fresaun  5578  fresaunres2  5579  nfvres  5713  ssimaex  5749  fneqeql2  5801  funiunfv  5943  isoini2  6004  ofrfval  6295  ofval  6296  ofrval  6297  off  6301  ofres  6302  ofco  6306  fparlem3  6631  fparlem4  6632  smores  6726  smores2  6728  pmresg  7153  sbthlem7  7335  sbthcl  7341  infi  7444  imafi  7511  ixpfi2  7517  unifpw  7521  f1opwfi  7522  fival  7529  fi0  7537  dffi2  7540  elfiun  7547  dffi3  7548  marypha1lem  7550  ordtypelem3  7601  ordtypelem4  7602  ordtypelem6  7604  ordtypelem7  7605  ordtypelem8  7606  wdomima2g  7666  epfrs  7779  tskwe  7951  r0weon  8008  fodomfi2  8055  infpwfien  8057  ackbij1lem6  8219  ackbij1lem9  8222  ackbij1lem10  8223  ackbij1lem11  8224  ackbij1lem15  8228  ackbij1lem16  8229  fin23lem24  8316  fin23lem26  8319  fin23lem23  8320  fin23lem22  8321  fin23lem19  8330  isfin1-3  8380  ttukeylem6  8508  brdom3  8520  brdom5  8521  brdom4  8522  imadomg  8526  fpwwe2lem12  8630  canthp1lem2  8642  wunin  8702  tskin  8748  gruima  8791  ingru  8804  gruina  8807  grur1a  8808  nqerf  8921  nqerrel  8923  hashun3  11939  hashdif  11960  rexanuz  12619  limsupgle  12741  rlimres  12822  lo1res  12823  lo1resb  12828  rlimresb  12829  o1resb  12830  lo1eq  12832  rlimeq  12833  o1of2  12876  o1rlimmul  12882  isercolllem2  12929  isercolllem3  12930  isercoll  12931  ackbijnn  13077  incexclem  13085  incexc  13086  bitsinvp1  13431  sadcaddlem  13439  sadadd2lem  13441  sadadd3  13443  sadaddlem  13448  sadasslem  13452  sadeq  13454  bitsres  13455  smuval2  13464  smupval  13470  smueqlem  13472  smumul  13475  prmreclem2  13764  ramub2  13861  ramub1lem2  13874  ressinbas  14016  ressress  14017  submre  14321  submrc  14344  isacs2  14369  isacs1i  14373  mreacs  14374  acsfn  14375  invss  14477  sscres  14514  coffth  14624  catcisolem  14752  catciso  14753  catcoppccl  14754  catcfuccl  14755  catcxpccl  14795  isdrs2  14887  isacs3lem  15114  isacs5lem  15117  acsfiindd  15125  psss  15162  psssdm2  15163  tsrss  15171  tsrdir  15186  resscntz  15633  sylow2a  15756  lsmmod  15810  frgpnabllem2  15988  gsumzres  16020  gsumzaddlem  16029  dprddisj2  16100  ablfac1eu  16134  ablfac2  16150  isunit  16265  lspextmo  16635  2idlval  16807  aspsubrg  16893  psrbagsn  17058  mplind  17065  zlpirlem2  17272  pjfval  17436  pjpm  17438  basdif0  17521  tgval2  17524  eltg3  17530  unitg  17535  tgcl  17537  tgdom  17546  tgidm  17548  ppttop  17574  epttop  17576  ntropn  17616  ntrin  17628  mretopd  17659  mreclatdemoBAD  17663  neiptoptop  17698  restbas  17725  restfpw  17746  neitr  17747  restcls  17748  ordtrest  17769  subbascn  17821  cncls  17841  cnpresti  17855  cnprest  17856  fincmp  17959  cmpsublem  17965  cmpsub  17966  fiuncmp  17970  indiscon  17985  connsub  17988  cnconn  17989  iunconlem  17994  clscon  17997  concompclo  18002  islly2  18051  cldllycmp  18062  kgentopon  18074  llycmpkgen2  18086  1stckgenlem  18089  ptbasfi  18117  txcls  18140  txcnp  18156  ptcnplem  18157  txcnmpt  18160  txcmplem2  18178  hausdiag  18181  txkgen  18188  xkopt  18191  xkococnlem  18195  txcon  18225  qtoptop2  18235  basqtop  18247  tgqtop  18248  kqnrmlem1  18279  kqnrmlem2  18280  nrmhmph  18330  fbssfi  18373  filin  18390  infil  18399  fbasrn  18420  fgtr  18426  ufprim  18445  flimrest  18519  hauspwpwf1  18523  txflf  18542  fclsrest  18560  alexsubALTlem3  18584  alexsubALTlem4  18585  ptcmplem5  18591  tsmsres  18677  tsmsxplem1  18686  ustund  18755  trust  18763  utoptop  18768  restutop  18771  cfiluweak  18829  xmetres  18898  metres  18899  blin2  18963  blbas  18964  blres  18965  setsmstopn  19012  met2ndci  19056  metrest  19058  ressxms  19059  tgioo  19331  xrsmopn  19347  zdis  19351  reconnlem1  19361  reconnlem2  19362  xrge0tsms  19369  cnheibor  19484  lebnum  19493  nmoleub2lem  19626  nmoleub2lem3  19627  nmoleub2lem2  19628  nmoleub3  19631  nmhmcn  19632  tchcph  19698  cfilresi  19752  cfilres  19753  caussi  19754  causs  19755  relcmpcmet  19773  minveclem4a  19835  minveclem4  19837  ismbl2  19927  cmmbl  19933  nulmbl2  19935  unmbl  19936  shftmbl  19937  volinun  19944  voliunlem1  19948  voliunlem2  19949  ioombl1lem4  19959  ioombl1  19960  ioorcl  19973  uniioombllem2  19979  uniioombllem3  19981  uniioombllem4  19982  uniioombllem5  19983  uniioombl  19985  volivth  20003  vitalilem3  20006  vitalilem4  20007  vitalilem5  20008  vitali  20009  mbfadd  20055  mbfsub  20056  i1fima2  20073  i1fd  20075  i1fadd  20089  itg1addlem2  20091  itg1addlem4  20093  itg1addlem5  20094  itg1climres  20108  mbfmul  20120  itg2splitlem  20142  itg2split  20143  limcresi  20276  limciun  20285  limcun  20286  dvreslem  20300  dvres2lem  20301  dvres  20302  dvres3a  20305  dvaddbr  20328  dvmulbr  20329  dvfsumle  20409  dvfsumabs  20411  ig1peu  20598  taylfvallem1  20777  tayl0  20782  pilem2  20872  pilem3  20873  rlimcnp2  21314  xrlimcnp  21316  ppisval  21395  ppifi  21397  ppiprm  21443  ppinprm  21444  chtprm  21445  chtnprm  21446  chtdif  21450  efchtdvds  21451  ppidif  21455  ppiltx  21469  prmorcht  21470  ppiub  21497  chtlepsi  21499  chtleppi  21503  pclogsum  21508  vmasum  21509  chpval2  21511  chpchtsum  21512  chpub  21513  2sqlem8  21665  chebbnd1lem1  21672  chtppilimlem1  21676  rplogsumlem2  21688  rpvmasum2  21715  dchrisum0re  21716  rplogsum  21730  dirith2  21731  opidon  22419  flddivrng  22512  phnv  22824  minvecolem2  22886  minvecolem3  22887  minvecolem5  22892  minvecolem6  22893  minvecolem7  22894  hlimcaui  23249  chdmm1i  23490  chabs1  23529  chabs2  23530  ledii  23549  lejdii  23551  pjoml4i  23600  cmbr3i  23613  cmbr4i  23614  cmm1i  23619  osumcor2i  23657  3oalem4  23678  pjssmii  23694  pjocini  23711  pjini  23712  mayete3i  23741  mayete3iOLD  23742  riesz4  24078  riesz1  24079  cnlnadjeui  24091  cnlnadjeu  24092  cnlnssadj  24094  nmopadjlei  24102  pjin1i  24206  pjclem1  24209  stji1i  24256  stm1i  24257  dmdbr2  24317  ssmd1  24325  mdslj2i  24334  mdsl2bi  24337  mdslmd1lem1  24339  mdslmd2i  24344  atomli  24396  atcvat4i  24411  sumdmdlem2  24433  dmdbr5ati  24436  dmdbr6ati  24437  dmdbr7ati  24438  disjin  24548  disjxpin  24549  imadifxp  24558  off2  24580  ffsrn  24650  gsumle  24897  xrge0tsmsd  24905  ordtrestNEW  25021  qqhnm  25090  qqhcn  25091  rrhre  25118  indf1ofs  25153  esumval  25171  esumel  25172  gsumesum  25181  esumlub  25182  esumcst  25185  esumfsup  25190  esumpcvgval  25198  esumcvg  25206  sigainb  25250  measunl  25301  measinb2  25308  sibfinima  25390  sibfof  25391  eulerpartlemelr  25405  eulerpartlem1  25415  eulerpartgbij  25420  eulerpartlemgvv  25424  eulerpartlemgu  25425  eulerpartlemgs2  25428  ballotlemfelz  25514  ballotlemfp1  25515  conpcon  25761  iccllyscon  25776  cvmsss2  25800  cvmcov2  25801  cvmopnlem  25804  cvmliftmolem2  25808  cvmliftlem15  25824  cvmlift2lem12  25840  nepss  26005  dedekindle  26018  dfon2lem4  26243  predss  26276  wfrlem4  26371  frrlem4  26415  nofulllem5  26491  txpss3v  26553  fixssdm  26581  fixssrn  26582  limitssson  26586  ontopbas  27008  mblfinlem3  27101  mblfinlem4  27102  ismblfin  27103  mbfposadd  27110  fneer  27231  fnessref  27236  neibastop1  27251  neibastop2lem  27252  filnetlem3  27272  sstotbnd2  27346  ssbnd  27360  heibor1lem  27381  heiborlem1  27383  heiborlem3  27385  heiborlem5  27387  heiborlem6  27388  heiborlem10  27392  heibor  27393  exidcl  27414  elrfi  27679  elrfirn  27680  elrfirn2  27681  ismrcd1  27683  istopclsd  27685  isnacs2  27691  mrefg3  27693  isnacs3  27695  diophrw  27748  diophin  27762  aomclem2  28059  islmodfg  28073  lsmfgcl  28078  lmhmfgima  28088  lmhmfgsplit  28090  lmhmlnmsplit  28091  frlmsplit2  28149  pwfi2f1o  28166  hbt  28240  acsfn1p  28413  onfrALTlem2  29823  onfrALTlem2VD  30194  bnj1292  30380  lshpinN  31060  lcvexchlem5  31109  pmodlem2  31917  pmod1i  31918  pmodN  31920  osumcllem7N  32032  pexmidlem4N  32043  pl42lem3N  32051  djaclN  33207  dihoml4c  33447  dochdmj1  33461  djhcl  33471  dochexmidlem4  33534  mapd1o  33719  mapdin  33733
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-4 1573  ax-5 1636  ax-6 1677  ax-7 1697  ax-10 1743  ax-11 1748  ax-12 1760  ax-13 1947  ax-ext 2462
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1337  df-ex 1558  df-nf 1561  df-sb 1669  df-clab 2468  df-cleq 2474  df-clel 2477  df-nfc 2606  df-v 3008  df-in 3360  df-ss 3367
  Copyright terms: Public domain W3C validator