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

Theorem elin 3358
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
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 elex 2796 . 2  |-  ( A  e.  ( B  i^i  C )  ->  A  e.  _V )
2 elex 2796 . . 3  |-  ( A  e.  C  ->  A  e.  _V )
32adantl 452 . 2  |-  ( ( A  e.  B  /\  A  e.  C )  ->  A  e.  _V )
4 eleq1 2343 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
5 eleq1 2343 . . . 4  |-  ( x  =  A  ->  (
x  e.  C  <->  A  e.  C ) )
64, 5anbi12d 691 . . 3  |-  ( x  =  A  ->  (
( x  e.  B  /\  x  e.  C
)  <->  ( A  e.  B  /\  A  e.  C ) ) )
7 df-in 3159 . . 3  |-  ( B  i^i  C )  =  { x  |  ( x  e.  B  /\  x  e.  C ) }
86, 7elab2g 2916 . 2  |-  ( A  e.  _V  ->  ( A  e.  ( B  i^i  C )  <->  ( A  e.  B  /\  A  e.  C ) ) )
91, 3, 8pm5.21nii 342 1  |-  ( A  e.  ( B  i^i  C )  <->  ( A  e.  B  /\  A  e.  C ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    = wceq 1623    e. wcel 1684   _Vcvv 2788    i^i cin 3151
This theorem is referenced by:  elin2  3359  elin3  3360  incom  3361  ineqri  3362  ineq1  3363  inass  3379  inss1  3389  ssin  3391  ssrin  3394  dfss4  3403  difin  3406  indi  3415  undi  3416  unineq  3419  indifdir  3425  difin2  3430  inrab2  3441  inelcm  3509  difin0ss  3520  inssdif0  3521  inundif  3532  uniin  3847  intun  3894  intpr  3895  elrint  3903  iunin2  3966  iinin2  3972  elriin  3974  disjor  4007  disjiun  4013  brin  4070  trin  4123  inex1  4155  inuni  4173  wefrc  4387  ordtri3or  4424  ordpwsuc  4606  inopab  4816  inxp  4818  dmin  4886  opelres  4960  intasym  5058  asymref  5059  dminss  5095  imainss  5096  ssrnres  5116  cnvresima  5162  dfco2a  5173  2elresin  5355  respreima  5654  isomin  5834  isoini  5835  offval  6085  tfrlem5  6396  erdisj  6707  mapval2  6797  ixpin  6841  boxriin  6858  disjen  7018  ssenen  7035  onfin2  7052  elfpw  7157  unifpw  7158  f1opwfi  7159  fissuni  7160  fipreima  7161  elfir  7169  fiin  7175  inf3lem2  7330  cantnfcl  7368  epfrs  7413  cp  7561  bnd2  7563  tskwe  7583  infpwfidom  7655  infpwfien  7689  dfac5lem1  7750  dfac5lem5  7754  dfac5  7755  kmlem3  7778  kmlem14  7789  kmlem15  7790  ackbij2lem1  7845  ackbij1lem3  7848  ackbij1lem4  7849  ackbij1lem6  7851  ackbij1lem11  7856  fin23lem24  7948  fin23lem26  7951  isfin1-3  8012  fpwwe2lem12  8263  fpwwe  8268  canthnumlem  8270  pwxpndom2  8287  ingru  8437  gruina  8440  grur1  8442  axgroth4  8454  grothprim  8456  ixxdisj  10671  icodisj  10761  fzdisj  10817  uzdisj  10856  fzouzdisj  10902  fz1isolem  11399  limsupgle  11951  ello12  11990  elo12  12001  lo1resb  12038  rlimresb  12039  o1resb  12040  lo1eq  12042  rlimeq  12043  fsumsplit  12212  sumsplit  12231  fsum2dlem  12233  explecnv  12323  bitsmod  12627  saddisjlem  12655  sadadd  12658  sadass  12662  smuval2  12673  smupval  12679  smueqlem  12681  smumul  12684  prmreclem5  12967  prmrec  12969  4sqlem12  13003  vdwmc  13025  strfv2d  13178  submre  13507  submrc  13530  isacs2  13555  acsfn  13561  coffth  13810  catcoppccl  13940  catcfuccl  13941  catcxpccl  13981  isdrs2  14073  fpwipodrs  14267  psss  14323  subgacs  14652  nsgacs  14653  resscntz  14807  sylow2a  14930  lsmmod  14984  lsmdisj  14990  lsmdisj2  14991  subgdisj1  15000  frgpnabllem1  15161  gsumzsplit  15206  dmdprdd  15237  dprdfeq0  15257  dprdres  15263  subgdmdprd  15269  dprdcntz2  15273  dprddisj2  15274  dprd2da  15277  dmdprdsplit2lem  15280  ablfacrp  15301  pgpfac1lem3a  15311  pgpfac1lem3  15312  pgpfaclem1  15316  isrhm  15501  subsubrg2  15572  lssacs  15724  lspdisj  15878  lspdisjb  15879  isassa  16056  aspval  16068  aspid  16070  aspval2  16086  mplind  16243  zlpirlem1  16441  zlpirlem3  16443  dfprm2  16447  ocvin  16574  unocv  16580  iunocv  16581  obselocv  16628  isbasis2g  16686  baspartn  16692  tgval2  16694  bastg  16704  tgcl  16707  ppttop  16744  epttop  16746  clsval2  16787  ssntr  16795  isopn3  16803  ntreq0  16814  isclo  16824  restbas  16889  restntr  16912  restlp  16913  cnpresti  17016  cnprest  17017  cnprest2  17018  lmss  17026  haust1  17080  nrmsep3  17083  isnrm2  17086  lmmo  17108  cmpcovf  17118  fincmp  17120  0cmp  17121  discmp  17125  cmpsublem  17126  cmpsub  17127  uncmp  17130  hauscmplem  17133  iscon2  17140  conclo  17141  dfcon2  17145  iunconlem  17153  uncon  17155  is1stc2  17168  1stcrest  17179  1stcelcls  17187  llyi  17200  nllyi  17201  llynlly  17203  subislly  17207  restnlly  17208  restlly  17209  islly2  17210  llyrest  17211  nllyrest  17212  llyidm  17214  nllyidm  17215  hausllycmp  17220  cldllycmp  17221  lly1stc  17222  dislly  17223  llycmpkgen2  17245  1stckgenlem  17248  txcnp  17314  txcnmpt  17318  txlly  17330  txnlly  17331  txtube  17334  txcmplem1  17335  txcmplem2  17336  hausdiag  17339  xkococnlem  17353  basqtop  17402  tgqtop  17403  kqcldsat  17424  ptcmpfi  17504  isfbas2  17530  isfil2  17551  infil  17558  fbasfip  17563  elfg  17566  filcon  17578  rnelfmlem  17647  rnelfm  17648  fmfnfmlem2  17650  fmfnfmlem4  17652  fmfnfm  17653  flimrest  17678  hauspwpwf1  17682  fclsrest  17719  alexsubALTlem2  17742  alexsubALTlem3  17743  alexsubALTlem4  17744  alexsubALT  17745  ptcmp  17752  istmd  17757  istgp  17760  tgpconcompss  17796  tsmssubm  17825  tsmssplit  17834  istrg  17846  istdrg  17848  istlm  17867  bldisj  17955  blin  17970  blin2  17975  blres  17977  lpbl  18049  metrest  18070  isngp  18118  isnlm  18186  isnmhm  18255  tgioo  18302  xrtgioo  18312  xrsmopn  18318  zdis  18322  icccmplem1  18327  icccmplem2  18328  reconnlem2  18332  xrge0tsms  18339  icoopnst  18437  iocopnst  18438  cnheibor  18453  cnllycmp  18454  bndth  18456  iscph  18606  cphsqrcl  18620  tchcph  18667  cfilfcls  18700  cmetcaulem  18714  cmetss  18740  isbn  18760  cldcss2  18806  hlhil  18807  ovolfcl  18826  ovollb2lem  18847  ovolctb  18849  ovolshftlem1  18868  ovolscalem1  18872  ovolicc1  18875  ovolicc2lem2  18877  ovolicc2lem4  18879  ovolicc2lem5  18880  ovolicc2  18881  shftmbl  18896  volfiniun  18904  ioombl1lem1  18915  ioorf  18928  ioorcl  18932  dyadf  18946  vitalilem2  18964  vitali  18968  mbfmax  19004  mbfimaopnlem  19010  mbfaddlem  19015  mbfadd  19016  mbfsub  19017  i1faddlem  19048  i1fmullem  19049  i1fres  19060  itg1climres  19069  mbfi1fseqlem4  19073  mbfmul  19081  itg2splitlem  19103  itg2split  19104  itgresr  19133  bddmulibl  19193  ellimc2  19227  ellimc3  19229  limcun  19245  dvreslem  19259  dvres2lem  19260  dvaddbr  19287  dvmulbr  19288  dvne0  19358  lhop1lem  19360  lhop  19363  dvcnvrelem2  19365  itgsubstlem  19395  ig1peu  19557  ig1pval3  19560  aaliou2  19720  aaliou2b  19721  tayl0  19741  pilem1  19827  rlimcnp2  20261  xrlimcnp  20263  fsumharmonic  20305  ppisval  20341  ppisval2  20342  ppinprm  20390  chtnprm  20392  prmorcht  20416  fsumvma2  20453  pclogsum  20454  vmasum  20455  chpchtsum  20458  chpub  20459  2sqlem7  20609  chebbnd1lem1  20618  rpvmasum2  20661  issubgo  20970  isexid2  20992  smgrpismgm  20999  smgrpisass  21000  issmgrp  21001  mndoissmgrp  21006  mndoisexid  21007  mndomgmid  21009  ismndo  21010  rngo1cl  21096  minvecolem1  21453  minvecolem4a  21456  minvecolem4b  21457  minvecolem4  21459  h2hcau  21559  axhcompl-zf  21578  hhcmpl  21779  hhcms  21782  ocin  21875  ocnel  21877  shuni  21879  shmodsi  21968  pjhthlem2  21971  omlsilem  21981  pjoc1i  22010  spansnm0i  22229  nonbooli  22230  5oalem1  22233  5oalem2  22234  5oalem4  22236  5oalem5  22237  5oalem7  22239  3oalem2  22242  3oalem3  22243  pjssmii  22260  mayete3i  22307  mayete3iOLD  22308  nmcopex  22609  nmcoplb  22610  lncnopbd  22617  nmcfnex  22633  nmcfnlb  22634  riesz4  22644  riesz1  22645  riesz2  22646  cnlnadjlem3  22649  cnlnadjlem5  22651  cnlnadjlem9  22655  cnlnadjeu  22658  rnbra  22687  pjimai  22756  pjclem4a  22778  pjclem4  22779  pj3lem1  22786  pj3si  22787  jpi  22850  sumdmdii  22995  sumdmdlem  22998  sumdmdlem2  22999  cdjreui  23012  cdj3lem1  23014  iocinioc2  23272  ssnnssfz  23277  cnre2csqima  23295  disjorf  23356  pnfneige0  23374  lmxrge0  23375  xrge0tsmsd  23382  esum0  23428  esumcst  23436  esumpcvgval  23446  esumcvg  23454  sigainb  23497  measvuni  23542  indf1ofs  23609  cnllyscon  23776  rellyscon  23782  cvmsss2  23805  cvmcov2  23806  cvmopnlem  23809  dfres3  24116  dfon2lem4  24142  predel  24183  wfrlem5  24260  frrlem5  24285  ellimits  24450  dfom5b  24452  brapply  24477  brcap  24479  dfrdg4  24488  tfrqfree  24489  onsucconi  24876  onintopsscon  24879  onsucsuccmpi  24882  limsucncmpi  24884  onint1  24888  uninqs  25039  splint  25048  inposet  25278  isdir2  25292  ablocomgrp  25342  fprodadd  25352  isfldOLD  25426  fldi  25427  zintdom  25438  unint2t  25518  intcont  25543  indcomp  25589  topunfincomp  25590  bwt2  25592  intrr  25699  intvconlem1  25703  issubcata  25846  vtarsuelt  25895  eltintpar  25899  inttaror  25900  inttarcar  25901  carinttar  25902  elcarelcl  25906  pfsubkl  26047  pgapspf  26052  isconcl6a  26103  isconcl6ab  26104  isconcl7a  26105  pxysxy  26142  lppotoslem  26143  lppotos  26144  nbssntrs  26147  cnvresimaOLD  26226  finminlem  26231  comppfsc  26307  neibastop2lem  26309  neibastop2  26310  neifg  26320  tailfb  26326  inixp  26399  0totbnd  26497  sstotbnd3  26500  blbnd  26511  ssbnd  26512  heibor1lem  26533  heibor1  26534  heiborlem1  26535  heiborlem6  26540  heiborlem8  26542  heibor  26545  exidresid  26569  isfld2  26630  prtlem14  26742  elrfi  26769  elrfirn  26770  cmpfiiin  26772  mrefg2  26782  fz1eqin  26848  fnwe2lem2  27148  dfac11  27160  kelac1  27161  kelac2lem  27162  dfac21  27164  islmodfg  27167  islssfg2  27169  islssfgi  27170  filnm  27192  lnr2i  27320  lpirlnr  27321  hbtlem6  27333  hbt  27334  acsfn1p  27507  subrgacs  27508  sdrgacs  27509  cntzsdrg  27510  stoweidlem39  27788  stoweidlem44  27793  stoweidlem50  27799  stoweidlem57  27806  eldmressn  27982  afvres  28034  onfrALTlem2  28311  onfrALTlem2VD  28665  bnj521  28765  bnj1153  28825  bnj1172  29031  bnj1173  29032  bnj1174  29033  bnj1279  29048  lshpdisj  29177  lkrin  29354  ishlat1  29542  pmodlem1  30035  pmodlem2  30036  pclfinN  30089  pclcmpatN  30090  osumcllem4N  30148  pexmidlem1N  30159  dihmeetlem1N  31480  dihglblem5apreN  31481  dihmeetlem4preN  31496  dihmeetlem13N  31509  dochnel2  31582  lcdlss  31809  mapd1o  31838  mapdunirnN  31840  baerlem3lem2  31900  baerlem5alem2  31901  baerlem5blem2  31902  hdmaprnlem9N  32050
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159
  Copyright terms: Public domain W3C validator