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

Theorem elin 3359
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 2797 . 2  |-  ( A  e.  ( B  i^i  C )  ->  A  e.  _V )
2 elex 2797 . . 3  |-  ( A  e.  C  ->  A  e.  _V )
32adantl 452 . 2  |-  ( ( A  e.  B  /\  A  e.  C )  ->  A  e.  _V )
4 eleq1 2344 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
5 eleq1 2344 . . . 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 3160 . . 3  |-  ( B  i^i  C )  =  { x  |  ( x  e.  B  /\  x  e.  C ) }
86, 7elab2g 2917 . 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 1685   _Vcvv 2789    i^i cin 3152
This theorem is referenced by:  elin2  3360  elin3  3361  incom  3362  ineqri  3363  ineq1  3364  inass  3380  inss1  3390  ssin  3392  ssrin  3395  dfss4  3404  difin  3407  indi  3416  undi  3417  unineq  3420  indifdir  3426  difin2  3431  inrab2  3442  inelcm  3510  difin0ss  3521  inssdif0  3522  inundif  3533  uniin  3848  intun  3895  intpr  3896  elrint  3904  iunin2  3967  iinin2  3973  elriin  3975  disjor  4008  disjiun  4014  brin  4071  trin  4124  inex1  4156  inuni  4176  wefrc  4386  ordtri3or  4423  ordpwsuc  4605  inopab  4815  inxp  4817  dmin  4885  opelres  4959  intasym  5057  asymref  5058  dminss  5094  imainss  5095  ssrnres  5115  cnvresima  5160  dfco2a  5171  2elresin  5321  respreima  5616  isomin  5796  isoini  5797  offval  6047  tfrlem5  6392  erdisj  6703  mapval2  6793  ixpin  6837  boxriin  6854  disjen  7014  ssenen  7031  onfin2  7048  elfpw  7153  unifpw  7154  f1opwfi  7155  fissuni  7156  fipreima  7157  elfir  7165  fiin  7171  inf3lem2  7326  cantnfcl  7364  epfrs  7409  cp  7557  bnd2  7559  tskwe  7579  infpwfidom  7651  infpwfien  7685  dfac5lem1  7746  dfac5lem5  7750  dfac5  7751  kmlem3  7774  kmlem14  7785  kmlem15  7786  ackbij2lem1  7841  ackbij1lem3  7844  ackbij1lem4  7845  ackbij1lem6  7847  ackbij1lem11  7852  fin23lem24  7944  fin23lem26  7947  isfin1-3  8008  fpwwe2lem12  8259  fpwwe  8264  canthnumlem  8266  pwxpndom2  8283  ingru  8433  gruina  8436  grur1  8438  axgroth4  8450  grothprim  8452  ixxdisj  10667  icodisj  10757  fzdisj  10813  uzdisj  10852  fzouzdisj  10898  fz1isolem  11395  limsupgle  11947  ello12  11986  elo12  11997  lo1resb  12034  rlimresb  12035  o1resb  12036  lo1eq  12038  rlimeq  12039  fsumsplit  12208  sumsplit  12227  fsum2dlem  12229  explecnv  12319  bitsmod  12623  saddisjlem  12651  sadadd  12654  sadass  12658  smuval2  12669  smupval  12675  smueqlem  12677  smumul  12680  prmreclem5  12963  prmrec  12965  4sqlem12  12999  vdwmc  13021  strfv2d  13174  submre  13503  submrc  13526  isacs2  13551  acsfn  13557  coffth  13806  catcoppccl  13936  catcfuccl  13937  catcxpccl  13977  isdrs2  14069  fpwipodrs  14263  psss  14319  subgacs  14648  nsgacs  14649  resscntz  14803  sylow2a  14926  lsmmod  14980  lsmdisj  14986  lsmdisj2  14987  subgdisj1  14996  frgpnabllem1  15157  gsumzsplit  15202  dmdprdd  15233  dprdfeq0  15253  dprdres  15259  subgdmdprd  15265  dprdcntz2  15269  dprddisj2  15270  dprd2da  15273  dmdprdsplit2lem  15276  ablfacrp  15297  pgpfac1lem3a  15307  pgpfac1lem3  15308  pgpfaclem1  15312  isrhm  15497  subsubrg2  15568  lssacs  15720  lspdisj  15874  lspdisjb  15875  isassa  16052  aspval  16064  aspid  16066  aspval2  16082  mplind  16239  zlpirlem1  16437  zlpirlem3  16439  dfprm2  16443  ocvin  16570  unocv  16576  iunocv  16577  obselocv  16624  isbasis2g  16682  baspartn  16688  tgval2  16690  bastg  16700  tgcl  16703  ppttop  16740  epttop  16742  clsval2  16783  ssntr  16791  isopn3  16799  ntreq0  16810  isclo  16820  restbas  16885  restntr  16908  restlp  16909  cnpresti  17012  cnprest  17013  cnprest2  17014  lmss  17022  haust1  17076  nrmsep3  17079  isnrm2  17082  lmmo  17104  cmpcovf  17114  fincmp  17116  0cmp  17117  discmp  17121  cmpsublem  17122  cmpsub  17123  uncmp  17126  hauscmplem  17129  iscon2  17136  conclo  17137  dfcon2  17141  iunconlem  17149  uncon  17151  is1stc2  17164  1stcrest  17175  1stcelcls  17183  llyi  17196  nllyi  17197  llynlly  17199  subislly  17203  restnlly  17204  restlly  17205  islly2  17206  llyrest  17207  nllyrest  17208  llyidm  17210  nllyidm  17211  hausllycmp  17216  cldllycmp  17217  lly1stc  17218  dislly  17219  llycmpkgen2  17241  1stckgenlem  17244  txcnp  17310  txcnmpt  17314  txlly  17326  txnlly  17327  txtube  17330  txcmplem1  17331  txcmplem2  17332  hausdiag  17335  xkococnlem  17349  basqtop  17398  tgqtop  17399  kqcldsat  17420  ptcmpfi  17500  isfbas2  17526  isfil2  17547  infil  17554  fbasfip  17559  elfg  17562  filcon  17574  rnelfmlem  17643  rnelfm  17644  fmfnfmlem2  17646  fmfnfmlem4  17648  fmfnfm  17649  flimrest  17674  hauspwpwf1  17678  fclsrest  17715  alexsubALTlem2  17738  alexsubALTlem3  17739  alexsubALTlem4  17740  alexsubALT  17741  ptcmp  17748  istmd  17753  istgp  17756  tgpconcompss  17792  tsmssubm  17821  tsmssplit  17830  istrg  17842  istdrg  17844  istlm  17863  bldisj  17951  blin  17966  blin2  17971  blres  17973  lpbl  18045  metrest  18066  isngp  18114  isnlm  18182  isnmhm  18251  tgioo  18298  xrtgioo  18308  xrsmopn  18314  zdis  18318  icccmplem1  18323  icccmplem2  18324  reconnlem2  18328  xrge0tsms  18335  icoopnst  18433  iocopnst  18434  cnheibor  18449  cnllycmp  18450  bndth  18452  iscph  18602  cphsqrcl  18616  tchcph  18663  cfilfcls  18696  cmetcaulem  18710  cmetss  18736  isbn  18756  cldcss2  18802  hlhil  18803  ovolfcl  18822  ovollb2lem  18843  ovolctb  18845  ovolshftlem1  18864  ovolscalem1  18868  ovolicc1  18871  ovolicc2lem2  18873  ovolicc2lem4  18875  ovolicc2lem5  18876  ovolicc2  18877  shftmbl  18892  volfiniun  18900  ioombl1lem1  18911  ioorf  18924  ioorcl  18928  dyadf  18942  vitalilem2  18960  vitali  18964  mbfmax  19000  mbfimaopnlem  19006  mbfaddlem  19011  mbfadd  19012  mbfsub  19013  i1faddlem  19044  i1fmullem  19045  i1fres  19056  itg1climres  19065  mbfi1fseqlem4  19069  mbfmul  19077  itg2splitlem  19099  itg2split  19100  itgresr  19129  bddmulibl  19189  ellimc2  19223  ellimc3  19225  limcun  19241  dvreslem  19255  dvres2lem  19256  dvaddbr  19283  dvmulbr  19284  dvne0  19354  lhop1lem  19356  lhop  19359  dvcnvrelem2  19361  itgsubstlem  19391  ig1peu  19553  ig1pval3  19556  aaliou2  19716  aaliou2b  19717  tayl0  19737  pilem1  19823  rlimcnp2  20257  xrlimcnp  20259  fsumharmonic  20301  ppisval  20337  ppisval2  20338  ppinprm  20386  chtnprm  20388  prmorcht  20412  fsumvma2  20449  pclogsum  20450  vmasum  20451  chpchtsum  20454  chpub  20455  2sqlem7  20605  chebbnd1lem1  20614  rpvmasum2  20657  issubgo  20964  isexid2  20986  smgrpismgm  20993  smgrpisass  20994  issmgrp  20995  mndoissmgrp  21000  mndoisexid  21001  mndomgmid  21003  ismndo  21004  rngo1cl  21090  minvecolem1  21447  minvecolem4a  21450  minvecolem4b  21451  minvecolem4  21453  h2hcau  21555  axhcompl-zf  21574  hhcmpl  21775  hhcms  21778  ocin  21871  ocnel  21873  shuni  21875  shmodsi  21964  pjhthlem2  21967  omlsilem  21977  pjoc1i  22006  spansnm0i  22225  nonbooli  22226  5oalem1  22229  5oalem2  22230  5oalem4  22232  5oalem5  22233  5oalem7  22235  3oalem2  22238  3oalem3  22239  pjssmii  22256  mayete3i  22303  mayete3iOLD  22304  nmcopex  22605  nmcoplb  22606  lncnopbd  22613  nmcfnex  22629  nmcfnlb  22630  riesz4  22640  riesz1  22641  riesz2  22642  cnlnadjlem3  22645  cnlnadjlem5  22647  cnlnadjlem9  22651  cnlnadjeu  22654  rnbra  22683  pjimai  22752  pjclem4a  22774  pjclem4  22775  pj3lem1  22782  pj3si  22783  jpi  22846  sumdmdii  22991  sumdmdlem  22994  sumdmdlem2  22995  cdjreui  23008  cdj3lem1  23010  cnllyscon  23183  rellyscon  23189  cvmsss2  23212  cvmcov2  23213  cvmopnlem  23216  dfres3  23522  dfon2lem4  23546  predel  23587  wfrlem5  23664  frrlem5  23689  axfelem18  23767  ellimits  23861  dfom5b  23863  brapply  23887  brcap  23889  dfrdg4  23898  tfrqfree  23899  onsucconi  24286  onintopsscon  24289  onsucsuccmpi  24292  limsucncmpi  24294  onint1  24298  uninqs  24449  splint  24458  inposet  24689  isdir2  24703  ablocomgrp  24753  fprodadd  24763  isfldOLD  24837  fldi  24838  zintdom  24849  unint2t  24929  intcont  24954  indcomp  25000  topunfincomp  25001  bwt2  25003  intrr  25110  intvconlem1  25114  issubcata  25257  vtarsuelt  25306  eltintpar  25310  inttaror  25311  inttarcar  25312  carinttar  25313  elcarelcl  25317  pfsubkl  25458  pgapspf  25463  isconcl6a  25514  isconcl6ab  25515  isconcl7a  25516  pxysxy  25553  lppotoslem  25554  lppotos  25555  nbssntrs  25558  cnvresimaOLD  25637  finminlem  25642  comppfsc  25718  neibastop2lem  25720  neibastop2  25721  neifg  25731  tailfb  25737  inixp  25810  0totbnd  25908  sstotbnd3  25911  blbnd  25922  ssbnd  25923  heibor1lem  25944  heibor1  25945  heiborlem1  25946  heiborlem6  25951  heiborlem8  25953  heibor  25956  exidresid  25980  isfld2  26041  prtlem14  26153  elrfi  26180  elrfirn  26181  cmpfiiin  26183  mrefg2  26193  fz1eqin  26259  fnwe2lem2  26559  dfac11  26571  kelac1  26572  kelac2lem  26573  dfac21  26575  islmodfg  26578  islssfg2  26580  islssfgi  26581  filnm  26603  lnr2i  26731  lpirlnr  26732  hbtlem6  26744  hbt  26745  acsfn1p  26918  subrgacs  26919  sdrgacs  26920  cntzsdrg  26921  stoweidlem39  27199  stoweidlem44  27204  stoweidlem50  27210  stoweidlem57  27217  eldmressn  27373  afvres  27425  onfrALTlem2  27594  onfrALTlem2VD  27945  bnj521  28044  bnj1153  28104  bnj1172  28310  bnj1173  28311  bnj1174  28312  bnj1279  28327  lshpdisj  28456  lkrin  28633  ishlat1  28821  pmodlem1  29314  pmodlem2  29315  pclfinN  29368  pclcmpatN  29369  osumcllem4N  29427  pexmidlem1N  29438  dihmeetlem1N  30759  dihglblem5apreN  30760  dihmeetlem4preN  30775  dihmeetlem13N  30788  dochnel2  30861  lcdlss  31088  mapd1o  31117  mapdunirnN  31119  baerlem3lem2  31179  baerlem5alem2  31180  baerlem5blem2  31181  hdmaprnlem9N  31329
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 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
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 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-in 3160
  Copyright terms: Public domain W3C validator