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

Theorem inss1 3547
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 3516 . . 3
21simplbi 450 . 2
32ssriv 3337 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1749  i^icin 3304  C_wss 3305
This theorem is referenced by:  inss2  3548  ssinss1  3555  unabs  3557  nssinpss  3559  dfin4  3567  inv1  3641  disjdif  3728  uniintsn  4140  wefrc  4685  ordtri3or  4722  onfr  4729  ordelinel  4788  relin1  4928  resss  5106  resmpt3  5129  cnvcnvss  5264  funin  5455  funimass2  5462  fnresin1  5495  fnres  5497  fresin  5550  fresaun  5552  fresaunres2  5553  nfvres  5690  ssimaex  5726  fneqeql2  5782  funiunfv  5933  isoini2  5998  ofrfval  6298  ofval  6299  ofrval  6300  off  6304  ofres  6305  ofco  6310  fparlem3  6643  fparlem4  6644  smores  6772  smores2  6774  tfrlem5  6798  pmresg  7199  sbthlem7  7386  sbthcl  7392  infi  7495  imafi  7563  ixpfi2  7568  unifpw  7573  f1opwfi  7574  fival  7609  fi0  7617  dffi2  7620  elfiun  7627  dffi3  7628  marypha1lem  7630  ordtypelem3  7681  ordtypelem4  7682  ordtypelem6  7684  ordtypelem7  7685  ordtypelem8  7686  wdomima2g  7748  epfrs  7898  tskwe  8067  r0weon  8126  fodomfi2  8177  infpwfien  8179  ackbij1lem6  8341  ackbij1lem9  8344  ackbij1lem10  8345  ackbij1lem11  8346  ackbij1lem15  8350  ackbij1lem16  8351  fin23lem24  8438  fin23lem26  8441  fin23lem23  8442  fin23lem22  8443  fin23lem19  8452  isfin1-3  8502  ttukeylem6  8630  brdom3  8642  brdom5  8643  brdom4  8644  imadomg  8648  fpwwe2lem12  8754  canthp1lem2  8766  wunin  8826  tskin  8872  gruima  8915  ingru  8928  gruina  8931  grur1a  8932  nqerf  9045  nqerrel  9047  dedekindle  9480  hashun3  12088  hashdif  12109  rexanuz  12774  limsupgle  12896  rlimres  12977  lo1res  12978  lo1resb  12983  rlimresb  12984  o1resb  12985  lo1eq  12987  rlimeq  12988  o1of2  13031  o1rlimmul  13037  isercolllem2  13084  isercolllem3  13085  isercoll  13086  ackbijnn  13231  incexclem  13239  incexc  13240  bitsinvp1  13585  sadcaddlem  13593  sadadd2lem  13595  sadadd3  13597  sadaddlem  13602  sadasslem  13606  sadeq  13608  bitsres  13609  smuval2  13618  smupval  13624  smueqlem  13626  smumul  13629  prmreclem2  13918  ramub2  14015  ramub1lem2  14028  fvsetsid  14139  ressinbas  14174  ressress  14175  submre  14483  submrc  14506  isacs2  14531  isacs1i  14535  mreacs  14536  acsfn  14537  invss  14639  sscres  14676  coffth  14786  catcisolem  14914  catciso  14915  catcoppccl  14916  catcfuccl  14917  catcxpccl  14957  isdrs2  15049  isacs3lem  15276  isacs5lem  15279  acsfiindd  15287  psss  15324  psssdm2  15325  tsrss  15333  tsrdir  15348  resscntz  15786  sylow2a  16055  lsmmod  16109  frgpnabllem2  16288  gsumzres  16320  gsumzaddlem  16329  dprddisj2  16406  ablfac1eu  16440  ablfac2  16456  isunit  16572  lspextmo  16946  2idlval  17124  aspsubrg  17210  psrbagsn  17379  mplind  17386  zringlpirlem2  17612  zlpirlem2  17617  pjfval  17839  pjpm  17841  frlmsplit2  17902  ofco2  18030  basdif0  18262  tgval2  18265  eltg3  18271  unitg  18276  tgcl  18278  tgdom  18287  tgidm  18289  ppttop  18315  epttop  18317  ntropn  18357  ntrin  18369  mretopd  18400  mreclatdemoBAD  18404  neiptoptop  18439  restbas  18466  restfpw  18487  neitr  18488  restcls  18489  ordtrest  18510  subbascn  18562  cncls  18582  cnpresti  18596  cnprest  18597  fincmp  18700  cmpsublem  18706  cmpsub  18707  fiuncmp  18711  indiscon  18726  connsub  18729  cnconn  18730  iunconlem  18735  clscon  18738  concompclo  18743  islly2  18792  cldllycmp  18803  kgentopon  18815  llycmpkgen2  18827  1stckgenlem  18830  ptbasfi  18858  txcls  18881  txcnp  18897  ptcnplem  18898  txcnmpt  18901  txcmplem2  18919  hausdiag  18922  txkgen  18929  xkopt  18932  xkococnlem  18936  txcon  18966  qtoptop2  18976  basqtop  18988  tgqtop  18989  kqnrmlem1  19020  kqnrmlem2  19021  nrmhmph  19071  fbssfi  19114  filin  19131  infil  19140  fbasrn  19161  fgtr  19167  ufprim  19186  flimrest  19260  hauspwpwf1  19264  txflf  19283  fclsrest  19301  alexsubALTlem3  19325  alexsubALTlem4  19326  ptcmplem5  19332  tsmsres  19418  tsmsxplem1  19427  ustund  19496  trust  19504  utoptop  19509  restutop  19512  cfiluweak  19570  xmetres  19639  metres  19640  blin2  19704  blbas  19705  blres  19706  setsmstopn  19753  met2ndci  19797  metrest  19799  ressxms  19800  tgioo  20073  xrsmopn  20089  zdis  20093  reconnlem1  20103  reconnlem2  20104  xrge0tsms  20111  cnheibor  20227  lebnum  20236  nmoleub2lem  20369  nmoleub2lem3  20370  nmoleub2lem2  20371  nmoleub3  20374  nmhmcn  20375  tchcph  20452  cfilresi  20506  cfilres  20507  caussi  20508  causs  20509  relcmpcmet  20527  minveclem4a  20617  minveclem4  20619  ismbl2  20710  cmmbl  20716  nulmbl2  20718  unmbl  20719  shftmbl  20720  volinun  20727  voliunlem1  20731  voliunlem2  20732  ioombl1lem4  20742  ioombl1  20743  ioorcl  20757  uniioombllem2  20763  uniioombllem3  20765  uniioombllem4  20766  uniioombllem5  20767  uniioombl  20769  volivth  20787  vitalilem3  20790  vitalilem4  20791  vitalilem5  20792  vitali  20793  mbfadd  20839  mbfsub  20840  i1fima2  20857  i1fd  20859  i1fadd  20873  itg1addlem2  20875  itg1addlem4  20877  itg1addlem5  20878  itg1climres  20892  mbfmul  20904  itg2splitlem  20926  itg2split  20927  limcresi  21060  limciun  21069  limcun  21070  dvreslem  21084  dvres2lem  21085  dvres  21086  dvres3a  21089  dvaddbr  21112  dvmulbr  21113  dvfsumle  21193  dvfsumabs  21195  ig1peu  21384  taylfvallem1  21563  tayl0  21568  pilem2  21658  pilem3  21659  rlimcnp2  22101  xrlimcnp  22103  ppisval  22182  ppifi  22184  ppiprm  22230  ppinprm  22231  chtprm  22232  chtnprm  22233  chtdif  22237  efchtdvds  22238  ppidif  22242  ppiltx  22256  prmorcht  22257  ppiub  22284  chtlepsi  22286  chtleppi  22290  pclogsum  22295  vmasum  22296  chpval2  22298  chpchtsum  22299  chpub  22300  2sqlem8  22452  chebbnd1lem1  22459  chtppilimlem1  22463  rplogsumlem2  22475  rpvmasum2  22502  dchrisum0re  22503  rplogsum  22517  dirith2  22518  axtgcgrrflx  22664  axtgcgrid  22665  axtgsegcon  22666  axtg5seg  22667  axtgbtwnid  22668  axtgpasch  22669  axtgcont1  22670  opidon  23488  flddivrng  23581  phnv  23893  minvecolem2  23955  minvecolem3  23956  minvecolem5  23961  minvecolem6  23962  minvecolem7  23963  hlimcaui  24318  chdmm1i  24559  chabs1  24598  chabs2  24599  ledii  24618  lejdii  24620  pjoml4i  24669  cmbr3i  24682  cmbr4i  24683  cmm1i  24688  osumcor2i  24726  3oalem4  24747  pjssmii  24763  pjocini  24780  pjini  24781  mayete3i  24810  mayete3iOLD  24811  riesz4  25147  riesz1  25148  cnlnadjeui  25160  cnlnadjeu  25161  cnlnssadj  25163  nmopadjlei  25171  pjin1i  25275  pjclem1  25278  stji1i  25325  stm1i  25326  dmdbr2  25386  ssmd1  25394  mdslj2i  25403  mdsl2bi  25406  mdslmd1lem1  25408  mdslmd2i  25413  atomli  25465  atcvat4i  25480  sumdmdlem2  25502  dmdbr5ati  25505  dmdbr6ati  25506  dmdbr7ati  25507  disjin  25609  disjxpin  25610  imadifxp  25619  off2  25639  ffsrn  25709  gsumle  25953  xrge0tsmsd  25961  ordtrestNEW  26060  qqhnm  26128  qqhcn  26129  rrhre  26156  indf1ofs  26191  esumval  26209  esumel  26210  gsumesum  26219  esumlub  26220  esumcst  26223  esumfsup  26228  esumpcvgval  26236  esumcvg  26244  sigainb  26288  measunl  26339  measinb2  26346  sibfinima  26428  sibfof  26429  eulerpartlemelr  26443  eulerpartlem1  26453  eulerpartgbij  26458  eulerpartlemgvv  26462  eulerpartlemgu  26463  eulerpartlemgs2  26466  sseqf  26478  ballotlemfelz  26576  ballotlemfp1  26577  conpcon  26827  iccllyscon  26842  cvmsss2  26866  cvmcov2  26867  cvmopnlem  26870  cvmliftmolem2  26874  cvmliftlem15  26890  cvmlift2lem12  26906  nepss  27076  dfon2lem4  27301  predss  27334  wfrlem4  27429  frrlem4  27473  nofulllem5  27549  txpss3v  27611  fixssdm  27639  fixssrn  27640  limitssson  27644  ontopbas  27977  ptrest  28096  mblfinlem3  28101  mblfinlem4  28102  ismblfin  28103  mbfposadd  28110  fneer  28231  fnessref  28236  neibastop1  28251  neibastop2lem  28252  filnetlem3  28272  sstotbnd2  28344  ssbnd  28358  heibor1lem  28379  heiborlem1  28381  heiborlem3  28383  heiborlem5  28385  heiborlem6  28386  heiborlem10  28390  heibor  28391  exidcl  28412  elrfi  28702  elrfirn  28703  elrfirn2  28704  ismrcd1  28706  istopclsd  28708  isnacs2  28714  mrefg3  28716  isnacs3  28718  diophrw  28770  diophin  28784  aomclem2  29081  islmodfg  29095  lsmfgcl  29100  lmhmfgima  29110  lmhmfgsplit  29112  lmhmlnmsplit  29113  pwfi2f1o  29124  hbt  29159  acsfn1p  29229  gsumXzres  30467  gsumXzaddlem  30478  onfrALTlem2  30831  onfrALTlem2VD  31203  bnj1292  31387  lshpinN  32071  lcvexchlem5  32120  pmodlem2  32928  pmod1i  32929  pmodN  32931  osumcllem7N  33043  pexmidlem4N  33054  pl42lem3N  33062  djaclN  34218  dihoml4c  34458  dochdmj1  34472  djhcl  34482  dochexmidlem4  34545  mapd1o  34730  mapdin  34744  taupilemrplb  35051  taupilem2  35053  taupi  35054
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-v 2953  df-in 3312  df-ss 3319
  Copyright terms: Public domain W3C validator