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

Theorem inss1 3549
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 3519 . . 3
21simplbi 448 . 2
32ssriv 3341 1
Colors of variables: wff set class
Syntax hints:  e.wcel 1728  i^icin 3308  C_wss 3309
This theorem is referenced by:  inss2  3550  ssinss1  3557  unabs  3559  nssinpss  3561  dfin4  3569  inv1  3642  disjdif  3726  uniintsn  4116  wefrc  4617  ordtri3or  4654  onfr  4661  ordelinel  4721  relin1  5034  resss  5214  resmpt3  5236  cnvcnvss  5369  funin  5567  funimass2  5574  fnresin1  5606  fnres  5608  fresin  5659  fresaun  5661  fresaunres2  5662  nfvres  5803  ssimaex  5836  fneqeql2  5887  funiunfv  6043  isoini2  6107  ofrfval  6363  ofval  6364  ofrval  6365  off  6370  ofres  6371  ofco  6374  fparlem3  6498  fparlem4  6499  smores  6663  smores2  6665  pmresg  7090  sbthlem7  7272  sbthcl  7278  infi  7381  imafi  7448  ixpfi2  7454  unifpw  7458  f1opwfi  7459  fival  7466  fi0  7474  dffi2  7477  elfiun  7484  dffi3  7485  marypha1lem  7487  ordtypelem3  7538  ordtypelem4  7539  ordtypelem6  7541  ordtypelem7  7542  ordtypelem8  7543  wdomima2g  7603  epfrs  7716  tskwe  7888  r0weon  7945  fodomfi2  7992  infpwfien  7994  ackbij1lem6  8156  ackbij1lem9  8159  ackbij1lem10  8160  ackbij1lem11  8161  ackbij1lem15  8165  ackbij1lem16  8166  fin23lem24  8253  fin23lem26  8256  fin23lem23  8257  fin23lem22  8258  fin23lem19  8267  isfin1-3  8317  ttukeylem6  8445  brdom3  8457  brdom5  8458  brdom4  8459  imadomg  8463  fpwwe2lem12  8567  canthp1lem2  8579  wunin  8639  tskin  8685  gruima  8728  ingru  8741  gruina  8744  grur1a  8745  nqerf  8858  nqerrel  8860  hashun3  11709  hashdif  11729  rexanuz  12200  limsupgle  12322  rlimres  12403  lo1res  12404  lo1resb  12409  rlimresb  12410  o1resb  12411  lo1eq  12413  rlimeq  12414  o1of2  12457  o1rlimmul  12463  isercolllem2  12510  isercolllem3  12511  isercoll  12512  ackbijnn  12658  incexclem  12667  incexc  12668  bitsinvp1  13012  sadcaddlem  13020  sadadd2lem  13022  sadadd3  13024  sadaddlem  13029  sadasslem  13033  sadeq  13035  bitsres  13036  smuval2  13045  smupval  13051  smueqlem  13053  smumul  13056  prmreclem2  13336  ramub2  13433  ramub1lem2  13446  ressinbas  13576  ressress  13577  submre  13881  submrc  13904  isacs2  13929  isacs1i  13933  mreacs  13934  acsfn  13935  invss  14037  sscres  14074  coffth  14184  catcisolem  14312  catciso  14313  catcoppccl  14314  catcfuccl  14315  catcxpccl  14355  isdrs2  14447  isacs3lem  14643  isacs5lem  14646  acsfiindd  14654  psss  14697  psssdm2  14698  tsrss  14706  tsrdir  14734  resscntz  15181  sylow2a  15304  lsmmod  15358  frgpnabllem2  15536  gsumzres  15568  gsumzaddlem  15577  dprddisj2  15648  ablfac1eu  15682  ablfac2  15698  isunit  15813  lspextmo  16183  2idlval  16355  aspsubrg  16441  psrbagsn  16606  mplind  16613  zlpirlem2  16820  pjfval  16984  pjpm  16986  basdif0  17069  tgval2  17072  eltg3  17078  unitg  17083  tgcl  17085  tgdom  17094  tgidm  17096  ppttop  17122  epttop  17124  ntropn  17164  ntrin  17176  mretopd  17207  mreclatdemo  17211  neiptoptop  17246  restbas  17273  restfpw  17294  neitr  17295  restcls  17296  ordtrest  17317  subbascn  17369  cncls  17389  cnpresti  17403  cnprest  17404  fincmp  17507  cmpsublem  17513  cmpsub  17514  fiuncmp  17518  indiscon  17532  connsub  17535  cnconn  17536  iunconlem  17541  clscon  17544  concompclo  17549  islly2  17598  cldllycmp  17609  kgentopon  17621  llycmpkgen2  17633  1stckgenlem  17636  ptbasfi  17664  txcls  17687  txcnp  17703  ptcnplem  17704  txcnmpt  17707  txcmplem2  17725  hausdiag  17728  txkgen  17735  xkopt  17738  xkococnlem  17742  txcon  17772  qtoptop2  17782  basqtop  17794  tgqtop  17795  kqnrmlem1  17826  kqnrmlem2  17827  nrmhmph  17877  fbssfi  17920  filin  17937  infil  17946  fbasrn  17967  fgtr  17973  ufprim  17992  flimrest  18066  hauspwpwf1  18070  txflf  18089  fclsrest  18107  alexsubALTlem3  18131  alexsubALTlem4  18132  ptcmplem5  18138  tsmsres  18224  tsmsxplem1  18233  ustund  18302  trust  18310  utoptop  18315  restutop  18318  cfiluweak  18376  xmetres  18445  metres  18446  blin2  18510  blbas  18511  blres  18512  setsmstopn  18559  met2ndci  18603  metrest  18605  ressxms  18606  tgioo  18878  xrsmopn  18894  zdis  18898  reconnlem1  18908  reconnlem2  18909  xrge0tsms  18916  cnheibor  19031  lebnum  19040  nmoleub2lem  19173  nmoleub2lem3  19174  nmoleub2lem2  19175  nmoleub3  19178  nmhmcn  19179  tchcph  19245  cfilresi  19299  cfilres  19300  caussi  19301  causs  19302  relcmpcmet  19320  minveclem4a  19382  minveclem4  19384  ismbl2  19474  cmmbl  19480  nulmbl2  19482  unmbl  19483  shftmbl  19484  volinun  19491  voliunlem1  19495  voliunlem2  19496  ioombl1lem4  19506  ioombl1  19507  ioorcl  19520  uniioombllem2  19526  uniioombllem3  19528  uniioombllem4  19529  uniioombllem5  19530  uniioombl  19532  volivth  19550  vitalilem3  19553  vitalilem4  19554  vitalilem5  19555  vitali  19556  mbfadd  19602  mbfsub  19603  i1fima2  19620  i1fd  19622  i1fadd  19636  itg1addlem2  19638  itg1addlem4  19640  itg1addlem5  19641  itg1climres  19655  mbfmul  19667  itg2splitlem  19689  itg2split  19690  limcresi  19823  limciun  19832  limcun  19833  dvreslem  19847  dvres2lem  19848  dvres  19849  dvres3a  19852  dvaddbr  19875  dvmulbr  19876  dvfsumle  19956  dvfsumabs  19958  ig1peu  20145  taylfvallem1  20324  tayl0  20329  pilem2  20419  pilem3  20420  rlimcnp2  20856  xrlimcnp  20858  ppisval  20937  ppifi  20939  ppiprm  20985  ppinprm  20986  chtprm  20987  chtnprm  20988  chtdif  20992  efchtdvds  20993  ppidif  20997  ppiltx  21011  prmorcht  21012  ppiub  21039  chtlepsi  21041  chtleppi  21045  pclogsum  21050  vmasum  21051  chpval2  21053  chpchtsum  21054  chpub  21055  2sqlem8  21207  chebbnd1lem1  21214  chtppilimlem1  21218  rplogsumlem2  21230  rpvmasum2  21257  dchrisum0re  21258  rplogsum  21272  dirith2  21273  opidon  21961  flddivrng  22054  phnv  22366  minvecolem2  22428  minvecolem3  22429  minvecolem5  22434  minvecolem6  22435  minvecolem7  22436  hlimcaui  22790  chdmm1i  23030  chabs1  23069  chabs2  23070  ledii  23089  lejdii  23091  pjoml4i  23140  cmbr3i  23153  cmbr4i  23154  cmm1i  23159  osumcor2i  23197  3oalem4  23218  pjssmii  23234  pjocini  23251  pjini  23252  mayete3i  23281  mayete3iOLD  23282  riesz4  23618  riesz1  23619  cnlnadjeui  23631  cnlnadjeu  23632  cnlnssadj  23634  nmopadjlei  23642  pjin1i  23746  pjclem1  23749  stji1i  23796  stm1i  23797  dmdbr2  23857  ssmd1  23865  mdslj2i  23874  mdsl2bi  23877  mdslmd1lem1  23879  mdslmd2i  23884  atomli  23936  atcvat4i  23951  sumdmdlem2  23973  dmdbr5ati  23976  dmdbr6ati  23977  dmdbr7ati  23978  disjin  24076  disjxpin  24077  imadifxp  24086  off2  24102  xrge0tsmsd  24272  qqhnm  24423  qqhcn  24424  rrhre  24436  indf1ofs  24472  esumval  24490  esumel  24491  gsumesum  24500  esumlub  24501  esumcst  24504  esumfsup  24509  esumpcvgval  24517  esumcvg  24525  sigainb  24568  measunl  24619  measinb2  24626  sibfof  24703  ffsrn  24726  eulerpartlemelr  24743  eulerpartlem1  24753  eulerpartgbij  24758  eulerpartlemgvv  24762  eulerpartlemgu  24763  eulerpartlemgs2  24766  ballotlemfelz  24852  ballotlemfp1  24853  conpcon  25026  iccllyscon  25041  cvmsss2  25065  cvmcov2  25066  cvmopnlem  25069  cvmliftmolem2  25073  cvmliftlem15  25089  cvmlift2lem12  25105  nepss  25279  dedekindle  25292  dfon2lem4  25517  predss  25550  wfrlem4  25645  frrlem4  25689  nofulllem5  25765  txpss3v  25827  fixssdm  25855  fixssrn  25856  limitssson  25860  ontopbas  26282  mblfinlem3  26354  mblfinlem4  26355  ismblfin  26356  mbfposadd  26363  fneer  26479  fnessref  26484  neibastop1  26499  neibastop2lem  26500  filnetlem3  26520  sstotbnd2  26594  ssbnd  26608  heibor1lem  26629  heiborlem1  26631  heiborlem3  26633  heiborlem5  26635  heiborlem6  26636  heiborlem10  26640  heibor  26641  exidcl  26662  elrfi  26929  elrfirn  26930  elrfirn2  26931  ismrcd1  26933  istopclsd  26935  isnacs2  26941  mrefg3  26943  isnacs3  26945  diophrw  26998  diophin  27012  aomclem2  27309  islmodfg  27323  lsmfgcl  27328  lmhmfgima  27338  lmhmfgsplit  27340  lmhmlnmsplit  27341  frlmsplit2  27399  pwfi2f1o  27416  hbt  27490  acsfn1p  27663  onfrALTlem2  28871  onfrALTlem2VD  29242  bnj1292  29428  lshpinN  30027  lcvexchlem5  30076  pmodlem2  30884  pmod1i  30885  pmodN  30887  osumcllem7N  30999  pexmidlem4N  31010  pl42lem3N  31018  djaclN  32174  dihoml4c  32414  dochdmj1  32428  djhcl  32438  dochexmidlem4  32501  mapd1o  32686  mapdin  32700
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-v 2967  df-in 3316  df-ss 3323
  Copyright terms: Public domain W3C validator