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

Theorem elin 3300
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 2748 . 2  |-  ( A  e.  ( B  i^i  C )  ->  A  e.  _V )
2 elex 2748 . . 3  |-  ( A  e.  C  ->  A  e.  _V )
32adantl 454 . 2  |-  ( ( A  e.  B  /\  A  e.  C )  ->  A  e.  _V )
4 eleq1 2316 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
5 eleq1 2316 . . . 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 3101 . . 3  |-  ( B  i^i  C )  =  { x  |  ( x  e.  B  /\  x  e.  C ) }
86, 7elab2g 2867 . 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 2740    i^i cin 3093
This theorem is referenced by:  elin2  3301  elin3  3302  incom  3303  ineqri  3304  ineq1  3305  inass  3321  inss1  3331  ssin  3333  ssrin  3336  dfss4  3345  difin  3348  indi  3357  undi  3358  unineq  3361  indifdir  3367  difin2  3372  inrab2  3383  inelcm  3451  difin0ss  3462  inssdif0  3463  inundif  3474  uniin  3788  intun  3835  intpr  3836  elrint  3844  iunin2  3907  iinin2  3913  elriin  3915  disjor  3947  disjiun  3953  brin  4010  trin  4063  inex1  4095  inuni  4115  wefrc  4324  ordtri3or  4361  ordpwsuc  4543  inopab  4769  inxp  4771  dmin  4839  opelres  4913  intasym  5011  asymref  5012  dminss  5048  imainss  5049  ssrnres  5069  cnvresima  5114  dfco2a  5125  2elresin  5258  respreima  5553  isomin  5733  isoini  5734  offval  5984  tfrlem5  6329  erdisj  6640  mapval2  6730  ixpin  6774  boxriin  6791  disjen  6951  ssenen  6968  onfin2  6985  elfpw  7090  unifpw  7091  f1opwfi  7092  fissuni  7093  fipreima  7094  elfir  7102  fiin  7108  inf3lem2  7263  cantnfcl  7301  epfrs  7346  cp  7494  bnd2  7496  tskwe  7516  infpwfidom  7588  infpwfien  7622  dfac5lem1  7683  dfac5lem5  7687  dfac5  7688  kmlem3  7711  kmlem14  7722  kmlem15  7723  ackbij2lem1  7778  ackbij1lem3  7781  ackbij1lem4  7782  ackbij1lem6  7784  ackbij1lem11  7789  fin23lem24  7881  fin23lem26  7884  isfin1-3  7945  fpwwe2lem12  8196  fpwwe  8201  canthnumlem  8203  pwxpndom2  8220  ingru  8370  gruina  8373  grur1  8375  axgroth4  8387  grothprim  8389  ixxdisj  10602  icodisj  10692  fzdisj  10748  uzdisj  10787  fzouzdisj  10833  fz1isolem  11329  limsupgle  11881  ello12  11920  elo12  11931  lo1resb  11968  rlimresb  11969  o1resb  11970  lo1eq  11972  rlimeq  11973  fsumsplit  12142  sumsplit  12161  fsum2dlem  12163  explecnv  12250  bitsmod  12554  saddisjlem  12582  sadadd  12585  sadass  12589  smuval2  12600  smupval  12606  smueqlem  12608  smumul  12611  prmreclem5  12894  prmrec  12896  4sqlem12  12930  vdwmc  12952  strfv2d  13105  submre  13434  submrc  13457  isacs2  13482  acsfn  13488  coffth  13737  catcoppccl  13867  catcfuccl  13868  catcxpccl  13908  isdrs2  14000  fpwipodrs  14194  psss  14250  subgacs  14579  nsgacs  14580  resscntz  14734  sylow2a  14857  lsmmod  14911  lsmdisj  14917  lsmdisj2  14918  subgdisj1  14927  frgpnabllem1  15088  gsumzsplit  15133  dmdprdd  15164  dprdfeq0  15184  dprdres  15190  subgdmdprd  15196  dprdcntz2  15200  dprddisj2  15201  dprd2da  15204  dmdprdsplit2lem  15207  ablfacrp  15228  pgpfac1lem3a  15238  pgpfac1lem3  15239  pgpfaclem1  15243  isrhm  15428  subsubrg2  15499  lssacs  15651  lspdisj  15805  lspdisjb  15806  isassa  15983  aspval  15995  aspid  15997  aspval2  16013  mplind  16170  zlpirlem1  16368  zlpirlem3  16370  dfprime2  16374  ocvin  16501  unocv  16507  iunocv  16508  obselocv  16555  isbasis2g  16613  baspartn  16619  tgval2  16621  bastg  16631  tgcl  16634  ppttop  16671  epttop  16673  clsval2  16714  ssntr  16722  isopn3  16730  ntreq0  16741  isclo  16751  restbas  16816  restntr  16839  restlp  16840  cnpresti  16943  cnprest  16944  cnprest2  16945  lmss  16953  haust1  17007  nrmsep3  17010  isnrm2  17013  lmmo  17035  cmpcovf  17045  fincmp  17047  0cmp  17048  discmp  17052  cmpsublem  17053  cmpsub  17054  uncmp  17057  hauscmplem  17060  iscon2  17067  conclo  17068  dfcon2  17072  iunconlem  17080  uncon  17082  is1stc2  17095  1stcrest  17106  1stcelcls  17114  llyi  17127  nllyi  17128  llynlly  17130  subislly  17134  restnlly  17135  restlly  17136  islly2  17137  llyrest  17138  nllyrest  17139  llyidm  17141  nllyidm  17142  hausllycmp  17147  cldllycmp  17148  lly1stc  17149  dislly  17150  llycmpkgen2  17172  1stckgenlem  17175  txcnp  17241  txcnmpt  17245  txlly  17257  txnlly  17258  txtube  17261  txcmplem1  17262  txcmplem2  17263  hausdiag  17266  xkococnlem  17280  basqtop  17329  tgqtop  17330  kqcldsat  17351  ptcmpfi  17431  isfbas2  17457  isfil2  17478  infil  17485  fbasfip  17490  elfg  17493  filcon  17505  rnelfmlem  17574  rnelfm  17575  fmfnfmlem2  17577  fmfnfmlem4  17579  fmfnfm  17580  flimrest  17605  hauspwpwf1  17609  fclsrest  17646  alexsubALTlem2  17669  alexsubALTlem3  17670  alexsubALTlem4  17671  alexsubALT  17672  ptcmp  17679  istmd  17684  istgp  17687  tgpconcompss  17723  tsmssubm  17752  tsmssplit  17761  istrg  17773  istdrg  17775  istlm  17794  bldisj  17882  blin  17897  blin2  17902  blres  17904  lpbl  17976  metrest  17997  isngp  18045  isnlm  18113  isnmhm  18182  tgioo  18229  xrtgioo  18239  xrsmopn  18245  zdis  18249  icccmplem1  18254  icccmplem2  18255  reconnlem2  18259  xrge0tsms  18266  icoopnst  18364  iocopnst  18365  cnheibor  18380  cnllycmp  18381  bndth  18383  iscph  18533  cphsqrcl  18547  tchcph  18594  cfilfcls  18627  cmetcaulem  18641  cmetss  18667  isbn  18687  cldcss2  18733  hlhil  18734  ovolfcl  18753  ovollb2lem  18774  ovolctb  18776  ovolshftlem1  18795  ovolscalem1  18799  ovolicc1  18802  ovolicc2lem2  18804  ovolicc2lem4  18806  ovolicc2lem5  18807  ovolicc2  18808  shftmbl  18823  volfiniun  18831  ioombl1lem1  18842  ioorf  18855  ioorcl  18859  dyadf  18873  vitalilem2  18891  vitali  18895  mbfmax  18931  mbfimaopnlem  18937  mbfaddlem  18942  mbfadd  18943  mbfsub  18944  i1faddlem  18975  i1fmullem  18976  i1fres  18987  itg1climres  18996  mbfi1fseqlem4  19000  mbfmul  19008  itg2splitlem  19030  itg2split  19031  itgresr  19060  bddmulibl  19120  ellimc2  19154  ellimc3  19156  limcun  19172  dvreslem  19186  dvres2lem  19187  dvaddbr  19214  dvmulbr  19215  dvne0  19285  lhop1lem  19287  lhop  19290  dvcnvrelem2  19292  itgsubstlem  19322  ig1peu  19484  ig1pval3  19487  aaliou2  19647  aaliou2b  19648  tayl0  19668  pilem1  19754  rlimcnp2  20188  xrlimcnp  20190  fsumharmonic  20232  ppisval  20268  ppisval2  20269  ppinprm  20317  chtnprm  20319  prmorcht  20343  fsumvma2  20380  pclogsum  20381  vmasum  20382  chpchtsum  20385  chpub  20386  2sqlem7  20536  chebbnd1lem1  20545  rpvmasum2  20588  issubgo  20895  isexid2  20917  smgrpismgm  20924  smgrpisass  20925  issmgrp  20926  mndoissmgrp  20931  mndoisexid  20932  mndomgmid  20934  ismndo  20935  rngo1cl  21021  minvecolem1  21378  minvecolem4a  21381  minvecolem4b  21382  minvecolem4  21384  h2hcau  21484  axhcompl-zf  21503  hhcmpl  21704  hhcms  21707  ocin  21800  ocnel  21802  shuni  21804  shmodsi  21893  pjhthlem2  21896  omlsilem  21906  pjoc1i  21935  spansnm0i  22172  nonbooli  22173  5oalem1  22176  5oalem2  22177  5oalem4  22179  5oalem5  22180  5oalem7  22182  3oalem2  22185  3oalem3  22186  pjssmii  22203  mayete3i  22250  mayete3iOLD  22251  nmcopex  22534  nmcoplb  22535  lncnopbd  22542  nmcfnex  22558  nmcfnlb  22559  riesz4  22569  riesz1  22570  riesz2  22571  cnlnadjlem3  22574  cnlnadjlem5  22576  cnlnadjlem9  22580  cnlnadjeu  22583  rnbra  22612  pjimai  22681  pjclem4a  22703  pjclem4  22704  pj3lem1  22711  pj3si  22712  jpi  22775  sumdmdii  22920  sumdmdlem  22923  sumdmdlem2  22924  cdjreui  22937  cdj3lem1  22939  cnllyscon  23113  rellyscon  23119  cvmsss2  23142  cvmcov2  23143  cvmopnlem  23146  dfres3  23452  dfon2lem4  23476  predel  23517  wfrlem5  23594  frrlem5  23619  axfelem18  23697  ellimits  23791  dfom5b  23793  brapply  23817  brcap  23819  dfrdg4  23828  tfrqfree  23829  onsucconi  24216  onintopsscon  24219  onsucsuccmpi  24222  limsucncmpi  24224  onint1  24228  uninqs  24370  splint  24379  inposet  24610  isdir2  24624  ablocomgrp  24674  fprodadd  24684  isfldOLD  24758  fldi  24759  zintdom  24770  unint2t  24850  intcont  24875  indcomp  24921  topunfincomp  24922  bwt2  24924  intrr  25031  intvconlem1  25035  issubcata  25178  vtarsuelt  25227  eltintpar  25231  inttaror  25232  inttarcar  25233  carinttar  25234  elcarelcl  25238  pfsubkl  25379  pgapspf  25384  isconcl6a  25435  isconcl6ab  25436  isconcl7a  25437  pxysxy  25474  lppotoslem  25475  lppotos  25476  nbssntrs  25479  cnvresimaOLD  25558  finminlem  25563  comppfsc  25639  neibastop2lem  25641  neibastop2  25642  neifg  25652  tailfb  25658  inixp  25731  0totbnd  25829  sstotbnd3  25832  blbnd  25843  ssbnd  25844  heibor1lem  25865  heibor1  25866  heiborlem1  25867  heiborlem6  25872  heiborlem8  25874  heibor  25877  exidresid  25901  isfld2  25962  prtlem14  26074  elrfi  26101  elrfirn  26102  cmpfiiin  26104  mrefg2  26114  fz1eqin  26180  fnwe2lem2  26480  dfac11  26492  kelac1  26493  kelac2lem  26494  dfac21  26496  islmodfg  26499  islssfg2  26501  islssfgi  26502  filnm  26524  lnr2i  26652  lpirlnr  26653  hbtlem6  26665  hbt  26666  acsfn1p  26839  subrgacs  26840  sdrgacs  26841  cntzsdrg  26842  stoweidlem39  27088  stoweidlem44  27093  stoweidlem50  27099  stoweidlem57  27106  onfrALTlem2  27327  onfrALTlem2VD  27678  bnj521  27777  bnj1153  27837  bnj1172  28043  bnj1173  28044  bnj1174  28045  bnj1279  28060  lshpdisj  28307  lkrin  28484  ishlat1  28672  pmodlem1  29165  pmodlem2  29166  pclfinN  29219  pclcmpatN  29220  osumcllem4N  29278  pexmidlem1N  29289  dihmeetlem1N  30610  dihglblem5apreN  30611  dihmeetlem4preN  30626  dihmeetlem13N  30639  dochnel2  30712  lcdlss  30939  mapd1o  30968  mapdunirnN  30970  baerlem3lem2  31030  baerlem5alem2  31031  baerlem5blem2  31032  hdmaprnlem9N  31180
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 2237
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 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2742  df-in 3101
  Copyright terms: Public domain W3C validator