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

Theorem inss1 3350
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
StepHypRef Expression
1 elin 3319 . . 3  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
21simplbi 448 . 2  |-  ( x  e.  ( A  i^i  B )  ->  x  e.  A )
32ssriv 3145 1  |-  ( A  i^i  B )  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1621    i^i cin 3112    C_ wss 3113
This theorem is referenced by:  inss2  3351  ssinss1  3358  unabs  3360  nssinpss  3362  dfin4  3370  inv1  3442  disjdif  3487  uniintsn  3859  epse  4334  wefrc  4345  ordtri3or  4382  onfr  4389  ordelinel  4449  relin1  4777  resss  4953  resmpt3  4975  cnvcnvss  5102  funin  5243  funimass2  5250  fnresin1  5282  fnres  5284  fresin  5334  fresaun  5336  fresaunres2  5337  nfvres  5477  ssimaex  5504  fneqeql2  5554  funiunfv  5694  isoini2  5756  ofrfval  6006  ofval  6007  ofrval  6008  off  6013  ofres  6014  ofco  6017  fparlem3  6140  fparlem4  6141  smores  6323  smores2  6325  pmresg  6749  sbthlem7  6931  sbthcl  6937  imafi  7102  ixpfi2  7108  unifpw  7112  f1opwfi  7113  fival  7120  fi0  7127  dffi2  7130  elfiun  7137  dffi3  7138  marypha1lem  7140  ordtypelem3  7189  ordtypelem4  7190  ordtypelem6  7192  ordtypelem7  7193  ordtypelem8  7194  wdomima2g  7254  epfrs  7367  tskwe  7537  r0weon  7594  fodomfi2  7641  infpwfien  7643  ackbij1lem6  7805  ackbij1lem9  7808  ackbij1lem10  7809  ackbij1lem11  7810  ackbij1lem15  7814  ackbij1lem16  7815  fin23lem24  7902  fin23lem26  7905  fin23lem23  7906  fin23lem22  7907  fin23lem19  7916  isfin1-3  7966  ttukeylem6  8095  brdom3  8107  brdom5  8108  brdom4  8109  imadomg  8113  fpwwe2lem12  8217  canthp1lem2  8229  wunin  8289  tskin  8335  gruima  8378  ingru  8391  gruina  8394  grur1a  8395  nqerf  8508  nqerrel  8510  hashdif  11326  rexanuz  11780  limsupgle  11902  rlimres  11983  lo1res  11984  lo1resb  11989  rlimresb  11990  o1resb  11991  lo1eq  11993  rlimeq  11994  o1of2  12037  o1rlimmul  12043  isercolllem2  12090  isercolllem3  12091  isercoll  12092  ackbijnn  12237  bitsinvp1  12588  sadcaddlem  12596  sadadd2lem  12598  sadadd3  12600  sadaddlem  12605  sadasslem  12609  sadeq  12611  bitsres  12612  smuval2  12621  smupval  12627  smueqlem  12629  smumul  12632  prmreclem2  12912  ramub2  13009  ramub1lem2  13022  ressinbas  13152  ressress  13153  submre  13455  submrc  13478  isacs2  13503  isacs1i  13507  mreacs  13508  acsfn  13509  invss  13611  sscres  13648  coffth  13758  catcisolem  13886  catciso  13887  catcoppccl  13888  catcfuccl  13889  catcxpccl  13929  isdrs2  14021  isacs3lem  14217  isacs5lem  14220  acsfiindd  14228  psss  14271  psssdm2  14272  tsrss  14280  tsrdir  14308  resscntz  14755  sylow2a  14878  lsmmod  14932  frgpnabllem2  15110  gsumzres  15142  gsumzaddlem  15151  dprddisj2  15222  ablfac1eu  15256  ablfac2  15272  isunit  15387  lspextmo  15761  2idlval  15933  aspsubrg  16019  psrbagsn  16184  mplind  16191  zlpirlem2  16390  pjfval  16554  pjpm  16556  basdif0  16639  tgval2  16642  eltg3  16648  unitg  16653  tgcl  16655  tgdom  16664  tgidm  16666  ppttop  16692  epttop  16694  ntropn  16734  ntrin  16746  mretopd  16777  mreclatdemo  16781  restbas  16837  restfpw  16858  restcls  16859  ordtrest  16880  subbascn  16932  cncls  16951  cnpresti  16964  cnprest  16965  fincmp  17068  cmpsublem  17074  cmpsub  17075  fiuncmp  17079  indiscon  17092  connsub  17095  cnconn  17096  iunconlem  17101  clscon  17104  concompclo  17109  islly2  17158  cldllycmp  17169  kgentopon  17181  llycmpkgen2  17193  1stckgenlem  17196  ptbasfi  17224  txcls  17247  txcnp  17262  ptcnplem  17263  txcnmpt  17266  txcmplem2  17284  hausdiag  17287  txkgen  17294  xkopt  17297  xkococnlem  17301  txcon  17331  qtoptop2  17338  basqtop  17350  tgqtop  17351  kqnrmlem1  17382  kqnrmlem2  17383  nrmhmph  17433  fbssfi  17480  filin  17497  infil  17506  fbasrn  17527  fgtr  17533  ufprim  17552  flimrest  17626  hauspwpwf1  17630  txflf  17649  fclsrest  17667  alexsubALTlem3  17691  alexsubALTlem4  17692  ptcmplem5  17698  tsmsres  17774  tsmsxplem1  17783  xmetres  17876  metres  17877  blin2  17923  blbas  17924  blres  17925  setsmstopn  17972  met2ndci  18016  metrest  18018  ressxms  18019  tgioo  18250  xrsmopn  18266  zdis  18270  reconnlem1  18279  reconnlem2  18280  xrge0tsms  18287  cnheibor  18401  lebnum  18410  nmoleub2lem  18543  nmoleub2lem3  18544  nmoleub2lem2  18545  nmoleub3  18548  nmhmcn  18549  tchcph  18615  cfilresi  18669  cfilres  18670  caussi  18671  causs  18672  relcmpcmet  18690  minveclem4a  18742  minveclem4  18744  ismbl2  18834  cmmbl  18840  nulmbl2  18842  unmbl  18843  shftmbl  18844  volinun  18851  voliunlem1  18855  voliunlem2  18856  ioombl1lem4  18866  ioombl1  18867  ioorcl  18880  uniioombllem2  18886  uniioombllem3  18888  uniioombllem4  18889  uniioombllem5  18890  uniioombl  18892  volivth  18910  vitalilem3  18913  vitalilem4  18914  vitalilem5  18915  vitali  18916  mbfadd  18964  mbfsub  18965  i1fima2  18982  i1fd  18984  i1fadd  18998  itg1addlem2  19000  itg1addlem4  19002  itg1addlem5  19003  itg1climres  19017  mbfmul  19029  itg2splitlem  19051  itg2split  19052  limcresi  19183  limciun  19192  limcun  19193  dvreslem  19207  dvres2lem  19208  dvres  19209  dvres3a  19212  dvaddbr  19235  dvmulbr  19236  dvfsumle  19316  dvfsumabs  19318  ig1peu  19505  taylfvallem1  19684  tayl0  19689  pilem2  19776  pilem3  19777  rlimcnp2  20209  xrlimcnp  20211  ppisval  20289  ppifi  20291  ppiprm  20337  ppinprm  20338  chtprm  20339  chtnprm  20340  chtdif  20344  efchtdvds  20345  ppidif  20349  ppiltx  20363  prmorcht  20364  ppiub  20391  chtlepsi  20393  chtleppi  20397  pclogsum  20402  vmasum  20403  chpval2  20405  chpchtsum  20406  chpub  20407  2sqlem8  20559  chebbnd1lem1  20566  chtppilimlem1  20570  rplogsumlem2  20582  rpvmasum2  20609  dchrisum0re  20610  rplogsum  20624  dirith2  20625  opidon  20935  flddivrng  21028  phnv  21338  minvecolem2  21400  minvecolem3  21401  minvecolem5  21406  minvecolem6  21407  minvecolem7  21408  hlimcaui  21762  chdmm1i  22002  chabs1  22041  chabs2  22042  ledii  22061  lejdii  22063  pjoml4i  22130  cmbr3i  22143  cmbr4i  22144  cmm1i  22149  osumcor2i  22187  3oalem4  22208  pjssmii  22224  pjocini  22241  pjini  22242  mayete3i  22271  mayete3iOLD  22272  riesz4  22590  riesz1  22591  cnlnadjeui  22603  cnlnadjeu  22604  cnlnssadj  22606  nmopadjlei  22614  pjin1i  22718  pjclem1  22721  stji1i  22768  stm1i  22769  dmdbr2  22829  ssmd1  22837  mdslj2i  22846  mdsl2bi  22849  mdslmd1lem1  22851  mdslmd2i  22856  atomli  22908  atcvat4i  22923  sumdmdlem2  22945  dmdbr5ati  22948  dmdbr6ati  22949  dmdbr7ati  22950  infi  22975  ballotlemfelz  22996  ballotlemfp1  22997  conpcon  23124  iccllyscon  23139  cvmsss2  23163  cvmcov2  23164  cvmopnlem  23167  cvmliftmolem2  23171  cvmliftlem15  23187  cvmlift2lem12  23203  nepss  23430  dedekindle  23440  dfon2lem4  23497  predss  23528  wfrlem4  23614  frrlem4  23639  txpss3v  23780  fixssdm  23808  fixssrn  23809  ontopbas  24228  domintrefb  24415  posprsr  24593  dfps2  24642  toplat  24643  reacomsmgrp1  24696  reacomsmgrp2  24697  reacomsmgrp3  24698  reacomsmgrp4  24699  clfsebsr  24702  resgcom  24704  clsint  24866  unint2t  24871  limptlimpr2lem2  24928  flfnei2  24930  islimrs4  24935  stfincomp  24944  lvsovso  24979  hdrmp  25059  inttaror  25253  fneer  25641  fnessref  25646  neibastop1  25661  neibastop2lem  25662  filnetlem3  25682  sstotbnd2  25851  ssbnd  25865  heibor1lem  25886  heiborlem1  25888  heiborlem3  25890  heiborlem5  25892  heiborlem6  25893  heiborlem10  25897  heibor  25898  exidcl  25919  elrfi  26122  elrfirn  26123  elrfirn2  26124  ismrcd1  26126  istopclsd  26128  isnacs2  26134  mrefg3  26136  isnacs3  26138  diophrw  26191  diophin  26205  aomclem2  26505  islmodfg  26520  lsmfgcl  26525  lmhmfgima  26535  lmhmfgsplit  26537  lmhmlnmsplit  26538  frlmsplit2  26596  pwfi2f1o  26613  hbt  26687  acsfn1p  26860  onfrALTlem2  27348  onfrALTlem2VD  27699  bnj1292  27881  lshpinN  28330  lcvexchlem5  28379  pmodlem2  29187  pmod1i  29188  pmodN  29190  osumcllem7N  29302  pexmidlem4N  29313  pl42lem3N  29321  djaclN  30477  dihoml4c  30717  dochdmj1  30731  djhcl  30741  dochexmidlem4  30804  mapd1o  30989  mapdin  31003
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2759  df-in 3120  df-ss 3127
  Copyright terms: Public domain W3C validator