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

Theorem elin 3360
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 2798 . 2  |-  ( A  e.  ( B  i^i  C )  ->  A  e.  _V )
2 elex 2798 . . 3  |-  ( A  e.  C  ->  A  e.  _V )
32adantl 452 . 2  |-  ( ( A  e.  B  /\  A  e.  C )  ->  A  e.  _V )
4 eleq1 2345 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
5 eleq1 2345 . . . 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 3161 . . 3  |-  ( B  i^i  C )  =  { x  |  ( x  e.  B  /\  x  e.  C ) }
86, 7elab2g 2918 . 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 1625    e. wcel 1686   _Vcvv 2790    i^i cin 3153
This theorem is referenced by:  elin2  3361  elin3  3362  incom  3363  ineqri  3364  ineq1  3365  inass  3381  inss1  3391  ssin  3393  ssrin  3396  dfss4  3405  difin  3408  indi  3417  undi  3418  unineq  3421  indifdir  3427  difin2  3432  inrab2  3443  inelcm  3511  difin0ss  3522  inssdif0  3523  inundif  3534  uniin  3849  intun  3896  intpr  3897  elrint  3905  iunin2  3968  iinin2  3974  elriin  3976  disjor  4009  disjiun  4015  brin  4072  trin  4125  inex1  4157  inuni  4175  wefrc  4389  ordtri3or  4426  ordpwsuc  4608  inopab  4818  inxp  4820  dmin  4888  opelres  4962  intasym  5060  asymref  5061  dminss  5097  imainss  5098  ssrnres  5118  cnvresima  5164  dfco2a  5175  2elresin  5357  respreima  5656  isomin  5836  isoini  5837  offval  6087  tfrlem5  6398  erdisj  6709  mapval2  6799  ixpin  6843  boxriin  6860  disjen  7020  ssenen  7037  onfin2  7054  elfpw  7159  unifpw  7160  f1opwfi  7161  fissuni  7162  fipreima  7163  elfir  7171  fiin  7177  inf3lem2  7332  cantnfcl  7370  epfrs  7415  cp  7563  bnd2  7565  tskwe  7585  infpwfidom  7657  infpwfien  7691  dfac5lem1  7752  dfac5lem5  7756  dfac5  7757  kmlem3  7780  kmlem14  7791  kmlem15  7792  ackbij2lem1  7847  ackbij1lem3  7850  ackbij1lem4  7851  ackbij1lem6  7853  ackbij1lem11  7858  fin23lem24  7950  fin23lem26  7953  isfin1-3  8014  fpwwe2lem12  8265  fpwwe  8270  canthnumlem  8272  pwxpndom2  8289  ingru  8439  gruina  8442  grur1  8444  axgroth4  8456  grothprim  8458  ixxdisj  10673  icodisj  10763  fzdisj  10819  uzdisj  10858  fzouzdisj  10904  fz1isolem  11401  limsupgle  11953  ello12  11992  elo12  12003  lo1resb  12040  rlimresb  12041  o1resb  12042  lo1eq  12044  rlimeq  12045  fsumsplit  12214  sumsplit  12233  fsum2dlem  12235  explecnv  12325  bitsmod  12629  saddisjlem  12657  sadadd  12660  sadass  12664  smuval2  12675  smupval  12681  smueqlem  12683  smumul  12686  prmreclem5  12969  prmrec  12971  4sqlem12  13005  vdwmc  13027  strfv2d  13180  submre  13509  submrc  13532  isacs2  13557  acsfn  13563  coffth  13812  catcoppccl  13942  catcfuccl  13943  catcxpccl  13983  isdrs2  14075  fpwipodrs  14269  psss  14325  subgacs  14654  nsgacs  14655  resscntz  14809  sylow2a  14932  lsmmod  14986  lsmdisj  14992  lsmdisj2  14993  subgdisj1  15002  frgpnabllem1  15163  gsumzsplit  15208  dmdprdd  15239  dprdfeq0  15259  dprdres  15265  subgdmdprd  15271  dprdcntz2  15275  dprddisj2  15276  dprd2da  15279  dmdprdsplit2lem  15282  ablfacrp  15303  pgpfac1lem3a  15313  pgpfac1lem3  15314  pgpfaclem1  15318  isrhm  15503  subsubrg2  15574  lssacs  15726  lspdisj  15880  lspdisjb  15881  isassa  16058  aspval  16070  aspid  16072  aspval2  16088  mplind  16245  zlpirlem1  16443  zlpirlem3  16445  dfprm2  16449  ocvin  16576  unocv  16582  iunocv  16583  obselocv  16630  isbasis2g  16688  baspartn  16694  tgval2  16696  bastg  16706  tgcl  16709  ppttop  16746  epttop  16748  clsval2  16789  ssntr  16797  isopn3  16805  ntreq0  16816  isclo  16826  restbas  16891  restntr  16914  restlp  16915  cnpresti  17018  cnprest  17019  cnprest2  17020  lmss  17028  haust1  17082  nrmsep3  17085  isnrm2  17088  lmmo  17110  cmpcovf  17120  fincmp  17122  0cmp  17123  discmp  17127  cmpsublem  17128  cmpsub  17129  uncmp  17132  hauscmplem  17135  iscon2  17142  conclo  17143  dfcon2  17147  iunconlem  17155  uncon  17157  is1stc2  17170  1stcrest  17181  1stcelcls  17189  llyi  17202  nllyi  17203  llynlly  17205  subislly  17209  restnlly  17210  restlly  17211  islly2  17212  llyrest  17213  nllyrest  17214  llyidm  17216  nllyidm  17217  hausllycmp  17222  cldllycmp  17223  lly1stc  17224  dislly  17225  llycmpkgen2  17247  1stckgenlem  17250  txcnp  17316  txcnmpt  17320  txlly  17332  txnlly  17333  txtube  17336  txcmplem1  17337  txcmplem2  17338  hausdiag  17341  xkococnlem  17355  basqtop  17404  tgqtop  17405  kqcldsat  17426  ptcmpfi  17506  isfbas2  17532  isfil2  17553  infil  17560  fbasfip  17565  elfg  17568  filcon  17580  rnelfmlem  17649  rnelfm  17650  fmfnfmlem2  17652  fmfnfmlem4  17654  fmfnfm  17655  flimrest  17680  hauspwpwf1  17684  fclsrest  17721  alexsubALTlem2  17744  alexsubALTlem3  17745  alexsubALTlem4  17746  alexsubALT  17747  ptcmp  17754  istmd  17759  istgp  17762  tgpconcompss  17798  tsmssubm  17827  tsmssplit  17836  istrg  17848  istdrg  17850  istlm  17869  bldisj  17957  blin  17972  blin2  17977  blres  17979  lpbl  18051  metrest  18072  isngp  18120  isnlm  18188  isnmhm  18257  tgioo  18304  xrtgioo  18314  xrsmopn  18320  zdis  18324  icccmplem1  18329  icccmplem2  18330  reconnlem2  18334  xrge0tsms  18341  icoopnst  18439  iocopnst  18440  cnheibor  18455  cnllycmp  18456  bndth  18458  iscph  18608  cphsqrcl  18622  tchcph  18669  cfilfcls  18702  cmetcaulem  18716  cmetss  18742  isbn  18762  cldcss2  18808  hlhil  18809  ovolfcl  18828  ovollb2lem  18849  ovolctb  18851  ovolshftlem1  18870  ovolscalem1  18874  ovolicc1  18877  ovolicc2lem2  18879  ovolicc2lem4  18881  ovolicc2lem5  18882  ovolicc2  18883  shftmbl  18898  volfiniun  18906  ioombl1lem1  18917  ioorf  18930  ioorcl  18934  dyadf  18948  vitalilem2  18966  vitali  18970  mbfmax  19006  mbfimaopnlem  19012  mbfaddlem  19017  mbfadd  19018  mbfsub  19019  i1faddlem  19050  i1fmullem  19051  i1fres  19062  itg1climres  19071  mbfi1fseqlem4  19075  mbfmul  19083  itg2splitlem  19105  itg2split  19106  itgresr  19135  bddmulibl  19195  ellimc2  19229  ellimc3  19231  limcun  19247  dvreslem  19261  dvres2lem  19262  dvaddbr  19289  dvmulbr  19290  dvne0  19360  lhop1lem  19362  lhop  19365  dvcnvrelem2  19367  itgsubstlem  19397  ig1peu  19559  ig1pval3  19562  aaliou2  19722  aaliou2b  19723  tayl0  19743  pilem1  19829  rlimcnp2  20263  xrlimcnp  20265  fsumharmonic  20307  ppisval  20343  ppisval2  20344  ppinprm  20392  chtnprm  20394  prmorcht  20418  fsumvma2  20455  pclogsum  20456  vmasum  20457  chpchtsum  20460  chpub  20461  2sqlem7  20611  chebbnd1lem1  20620  rpvmasum2  20663  issubgo  20972  isexid2  20994  smgrpismgm  21001  smgrpisass  21002  issmgrp  21003  mndoissmgrp  21008  mndoisexid  21009  mndomgmid  21011  ismndo  21012  rngo1cl  21098  minvecolem1  21455  minvecolem4a  21458  minvecolem4b  21459  minvecolem4  21461  h2hcau  21561  axhcompl-zf  21580  hhcmpl  21781  hhcms  21784  ocin  21877  ocnel  21879  shuni  21881  shmodsi  21970  pjhthlem2  21973  omlsilem  21983  pjoc1i  22012  spansnm0i  22231  nonbooli  22232  5oalem1  22235  5oalem2  22236  5oalem4  22238  5oalem5  22239  5oalem7  22241  3oalem2  22244  3oalem3  22245  pjssmii  22262  mayete3i  22309  mayete3iOLD  22310  nmcopex  22611  nmcoplb  22612  lncnopbd  22619  nmcfnex  22635  nmcfnlb  22636  riesz4  22646  riesz1  22647  riesz2  22648  cnlnadjlem3  22651  cnlnadjlem5  22653  cnlnadjlem9  22657  cnlnadjeu  22660  rnbra  22689  pjimai  22758  pjclem4a  22780  pjclem4  22781  pj3lem1  22788  pj3si  22789  jpi  22852  sumdmdii  22997  sumdmdlem  23000  sumdmdlem2  23001  cdjreui  23014  cdj3lem1  23016  iocinioc2  23274  ssnnssfz  23279  cnre2csqima  23297  disjorf  23358  pnfneige0  23376  lmxrge0  23377  xrge0tsmsd  23384  esum0  23430  esumcst  23438  esumpcvgval  23448  esumcvg  23456  sigainb  23499  measvuni  23544  indf1ofs  23611  cnllyscon  23778  rellyscon  23784  cvmsss2  23807  cvmcov2  23808  cvmopnlem  23811  dfres3  24118  dfon2lem4  24144  predel  24185  wfrlem5  24262  frrlem5  24287  ellimits  24452  dfom5b  24454  brapply  24479  brcap  24481  dfrdg4  24490  tfrqfree  24491  onsucconi  24878  onintopsscon  24881  onsucsuccmpi  24884  limsucncmpi  24886  onint1  24890  uninqs  25050  splint  25059  inposet  25289  isdir2  25303  ablocomgrp  25353  fprodadd  25363  isfldOLD  25437  fldi  25438  zintdom  25449  unint2t  25529  intcont  25554  indcomp  25600  topunfincomp  25601  bwt2  25603  intrr  25710  intvconlem1  25714  issubcata  25857  vtarsuelt  25906  eltintpar  25910  inttaror  25911  inttarcar  25912  carinttar  25913  elcarelcl  25917  pfsubkl  26058  pgapspf  26063  isconcl6a  26114  isconcl6ab  26115  isconcl7a  26116  pxysxy  26153  lppotoslem  26154  lppotos  26155  nbssntrs  26158  cnvresimaOLD  26237  finminlem  26242  comppfsc  26318  neibastop2lem  26320  neibastop2  26321  neifg  26331  tailfb  26337  inixp  26410  0totbnd  26508  sstotbnd3  26511  blbnd  26522  ssbnd  26523  heibor1lem  26544  heibor1  26545  heiborlem1  26546  heiborlem6  26551  heiborlem8  26553  heibor  26556  exidresid  26580  isfld2  26641  prtlem14  26753  elrfi  26780  elrfirn  26781  cmpfiiin  26783  mrefg2  26793  fz1eqin  26859  fnwe2lem2  27159  dfac11  27171  kelac1  27172  kelac2lem  27173  dfac21  27175  islmodfg  27178  islssfg2  27180  islssfgi  27181  filnm  27203  lnr2i  27331  lpirlnr  27332  hbtlem6  27344  hbt  27345  acsfn1p  27518  subrgacs  27519  sdrgacs  27520  cntzsdrg  27521  stoweidlem39  27799  stoweidlem44  27804  stoweidlem50  27810  stoweidlem57  27817  eldmressn  27993  afvres  28045  onfrALTlem2  28367  onfrALTlem2VD  28738  bnj521  28838  bnj1153  28898  bnj1172  29104  bnj1173  29105  bnj1174  29106  bnj1279  29121  lshpdisj  29250  lkrin  29427  ishlat1  29615  pmodlem1  30108  pmodlem2  30109  pclfinN  30162  pclcmpatN  30163  osumcllem4N  30221  pexmidlem1N  30232  dihmeetlem1N  31553  dihglblem5apreN  31554  dihmeetlem4preN  31569  dihmeetlem13N  31582  dochnel2  31655  lcdlss  31882  mapd1o  31911  mapdunirnN  31913  baerlem3lem2  31973  baerlem5alem2  31974  baerlem5blem2  31975  hdmaprnlem9N  32123
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-in 3161
  Copyright terms: Public domain W3C validator