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

Theorem elin 3466
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 2900 . 2  |-  ( A  e.  ( B  i^i  C )  ->  A  e.  _V )
2 elex 2900 . . 3  |-  ( A  e.  C  ->  A  e.  _V )
32adantl 453 . 2  |-  ( ( A  e.  B  /\  A  e.  C )  ->  A  e.  _V )
4 eleq1 2440 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
5 eleq1 2440 . . . 4  |-  ( x  =  A  ->  (
x  e.  C  <->  A  e.  C ) )
64, 5anbi12d 692 . . 3  |-  ( x  =  A  ->  (
( x  e.  B  /\  x  e.  C
)  <->  ( A  e.  B  /\  A  e.  C ) ) )
7 df-in 3263 . . 3  |-  ( B  i^i  C )  =  { x  |  ( x  e.  B  /\  x  e.  C ) }
86, 7elab2g 3020 . 2  |-  ( A  e.  _V  ->  ( A  e.  ( B  i^i  C )  <->  ( A  e.  B  /\  A  e.  C ) ) )
91, 3, 8pm5.21nii 343 1  |-  ( A  e.  ( B  i^i  C )  <->  ( A  e.  B  /\  A  e.  C ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1717   _Vcvv 2892    i^i cin 3255
This theorem is referenced by:  elin2  3467  elin3  3468  incom  3469  ineqri  3470  ineq1  3471  inass  3487  inss1  3497  ssin  3499  ssrin  3502  dfss4  3511  difin  3514  indi  3523  undi  3524  unineq  3527  indifdir  3533  difin2  3539  inrab2  3550  inelcm  3618  difin0ss  3630  inssdif0  3631  inundif  3642  uniin  3970  intun  4017  intpr  4018  elrint  4026  iunin2  4089  iinin2  4095  elriin  4097  disjor  4130  disjiun  4136  brin  4193  trin  4246  inex1  4278  inuni  4296  wefrc  4510  ordtri3or  4547  ordpwsuc  4728  inopab  4938  inxp  4940  dmin  5010  opelres  5084  intasym  5182  asymref  5183  dminss  5219  imainss  5220  inimasn  5222  ssrnres  5242  cnvresima  5292  dfco2a  5303  2elresin  5489  respreima  5791  isomin  5989  isoini  5990  offval  6244  tfrlem5  6570  erdisj  6881  uniinqs  6913  mapval2  6972  ixpin  7016  boxriin  7033  disjen  7193  ssenen  7210  onfin2  7227  elfpw  7336  unifpw  7337  f1opwfi  7338  fissuni  7339  fipreima  7340  elfir  7348  inelfi  7351  fiin  7355  inf3lem2  7510  cantnfcl  7548  epfrs  7593  cp  7741  bnd2  7743  tskwe  7763  infpwfidom  7835  infpwfien  7869  dfac5lem1  7930  dfac5lem5  7934  dfac5  7935  kmlem3  7958  kmlem14  7969  kmlem15  7970  ackbij2lem1  8025  ackbij1lem3  8028  ackbij1lem4  8029  ackbij1lem6  8031  ackbij1lem11  8036  fin23lem24  8128  fin23lem26  8131  isfin1-3  8192  fpwwe2lem12  8442  fpwwe  8447  canthnumlem  8449  pwxpndom2  8466  ingru  8616  gruina  8619  grur1  8621  axgroth4  8633  grothprim  8635  ixxdisj  10856  icodisj  10947  fzdisj  11003  uzdisj  11042  fzouzdisj  11092  fz1isolem  11630  limsupgle  12191  ello12  12230  elo12  12241  lo1resb  12278  rlimresb  12279  o1resb  12280  lo1eq  12282  rlimeq  12283  fsumsplit  12453  sumsplit  12472  fsum2dlem  12474  explecnv  12564  bitsmod  12868  saddisjlem  12896  sadadd  12899  sadass  12903  smuval2  12914  smupval  12920  smueqlem  12922  smumul  12925  prmreclem5  13208  prmrec  13210  4sqlem12  13244  vdwmc  13266  strfv2d  13419  submre  13750  submrc  13773  isacs2  13798  acsfn  13804  coffth  14053  catcoppccl  14183  catcfuccl  14184  catcxpccl  14224  isdrs2  14316  fpwipodrs  14510  psss  14566  subgacs  14895  nsgacs  14896  resscntz  15050  sylow2a  15173  lsmmod  15227  lsmdisj  15233  lsmdisj2  15234  subgdisj1  15243  frgpnabllem1  15404  gsumzsplit  15449  dmdprdd  15480  dprdfeq0  15500  dprdres  15506  subgdmdprd  15512  dprdcntz2  15516  dprddisj2  15517  dprd2da  15520  dmdprdsplit2lem  15523  ablfacrp  15544  pgpfac1lem3a  15554  pgpfac1lem3  15555  pgpfaclem1  15559  isrhm  15744  subsubrg2  15815  lssacs  15963  lspdisj  16117  lspdisjb  16118  isassa  16295  aspval  16307  aspid  16309  aspval2  16325  mplind  16482  zlpirlem1  16684  zlpirlem3  16686  dfprm2  16690  ocvin  16817  unocv  16823  iunocv  16824  obselocv  16871  isbasis2g  16929  baspartn  16935  tgval2  16937  bastg  16947  tgcl  16950  ppttop  16987  epttop  16989  clsval2  17030  ssntr  17038  isopn3  17046  ntreq0  17057  isclo  17067  restbas  17137  restntr  17161  restlp  17162  cnpresti  17267  cnprest  17268  cnprest2  17269  lmss  17277  haust1  17331  nrmsep3  17334  isnrm2  17337  lmmo  17359  cmpcovf  17369  fincmp  17371  0cmp  17372  discmp  17376  cmpsublem  17377  cmpsub  17378  uncmp  17381  hauscmplem  17384  iscon2  17391  conclo  17392  dfcon2  17396  iunconlem  17404  uncon  17406  is1stc2  17419  1stcrest  17430  1stcelcls  17438  llyi  17451  nllyi  17452  llynlly  17454  subislly  17458  restnlly  17459  restlly  17460  islly2  17461  llyrest  17462  nllyrest  17463  llyidm  17465  nllyidm  17466  hausllycmp  17471  cldllycmp  17472  lly1stc  17473  dislly  17474  llycmpkgen2  17496  1stckgenlem  17499  txcnp  17566  txcnmpt  17570  txlly  17582  txnlly  17583  txtube  17586  txcmplem1  17587  txcmplem2  17588  hausdiag  17591  xkococnlem  17605  basqtop  17657  tgqtop  17658  kqcldsat  17679  ptcmpfi  17759  isfbas2  17781  isfil2  17802  infil  17809  fbasfip  17814  elfg  17817  filcon  17829  rnelfmlem  17898  rnelfm  17899  fmfnfmlem2  17901  fmfnfmlem4  17903  fmfnfm  17904  flimrest  17929  hauspwpwf1  17933  fclsrest  17970  alexsubALTlem2  17993  alexsubALTlem3  17994  alexsubALTlem4  17995  alexsubALT  17996  ptcmp  18003  istmd  18018  istgp  18021  tgpconcompss  18057  tsmssubm  18086  tsmssplit  18095  istrg  18107  istdrg  18109  istlm  18128  ustfilxp  18156  utoptop  18178  utop3cls  18195  bldisj  18322  blin  18337  blin2  18342  blres  18344  lpbl  18416  metrest  18437  restmetu  18482  isngp  18507  isnlm  18575  isnmhm  18644  tgioo  18691  xrtgioo  18701  xrsmopn  18707  zdis  18711  icccmplem1  18717  icccmplem2  18718  reconnlem2  18722  xrge0tsms  18729  icoopnst  18828  iocopnst  18829  cnheibor  18844  cnllycmp  18845  bndth  18847  iscph  18997  cphsqrcl  19011  tchcph  19058  cfilfcls  19091  cmetcaulem  19105  cmetss  19131  isbn  19153  cldcss2  19203  hlhil  19204  ovolfcl  19223  ovollb2lem  19244  ovolctb  19246  ovolshftlem1  19265  ovolscalem1  19269  ovolicc1  19272  ovolicc2lem2  19274  ovolicc2lem4  19276  ovolicc2lem5  19277  ovolicc2  19278  shftmbl  19293  volfiniun  19301  ioombl1lem1  19312  ioorf  19325  ioorcl  19329  dyadf  19343  vitalilem2  19361  vitali  19365  mbfmax  19401  mbfimaopnlem  19407  mbfaddlem  19412  mbfadd  19413  mbfsub  19414  i1faddlem  19445  i1fmullem  19446  i1fres  19457  itg1climres  19466  mbfi1fseqlem4  19470  mbfmul  19478  itg2splitlem  19500  itg2split  19501  itgresr  19530  bddmulibl  19590  ellimc2  19624  ellimc3  19626  limcun  19642  dvreslem  19656  dvres2lem  19657  dvaddbr  19684  dvmulbr  19685  dvne0  19755  lhop1lem  19757  lhop  19760  dvcnvrelem2  19762  itgsubstlem  19792  ig1peu  19954  ig1pval3  19957  aaliou2  20117  aaliou2b  20118  tayl0  20138  pilem1  20227  rlimcnp2  20665  xrlimcnp  20667  fsumharmonic  20710  ppisval  20746  ppisval2  20747  ppinprm  20795  chtnprm  20797  prmorcht  20821  fsumvma2  20858  pclogsum  20859  vmasum  20860  chpchtsum  20863  chpub  20864  2sqlem7  21014  chebbnd1lem1  21023  rpvmasum2  21066  issubgo  21732  isexid2  21754  smgrpismgm  21761  smgrpisass  21762  issmgrp  21763  mndoissmgrp  21768  mndoisexid  21769  mndomgmid  21771  ismndo  21772  rngo1cl  21858  minvecolem1  22217  minvecolem4a  22220  minvecolem4b  22221  minvecolem4  22223  h2hcau  22323  axhcompl-zf  22342  hhcmpl  22543  hhcms  22546  ocin  22639  ocnel  22641  shuni  22643  shmodsi  22732  pjhthlem2  22735  omlsilem  22745  pjoc1i  22774  spansnm0i  22993  nonbooli  22994  5oalem1  22997  5oalem2  22998  5oalem4  23000  5oalem5  23001  5oalem7  23003  3oalem2  23006  3oalem3  23007  pjssmii  23024  mayete3i  23071  mayete3iOLD  23072  nmcopex  23373  nmcoplb  23374  lncnopbd  23381  nmcfnex  23397  nmcfnlb  23398  riesz4  23408  riesz1  23409  riesz2  23410  cnlnadjlem3  23413  cnlnadjlem5  23415  cnlnadjlem9  23419  cnlnadjeu  23422  rnbra  23451  pjimai  23520  pjclem4a  23542  pjclem4  23543  pj3lem1  23550  pj3si  23551  jpi  23614  sumdmdii  23759  sumdmdlem  23762  sumdmdlem2  23763  cdjreui  23776  cdj3lem1  23778  disjorf  23858  1stpreima  23929  2ndpreima  23930  iocinioc2  23971  ssnnssfz  23977  xrge0tsmsd  24045  kerunit  24070  cnre2csqima  24106  pnfneige0  24133  lmxrge0  24134  qqhucn  24168  esum0  24233  gsumesum  24240  esumcst  24244  esumpcvgval  24257  esumcvg  24265  sigainb  24308  measvuni  24355  cnllyscon  24704  rellyscon  24710  cvmsss2  24733  cvmcov2  24734  cvmopnlem  24737  dfres3  25133  dfon2lem4  25159  predel  25200  wfrlem5  25277  frrlem5  25302  ellimits  25467  dfom5b  25469  brapply  25494  brcap  25496  dfrdg4  25506  tfrqfree  25507  onsucconi  25894  onintopsscon  25897  onsucsuccmpi  25900  limsucncmpi  25902  onint1  25906  itg2gt0cn  25953  finminlem  26005  comppfsc  26071  neibastop2lem  26073  neibastop2  26074  neifg  26084  tailfb  26090  inixp  26114  0totbnd  26166  sstotbnd3  26169  blbnd  26180  ssbnd  26181  heibor1lem  26202  heibor1  26203  heiborlem1  26204  heiborlem6  26209  heiborlem8  26211  heibor  26214  exidresid  26238  isfld2  26299  prtlem14  26407  elrfi  26432  elrfirn  26433  cmpfiiin  26435  mrefg2  26445  fz1eqin  26511  fnwe2lem2  26810  dfac11  26822  kelac1  26823  kelac2lem  26824  dfac21  26826  islmodfg  26829  islssfg2  26831  islssfgi  26832  filnm  26854  lnr2i  26982  lpirlnr  26983  hbtlem6  26995  hbt  26996  acsfn1p  27169  subrgacs  27170  sdrgacs  27171  cntzsdrg  27172  stoweidlem39  27449  stoweidlem44  27454  stoweidlem50  27460  stoweidlem57  27467  eldmressn  27645  afvres  27698  frgrancvvdeqlem4  27778  frgrancvvdeqlem7  27781  frgrancvvdeqlemA  27782  frgrancvvdeqlemC  27784  onfrALTlem2  27968  onfrALTlem2VD  28335  bnj521  28435  bnj1153  28495  bnj1172  28701  bnj1173  28702  bnj1174  28703  bnj1279  28718  lshpdisj  29153  lkrin  29330  ishlat1  29518  pmodlem1  30011  pmodlem2  30012  pclfinN  30065  pclcmpatN  30066  osumcllem4N  30124  pexmidlem1N  30135  dihmeetlem1N  31456  dihglblem5apreN  31457  dihmeetlem4preN  31472  dihmeetlem13N  31485  dochnel2  31558  lcdlss  31785  mapd1o  31814  mapdunirnN  31816  baerlem3lem2  31876  baerlem5alem2  31877  baerlem5blem2  31878  hdmaprnlem9N  32026
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-v 2894  df-in 3263
  Copyright terms: Public domain W3C validator