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

Theorem elin 3333
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 2771 . 2  |-  ( A  e.  ( B  i^i  C )  ->  A  e.  _V )
2 elex 2771 . . 3  |-  ( A  e.  C  ->  A  e.  _V )
32adantl 454 . 2  |-  ( ( A  e.  B  /\  A  e.  C )  ->  A  e.  _V )
4 eleq1 2318 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
5 eleq1 2318 . . . 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 3134 . . 3  |-  ( B  i^i  C )  =  { x  |  ( x  e.  B  /\  x  e.  C ) }
86, 7elab2g 2891 . 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 2763    i^i cin 3126
This theorem is referenced by:  elin2  3334  elin3  3335  incom  3336  ineqri  3337  ineq1  3338  inass  3354  inss1  3364  ssin  3366  ssrin  3369  dfss4  3378  difin  3381  indi  3390  undi  3391  unineq  3394  indifdir  3400  difin2  3405  inrab2  3416  inelcm  3484  difin0ss  3495  inssdif0  3496  inundif  3507  uniin  3821  intun  3868  intpr  3869  elrint  3877  iunin2  3940  iinin2  3946  elriin  3948  disjor  3981  disjiun  3987  brin  4044  trin  4097  inex1  4129  inuni  4149  wefrc  4359  ordtri3or  4396  ordpwsuc  4578  inopab  4804  inxp  4806  dmin  4874  opelres  4948  intasym  5046  asymref  5047  dminss  5083  imainss  5084  ssrnres  5104  cnvresima  5149  dfco2a  5160  2elresin  5293  respreima  5588  isomin  5768  isoini  5769  offval  6019  tfrlem5  6364  erdisj  6675  mapval2  6765  ixpin  6809  boxriin  6826  disjen  6986  ssenen  7003  onfin2  7020  elfpw  7125  unifpw  7126  f1opwfi  7127  fissuni  7128  fipreima  7129  elfir  7137  fiin  7143  inf3lem2  7298  cantnfcl  7336  epfrs  7381  cp  7529  bnd2  7531  tskwe  7551  infpwfidom  7623  infpwfien  7657  dfac5lem1  7718  dfac5lem5  7722  dfac5  7723  kmlem3  7746  kmlem14  7757  kmlem15  7758  ackbij2lem1  7813  ackbij1lem3  7816  ackbij1lem4  7817  ackbij1lem6  7819  ackbij1lem11  7824  fin23lem24  7916  fin23lem26  7919  isfin1-3  7980  fpwwe2lem12  8231  fpwwe  8236  canthnumlem  8238  pwxpndom2  8255  ingru  8405  gruina  8408  grur1  8410  axgroth4  8422  grothprim  8424  ixxdisj  10638  icodisj  10728  fzdisj  10784  uzdisj  10823  fzouzdisj  10869  fz1isolem  11365  limsupgle  11917  ello12  11956  elo12  11967  lo1resb  12004  rlimresb  12005  o1resb  12006  lo1eq  12008  rlimeq  12009  fsumsplit  12178  sumsplit  12197  fsum2dlem  12199  explecnv  12286  bitsmod  12590  saddisjlem  12618  sadadd  12621  sadass  12625  smuval2  12636  smupval  12642  smueqlem  12644  smumul  12647  prmreclem5  12930  prmrec  12932  4sqlem12  12966  vdwmc  12988  strfv2d  13141  submre  13470  submrc  13493  isacs2  13518  acsfn  13524  coffth  13773  catcoppccl  13903  catcfuccl  13904  catcxpccl  13944  isdrs2  14036  fpwipodrs  14230  psss  14286  subgacs  14615  nsgacs  14616  resscntz  14770  sylow2a  14893  lsmmod  14947  lsmdisj  14953  lsmdisj2  14954  subgdisj1  14963  frgpnabllem1  15124  gsumzsplit  15169  dmdprdd  15200  dprdfeq0  15220  dprdres  15226  subgdmdprd  15232  dprdcntz2  15236  dprddisj2  15237  dprd2da  15240  dmdprdsplit2lem  15243  ablfacrp  15264  pgpfac1lem3a  15274  pgpfac1lem3  15275  pgpfaclem1  15279  isrhm  15464  subsubrg2  15535  lssacs  15687  lspdisj  15841  lspdisjb  15842  isassa  16019  aspval  16031  aspid  16033  aspval2  16049  mplind  16206  zlpirlem1  16404  zlpirlem3  16406  dfprime2  16410  ocvin  16537  unocv  16543  iunocv  16544  obselocv  16591  isbasis2g  16649  baspartn  16655  tgval2  16657  bastg  16667  tgcl  16670  ppttop  16707  epttop  16709  clsval2  16750  ssntr  16758  isopn3  16766  ntreq0  16777  isclo  16787  restbas  16852  restntr  16875  restlp  16876  cnpresti  16979  cnprest  16980  cnprest2  16981  lmss  16989  haust1  17043  nrmsep3  17046  isnrm2  17049  lmmo  17071  cmpcovf  17081  fincmp  17083  0cmp  17084  discmp  17088  cmpsublem  17089  cmpsub  17090  uncmp  17093  hauscmplem  17096  iscon2  17103  conclo  17104  dfcon2  17108  iunconlem  17116  uncon  17118  is1stc2  17131  1stcrest  17142  1stcelcls  17150  llyi  17163  nllyi  17164  llynlly  17166  subislly  17170  restnlly  17171  restlly  17172  islly2  17173  llyrest  17174  nllyrest  17175  llyidm  17177  nllyidm  17178  hausllycmp  17183  cldllycmp  17184  lly1stc  17185  dislly  17186  llycmpkgen2  17208  1stckgenlem  17211  txcnp  17277  txcnmpt  17281  txlly  17293  txnlly  17294  txtube  17297  txcmplem1  17298  txcmplem2  17299  hausdiag  17302  xkococnlem  17316  basqtop  17365  tgqtop  17366  kqcldsat  17387  ptcmpfi  17467  isfbas2  17493  isfil2  17514  infil  17521  fbasfip  17526  elfg  17529  filcon  17541  rnelfmlem  17610  rnelfm  17611  fmfnfmlem2  17613  fmfnfmlem4  17615  fmfnfm  17616  flimrest  17641  hauspwpwf1  17645  fclsrest  17682  alexsubALTlem2  17705  alexsubALTlem3  17706  alexsubALTlem4  17707  alexsubALT  17708  ptcmp  17715  istmd  17720  istgp  17723  tgpconcompss  17759  tsmssubm  17788  tsmssplit  17797  istrg  17809  istdrg  17811  istlm  17830  bldisj  17918  blin  17933  blin2  17938  blres  17940  lpbl  18012  metrest  18033  isngp  18081  isnlm  18149  isnmhm  18218  tgioo  18265  xrtgioo  18275  xrsmopn  18281  zdis  18285  icccmplem1  18290  icccmplem2  18291  reconnlem2  18295  xrge0tsms  18302  icoopnst  18400  iocopnst  18401  cnheibor  18416  cnllycmp  18417  bndth  18419  iscph  18569  cphsqrcl  18583  tchcph  18630  cfilfcls  18663  cmetcaulem  18677  cmetss  18703  isbn  18723  cldcss2  18769  hlhil  18770  ovolfcl  18789  ovollb2lem  18810  ovolctb  18812  ovolshftlem1  18831  ovolscalem1  18835  ovolicc1  18838  ovolicc2lem2  18840  ovolicc2lem4  18842  ovolicc2lem5  18843  ovolicc2  18844  shftmbl  18859  volfiniun  18867  ioombl1lem1  18878  ioorf  18891  ioorcl  18895  dyadf  18909  vitalilem2  18927  vitali  18931  mbfmax  18967  mbfimaopnlem  18973  mbfaddlem  18978  mbfadd  18979  mbfsub  18980  i1faddlem  19011  i1fmullem  19012  i1fres  19023  itg1climres  19032  mbfi1fseqlem4  19036  mbfmul  19044  itg2splitlem  19066  itg2split  19067  itgresr  19096  bddmulibl  19156  ellimc2  19190  ellimc3  19192  limcun  19208  dvreslem  19222  dvres2lem  19223  dvaddbr  19250  dvmulbr  19251  dvne0  19321  lhop1lem  19323  lhop  19326  dvcnvrelem2  19328  itgsubstlem  19358  ig1peu  19520  ig1pval3  19523  aaliou2  19683  aaliou2b  19684  tayl0  19704  pilem1  19790  rlimcnp2  20224  xrlimcnp  20226  fsumharmonic  20268  ppisval  20304  ppisval2  20305  ppinprm  20353  chtnprm  20355  prmorcht  20379  fsumvma2  20416  pclogsum  20417  vmasum  20418  chpchtsum  20421  chpub  20422  2sqlem7  20572  chebbnd1lem1  20581  rpvmasum2  20624  issubgo  20931  isexid2  20953  smgrpismgm  20960  smgrpisass  20961  issmgrp  20962  mndoissmgrp  20967  mndoisexid  20968  mndomgmid  20970  ismndo  20971  rngo1cl  21057  minvecolem1  21414  minvecolem4a  21417  minvecolem4b  21418  minvecolem4  21420  h2hcau  21520  axhcompl-zf  21539  hhcmpl  21740  hhcms  21743  ocin  21836  ocnel  21838  shuni  21840  shmodsi  21929  pjhthlem2  21932  omlsilem  21942  pjoc1i  21971  spansnm0i  22190  nonbooli  22191  5oalem1  22194  5oalem2  22195  5oalem4  22197  5oalem5  22198  5oalem7  22200  3oalem2  22203  3oalem3  22204  pjssmii  22221  mayete3i  22268  mayete3iOLD  22269  nmcopex  22570  nmcoplb  22571  lncnopbd  22578  nmcfnex  22594  nmcfnlb  22595  riesz4  22605  riesz1  22606  riesz2  22607  cnlnadjlem3  22610  cnlnadjlem5  22612  cnlnadjlem9  22616  cnlnadjeu  22619  rnbra  22648  pjimai  22717  pjclem4a  22739  pjclem4  22740  pj3lem1  22747  pj3si  22748  jpi  22811  sumdmdii  22956  sumdmdlem  22959  sumdmdlem2  22960  cdjreui  22973  cdj3lem1  22975  cnllyscon  23149  rellyscon  23155  cvmsss2  23178  cvmcov2  23179  cvmopnlem  23182  dfres3  23488  dfon2lem4  23512  predel  23553  wfrlem5  23630  frrlem5  23655  axfelem18  23733  ellimits  23827  dfom5b  23829  brapply  23853  brcap  23855  dfrdg4  23864  tfrqfree  23865  onsucconi  24252  onintopsscon  24255  onsucsuccmpi  24258  limsucncmpi  24260  onint1  24264  uninqs  24406  splint  24415  inposet  24646  isdir2  24660  ablocomgrp  24710  fprodadd  24720  isfldOLD  24794  fldi  24795  zintdom  24806  unint2t  24886  intcont  24911  indcomp  24957  topunfincomp  24958  bwt2  24960  intrr  25067  intvconlem1  25071  issubcata  25214  vtarsuelt  25263  eltintpar  25267  inttaror  25268  inttarcar  25269  carinttar  25270  elcarelcl  25274  pfsubkl  25415  pgapspf  25420  isconcl6a  25471  isconcl6ab  25472  isconcl7a  25473  pxysxy  25510  lppotoslem  25511  lppotos  25512  nbssntrs  25515  cnvresimaOLD  25594  finminlem  25599  comppfsc  25675  neibastop2lem  25677  neibastop2  25678  neifg  25688  tailfb  25694  inixp  25767  0totbnd  25865  sstotbnd3  25868  blbnd  25879  ssbnd  25880  heibor1lem  25901  heibor1  25902  heiborlem1  25903  heiborlem6  25908  heiborlem8  25910  heibor  25913  exidresid  25937  isfld2  25998  prtlem14  26110  elrfi  26137  elrfirn  26138  cmpfiiin  26140  mrefg2  26150  fz1eqin  26216  fnwe2lem2  26516  dfac11  26528  kelac1  26529  kelac2lem  26530  dfac21  26532  islmodfg  26535  islssfg2  26537  islssfgi  26538  filnm  26560  lnr2i  26688  lpirlnr  26689  hbtlem6  26701  hbt  26702  acsfn1p  26875  subrgacs  26876  sdrgacs  26877  cntzsdrg  26878  stoweidlem39  27157  stoweidlem44  27162  stoweidlem50  27168  stoweidlem57  27175  onfrALTlem2  27447  onfrALTlem2VD  27798  bnj521  27897  bnj1153  27957  bnj1172  28163  bnj1173  28164  bnj1174  28165  bnj1279  28180  lshpdisj  28427  lkrin  28604  ishlat1  28792  pmodlem1  29285  pmodlem2  29286  pclfinN  29339  pclcmpatN  29340  osumcllem4N  29398  pexmidlem1N  29409  dihmeetlem1N  30730  dihglblem5apreN  30731  dihmeetlem4preN  30746  dihmeetlem13N  30759  dochnel2  30832  lcdlss  31059  mapd1o  31088  mapdunirnN  31090  baerlem3lem2  31150  baerlem5alem2  31151  baerlem5blem2  31152  hdmaprnlem9N  31300
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 2239
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 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-in 3134
  Copyright terms: Public domain W3C validator