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

Theorem elin 3266
Description: Expansion of membership in an intersection of two classes. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 29-Apr-1994.)
Assertion
Ref Expression
elin  |-  ( A  e.  ( B  i^i  C )  <->  ( A  e.  B  /\  A  e.  C ) )

Proof of Theorem elin
StepHypRef Expression
1 elex 2735 . 2  |-  ( A  e.  ( B  i^i  C )  ->  A  e.  _V )
2 elex 2735 . . 3  |-  ( A  e.  C  ->  A  e.  _V )
32adantl 454 . 2  |-  ( ( A  e.  B  /\  A  e.  C )  ->  A  e.  _V )
4 eleq1 2313 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
5 eleq1 2313 . . . 4  |-  ( x  =  A  ->  (
x  e.  C  <->  A  e.  C ) )
64, 5anbi12d 694 . . 3  |-  ( x  =  A  ->  (
( x  e.  B  /\  x  e.  C
)  <->  ( A  e.  B  /\  A  e.  C ) ) )
7 df-in 3085 . . 3  |-  ( B  i^i  C )  =  { x  |  ( x  e.  B  /\  x  e.  C ) }
86, 7elab2g 2853 . 2  |-  ( A  e.  _V  ->  ( A  e.  ( B  i^i  C )  <->  ( A  e.  B  /\  A  e.  C ) ) )
91, 3, 8pm5.21nii 344 1  |-  ( A  e.  ( B  i^i  C )  <->  ( A  e.  B  /\  A  e.  C ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360    = wceq 1619    e. wcel 1621   _Vcvv 2727    i^i cin 3077
This theorem is referenced by:  elin2  3267  elin3  3268  incom  3269  ineqri  3270  ineq1  3271  inass  3286  inss1  3296  ssin  3298  ssrin  3301  dfss4  3310  difin  3313  indi  3322  undi  3323  unineq  3326  indifdir  3332  difin2  3337  inrab2  3348  inelcm  3416  difin0ss  3426  inssdif0  3427  inundif  3438  uniin  3747  intun  3792  intpr  3793  elrint  3801  iunin2  3864  iinin2  3870  elriin  3872  disjor  3904  disjiun  3910  brin  3967  trin  4020  inex1  4052  inuni  4071  wefrc  4280  ordtri3or  4317  ordpwsuc  4497  inopab  4723  inxp  4725  dmin  4793  opelres  4867  intasym  4965  asymref  4966  dminss  5002  imainss  5003  ssrnres  5023  cnvresima  5068  dfco2a  5079  2elresin  5212  respreima  5506  isomin  5686  isoini  5687  offval  5937  tfrlem5  6282  erdisj  6593  mapval2  6683  ixpin  6727  boxriin  6744  disjen  6903  ssenen  6920  onfin2  6937  elfpw  7041  unifpw  7042  f1opwfi  7043  fissuni  7044  fipreima  7045  elfir  7053  fiin  7059  inf3lem2  7214  cantnfcl  7252  epfrs  7297  cp  7445  bnd2  7447  tskwe  7467  infpwfidom  7539  infpwfien  7573  dfac5lem1  7634  dfac5lem5  7638  dfac5  7639  kmlem3  7662  kmlem14  7673  kmlem15  7674  ackbij2lem1  7729  ackbij1lem3  7732  ackbij1lem4  7733  ackbij1lem6  7735  ackbij1lem11  7740  fin23lem24  7832  fin23lem26  7835  isfin1-3  7896  fpwwe2lem12  8143  fpwwe  8148  canthnumlem  8150  pwxpndom2  8167  ingru  8317  gruina  8320  grur1  8322  axgroth4  8334  grothprim  8336  ixxdisj  10549  icodisj  10639  fzdisj  10695  uzdisj  10734  fzouzdisj  10780  fz1isolem  11276  limsupgle  11828  ello12  11867  elo12  11878  lo1resb  11915  rlimresb  11916  o1resb  11917  lo1eq  11919  rlimeq  11920  fsumsplit  12089  sumsplit  12108  fsum2dlem  12110  explecnv  12197  bitsmod  12501  saddisjlem  12529  sadadd  12532  sadass  12536  smuval2  12547  smupval  12553  smueqlem  12555  smumul  12558  prmreclem5  12841  prmrec  12843  4sqlem12  12877  vdwmc  12899  strfv2d  13052  submre  13379  submrc  13397  isacs2  13400  acsfn  13405  coffth  13654  catcoppccl  13784  catcfuccl  13785  catcxpccl  13825  isdrs2  13917  fpwipodrs  14111  psss  14158  subgacs  14487  nsgacs  14488  resscntz  14642  sylow2a  14765  lsmmod  14819  lsmdisj  14825  lsmdisj2  14826  subgdisj1  14835  frgpnabllem1  14996  gsumzsplit  15041  dmdprdd  15072  dprdfeq0  15092  dprdres  15098  subgdmdprd  15104  dprdcntz2  15108  dprddisj2  15109  dprd2da  15112  dmdprdsplit2lem  15115  ablfacrp  15136  pgpfac1lem3a  15146  pgpfac1lem3  15147  pgpfaclem1  15151  isrhm  15336  subsubrg2  15407  lssacs  15559  lspdisj  15713  lspdisjb  15714  isassa  15888  aspval  15900  aspid  15902  aspval2  15918  mplind  16075  zlpirlem1  16273  zlpirlem3  16275  dfprime2  16279  ocvin  16406  unocv  16412  iunocv  16413  obselocv  16460  isbasis2g  16518  baspartn  16524  tgval2  16526  bastg  16536  tgcl  16539  ppttop  16576  epttop  16578  clsval2  16619  ssntr  16627  isopn3  16635  ntreq0  16646  isclo  16656  restbas  16721  restntr  16744  restlp  16745  cnpresti  16848  cnprest  16849  cnprest2  16850  lmss  16858  haust1  16912  nrmsep3  16915  isnrm2  16918  lmmo  16940  cmpcovf  16950  fincmp  16952  0cmp  16953  discmp  16957  cmpsublem  16958  cmpsub  16959  uncmp  16962  hauscmplem  16965  iscon2  16972  conclo  16973  dfcon2  16977  iunconlem  16985  uncon  16987  is1stc2  17000  1stcrest  17011  1stcelcls  17019  llyi  17032  nllyi  17033  llynlly  17035  subislly  17039  restnlly  17040  restlly  17041  islly2  17042  llyrest  17043  nllyrest  17044  llyidm  17046  nllyidm  17047  hausllycmp  17052  cldllycmp  17053  lly1stc  17054  dislly  17055  llycmpkgen2  17077  1stckgenlem  17080  txcnp  17146  txcnmpt  17150  txlly  17162  txnlly  17163  txtube  17166  txcmplem1  17167  txcmplem2  17168  hausdiag  17171  xkococnlem  17185  basqtop  17234  tgqtop  17235  kqcldsat  17256  ptcmpfi  17336  isfbas2  17362  isfil2  17383  infil  17390  fbasfip  17395  elfg  17398  filcon  17410  rnelfmlem  17479  rnelfm  17480  fmfnfmlem2  17482  fmfnfmlem4  17484  fmfnfm  17485  flimrest  17510  hauspwpwf1  17514  fclsrest  17551  alexsubALTlem2  17574  alexsubALTlem3  17575  alexsubALTlem4  17576  alexsubALT  17577  ptcmp  17584  istmd  17589  istgp  17592  tgpconcompss  17628  tsmssubm  17657  tsmssplit  17666  istrg  17678  istdrg  17680  istlm  17699  bldisj  17787  blin  17802  blin2  17807  blres  17809  lpbl  17881  metrest  17902  isngp  17950  isnlm  18018  isnmhm  18087  tgioo  18134  xrtgioo  18144  xrsmopn  18150  zdis  18154  icccmplem1  18159  icccmplem2  18160  reconnlem2  18164  xrge0tsms  18171  icoopnst  18269  iocopnst  18270  cnheibor  18285  cnllycmp  18286  bndth  18288  iscph  18438  cphsqrcl  18452  tchcph  18499  cfilfcls  18532  cmetcaulem  18546  cmetss  18572  isbn  18592  cldcss2  18638  hlhil  18639  ovolfcl  18658  ovollb2lem  18679  ovolctb  18681  ovolshftlem1  18700  ovolscalem1  18704  ovolicc1  18707  ovolicc2lem2  18709  ovolicc2lem4  18711  ovolicc2lem5  18712  ovolicc2  18713  shftmbl  18728  volfiniun  18736  ioombl1lem1  18747  ioorf  18760  ioorcl  18764  dyadf  18778  vitalilem2  18796  vitali  18800  mbfmax  18836  mbfimaopnlem  18842  mbfaddlem  18847  mbfadd  18848  mbfsub  18849  i1faddlem  18880  i1fmullem  18881  i1fres  18892  itg1climres  18901  mbfi1fseqlem4  18905  mbfmul  18913  itg2splitlem  18935  itg2split  18936  itgresr  18965  bddmulibl  19025  ellimc2  19059  ellimc3  19061  limcun  19077  dvreslem  19091  dvres2lem  19092  dvaddbr  19119  dvmulbr  19120  dvne0  19190  lhop1lem  19192  lhop  19195  dvcnvrelem2  19197  itgsubstlem  19227  ig1peu  19389  ig1pval3  19392  aaliou2  19552  aaliou2b  19553  tayl0  19573  pilem1  19659  rlimcnp2  20093  xrlimcnp  20095  fsumharmonic  20137  ppisval  20173  ppisval2  20174  ppinprm  20222  chtnprm  20224  prmorcht  20248  fsumvma2  20285  pclogsum  20286  vmasum  20287  chpchtsum  20290  chpub  20291  2sqlem7  20441  chebbnd1lem1  20450  rpvmasum2  20493  issubgo  20800  isexid2  20822  smgrpismgm  20829  smgrpisass  20830  issmgrp  20831  mndoissmgrp  20836  mndoisexid  20837  mndomgmid  20839  ismndo  20840  rngo1cl  20926  minvecolem1  21283  minvecolem4a  21286  minvecolem4b  21287  minvecolem4  21289  h2hcau  21389  axhcompl-zf  21408  hhcmpl  21609  hhcms  21612  ocin  21705  ocnel  21707  shuni  21709  shmodsi  21798  pjhthlem2  21801  omlsilem  21811  pjoc1i  21840  spansnm0i  22077  nonbooli  22078  5oalem1  22081  5oalem2  22082  5oalem4  22084  5oalem5  22085  5oalem7  22087  3oalem2  22090  3oalem3  22091  pjssmii  22108  mayete3i  22155  mayete3iOLD  22156  nmcopex  22439  nmcoplb  22440  lncnopbd  22447  nmcfnex  22463  nmcfnlb  22464  riesz4  22474  riesz1  22475  riesz2  22476  cnlnadjlem3  22479  cnlnadjlem5  22481  cnlnadjlem9  22485  cnlnadjeu  22488  rnbra  22517  pjimai  22586  pjclem4a  22608  pjclem4  22609  pj3lem1  22616  pj3si  22617  jpi  22680  sumdmdii  22825  sumdmdlem  22828  sumdmdlem2  22829  cdjreui  22842  cdj3lem1  22844  cnllyscon  22947  rellyscon  22953  cvmsss2  22976  cvmcov2  22977  cvmopnlem  22980  dfres3  23286  dfon2lem4  23310  predel  23351  wfrlem5  23428  frrlem5  23453  axfelem18  23531  ellimits  23625  dfom5b  23627  brapply  23651  brcap  23653  dfrdg4  23662  tfrqfree  23663  onsucconi  24050  onintopsscon  24053  onsucsuccmpi  24056  limsucncmpi  24058  onint1  24062  uninqs  24204  splint  24213  inposet  24444  isdir2  24458  ablocomgrp  24508  fprodadd  24518  isfldOLD  24592  fldi  24593  zintdom  24604  unint2t  24684  intcont  24709  indcomp  24755  topunfincomp  24756  bwt2  24758  intrr  24865  intvconlem1  24869  issubcata  25012  vtarsuelt  25061  eltintpar  25065  inttaror  25066  inttarcar  25067  carinttar  25068  elcarelcl  25072  pfsubkl  25213  pgapspf  25218  isconcl6a  25269  isconcl6ab  25270  isconcl7a  25271  pxysxy  25308  lppotoslem  25309  lppotos  25310  nbssntrs  25313  cnvresimaOLD  25392  finminlem  25397  comppfsc  25473  neibastop2lem  25475  neibastop2  25476  neifg  25486  tailfb  25492  inixp  25565  0totbnd  25663  sstotbnd3  25666  blbnd  25677  ssbnd  25678  heibor1lem  25699  heibor1  25700  heiborlem1  25701  heiborlem6  25706  heiborlem8  25708  heibor  25711  exidresid  25735  isfld2  25796  prtlem14  25908  elrfi  25935  elrfirn  25936  cmpfiiin  25938  mrefg2  25948  fz1eqin  26014  fnwe2lem2  26314  dfac11  26326  kelac1  26327  kelac2lem  26328  dfac21  26330  islmodfg  26333  islssfg2  26335  islssfgi  26336  filnm  26358  lnr2i  26486  lpirlnr  26487  hbtlem6  26499  hbt  26500  acsfn1p  26673  subrgacs  26674  sdrgacs  26675  cntzsdrg  26676  onfrALTlem2  27004  onfrALTlem2VD  27355  bnj521  27454  bnj1153  27514  bnj1172  27720  bnj1173  27721  bnj1174  27722  bnj1279  27737  lshpdisj  27866  lkrin  28043  ishlat1  28231  pmodlem1  28724  pmodlem2  28725  pclfinN  28778  pclcmpatN  28779  osumcllem4N  28837  pexmidlem1N  28848  dihmeetlem1N  30169  dihglblem5apreN  30170  dihmeetlem4preN  30185  dihmeetlem13N  30198  dochnel2  30271  lcdlss  30498  mapd1o  30527  mapdunirnN  30529  baerlem3lem2  30589  baerlem5alem2  30590  baerlem5blem2  30591  hdmaprnlem9N  30739
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 1926  ax-ext 2234
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-in 3085
  Copyright terms: Public domain W3C validator