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

Theorem elin 3494
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 2928 . 2  |-  ( A  e.  ( B  i^i  C )  ->  A  e.  _V )
2 elex 2928 . . 3  |-  ( A  e.  C  ->  A  e.  _V )
32adantl 453 . 2  |-  ( ( A  e.  B  /\  A  e.  C )  ->  A  e.  _V )
4 eleq1 2468 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
5 eleq1 2468 . . . 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 3291 . . 3  |-  ( B  i^i  C )  =  { x  |  ( x  e.  B  /\  x  e.  C ) }
86, 7elab2g 3048 . 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 1721   _Vcvv 2920    i^i cin 3283
This theorem is referenced by:  elin2  3495  elin3  3496  incom  3497  ineqri  3498  ineq1  3499  inass  3515  inss1  3525  ssin  3527  ssrin  3530  dfss4  3539  difin  3542  indi  3551  undi  3552  unineq  3555  indifdir  3561  difin2  3567  inrab2  3578  inelcm  3646  difin0ss  3658  inssdif0  3659  inundif  3670  uniin  3999  intun  4046  intpr  4047  elrint  4055  iunin2  4119  iinin2  4125  elriin  4127  disjor  4160  disjiun  4166  brin  4223  trin  4276  inex1  4308  inuni  4326  wefrc  4540  ordtri3or  4577  ordpwsuc  4758  inopab  4968  inxp  4970  dmin  5040  opelres  5114  intasym  5212  asymref  5213  dminss  5249  imainss  5250  inimasn  5252  ssrnres  5272  cnvresima  5322  dfco2a  5333  2elresin  5519  respreima  5822  isomin  6020  isoini  6021  offval  6275  tfrlem5  6604  erdisj  6915  uniinqs  6947  mapval2  7006  ixpin  7050  boxriin  7067  disjen  7227  ssenen  7244  onfin2  7261  elfpw  7370  unifpw  7371  f1opwfi  7372  fissuni  7373  fipreima  7374  elfir  7382  inelfi  7385  fiin  7389  inf3lem2  7544  cantnfcl  7582  epfrs  7627  cp  7775  bnd2  7777  tskwe  7797  infpwfidom  7869  infpwfien  7903  dfac5lem1  7964  dfac5lem5  7968  dfac5  7969  kmlem3  7992  kmlem14  8003  kmlem15  8004  ackbij2lem1  8059  ackbij1lem3  8062  ackbij1lem4  8063  ackbij1lem6  8065  ackbij1lem11  8070  fin23lem24  8162  fin23lem26  8165  isfin1-3  8226  fpwwe2lem12  8476  fpwwe  8481  canthnumlem  8483  pwxpndom2  8500  ingru  8650  gruina  8653  grur1  8655  axgroth4  8667  grothprim  8669  ixxdisj  10891  icodisj  10982  fzdisj  11038  uzdisj  11078  fzouzdisj  11128  fz1isolem  11669  limsupgle  12230  ello12  12269  elo12  12280  lo1resb  12317  rlimresb  12318  o1resb  12319  lo1eq  12321  rlimeq  12322  fsumsplit  12492  sumsplit  12511  fsum2dlem  12513  explecnv  12603  bitsmod  12907  saddisjlem  12935  sadadd  12938  sadass  12942  smuval2  12953  smupval  12959  smueqlem  12961  smumul  12964  prmreclem5  13247  prmrec  13249  4sqlem12  13283  vdwmc  13305  strfv2d  13458  submre  13789  submrc  13812  isacs2  13837  acsfn  13843  coffth  14092  catcoppccl  14222  catcfuccl  14223  catcxpccl  14263  isdrs2  14355  fpwipodrs  14549  psss  14605  subgacs  14934  nsgacs  14935  resscntz  15089  sylow2a  15212  lsmmod  15266  lsmdisj  15272  lsmdisj2  15273  subgdisj1  15282  frgpnabllem1  15443  gsumzsplit  15488  dmdprdd  15519  dprdfeq0  15539  dprdres  15545  subgdmdprd  15551  dprdcntz2  15555  dprddisj2  15556  dprd2da  15559  dmdprdsplit2lem  15562  ablfacrp  15583  pgpfac1lem3a  15593  pgpfac1lem3  15594  pgpfaclem1  15598  isrhm  15783  subsubrg2  15854  lssacs  16002  lspdisj  16156  lspdisjb  16157  isassa  16334  aspval  16346  aspid  16348  aspval2  16364  mplind  16521  zlpirlem1  16727  zlpirlem3  16729  dfprm2  16733  ocvin  16860  unocv  16866  iunocv  16867  obselocv  16914  isbasis2g  16972  baspartn  16978  tgval2  16980  bastg  16990  tgcl  16993  ppttop  17030  epttop  17032  clsval2  17073  ssntr  17081  isopn3  17089  ntreq0  17100  isclo  17110  restbas  17180  restntr  17204  restlp  17205  cnpresti  17310  cnprest  17311  cnprest2  17312  lmss  17320  haust1  17374  nrmsep3  17377  isnrm2  17380  lmmo  17402  cmpcovf  17412  fincmp  17414  0cmp  17415  discmp  17419  cmpsublem  17420  cmpsub  17421  uncmp  17424  hauscmplem  17427  iscon2  17434  conclo  17435  dfcon2  17439  iunconlem  17447  uncon  17449  is1stc2  17462  1stcrest  17473  1stcelcls  17481  llyi  17494  nllyi  17495  llynlly  17497  subislly  17501  restnlly  17502  restlly  17503  islly2  17504  llyrest  17505  nllyrest  17506  llyidm  17508  nllyidm  17509  hausllycmp  17514  cldllycmp  17515  lly1stc  17516  dislly  17517  llycmpkgen2  17539  1stckgenlem  17542  txcnp  17609  txcnmpt  17613  txlly  17625  txnlly  17626  txtube  17629  txcmplem1  17630  txcmplem2  17631  hausdiag  17634  xkococnlem  17648  basqtop  17700  tgqtop  17701  kqcldsat  17722  ptcmpfi  17802  isfbas2  17824  isfil2  17845  infil  17852  fbasfip  17857  elfg  17860  filcon  17872  rnelfmlem  17941  rnelfm  17942  fmfnfmlem2  17944  fmfnfmlem4  17946  fmfnfm  17947  flimrest  17972  hauspwpwf1  17976  fclsrest  18013  alexsubALTlem2  18036  alexsubALTlem3  18037  alexsubALTlem4  18038  alexsubALT  18039  ptcmp  18046  istmd  18061  istgp  18064  tgpconcompss  18100  tsmssubm  18129  tsmssplit  18138  istrg  18150  istdrg  18152  istlm  18171  ustfilxp  18199  utoptop  18221  utop3cls  18238  bldisj  18385  blin  18408  blin2  18416  blres  18418  lpbl  18490  metrest  18511  restmetu  18574  isngp  18600  isnlm  18668  isnmhm  18737  tgioo  18784  xrtgioo  18794  xrsmopn  18800  zdis  18804  icccmplem1  18810  icccmplem2  18811  reconnlem2  18815  xrge0tsms  18822  icoopnst  18921  iocopnst  18922  cnheibor  18937  cnllycmp  18938  bndth  18940  iscph  19090  cphsqrcl  19104  tchcph  19151  cfilfcls  19184  cmetcaulem  19198  cmetss  19224  isbn  19248  cldcss2  19300  hlhil  19301  ovolfcl  19320  ovollb2lem  19341  ovolctb  19343  ovolshftlem1  19362  ovolscalem1  19366  ovolicc1  19369  ovolicc2lem2  19371  ovolicc2lem4  19373  ovolicc2lem5  19374  ovolicc2  19375  shftmbl  19390  volfiniun  19398  ioombl1lem1  19409  ioorf  19422  ioorcl  19426  dyadf  19440  vitalilem2  19458  vitali  19462  mbfmax  19498  mbfimaopnlem  19504  mbfaddlem  19509  mbfadd  19510  mbfsub  19511  i1faddlem  19542  i1fmullem  19543  i1fres  19554  itg1climres  19563  mbfi1fseqlem4  19567  mbfmul  19575  itg2splitlem  19597  itg2split  19598  itgresr  19627  bddmulibl  19687  ellimc2  19721  ellimc3  19723  limcun  19739  dvreslem  19753  dvres2lem  19754  dvaddbr  19781  dvmulbr  19782  dvne0  19852  lhop1lem  19854  lhop  19857  dvcnvrelem2  19859  itgsubstlem  19889  ig1peu  20051  ig1pval3  20054  aaliou2  20214  aaliou2b  20215  tayl0  20235  pilem1  20324  rlimcnp2  20762  xrlimcnp  20764  fsumharmonic  20807  ppisval  20843  ppisval2  20844  ppinprm  20892  chtnprm  20894  prmorcht  20918  fsumvma2  20955  pclogsum  20956  vmasum  20957  chpchtsum  20960  chpub  20961  2sqlem7  21111  chebbnd1lem1  21120  rpvmasum2  21163  issubgo  21848  isexid2  21870  smgrpismgm  21877  smgrpisass  21878  issmgrp  21879  mndoissmgrp  21884  mndoisexid  21885  mndomgmid  21887  ismndo  21888  rngo1cl  21974  minvecolem1  22333  minvecolem4a  22336  minvecolem4b  22337  minvecolem4  22339  h2hcau  22439  axhcompl-zf  22458  hhcmpl  22659  hhcms  22662  ocin  22755  ocnel  22757  shuni  22759  shmodsi  22848  pjhthlem2  22851  omlsilem  22861  pjoc1i  22890  spansnm0i  23109  nonbooli  23110  5oalem1  23113  5oalem2  23114  5oalem4  23116  5oalem5  23117  5oalem7  23119  3oalem2  23122  3oalem3  23123  pjssmii  23140  mayete3i  23187  mayete3iOLD  23188  nmcopex  23489  nmcoplb  23490  lncnopbd  23497  nmcfnex  23513  nmcfnlb  23514  riesz4  23524  riesz1  23525  riesz2  23526  cnlnadjlem3  23529  cnlnadjlem5  23531  cnlnadjlem9  23535  cnlnadjeu  23538  rnbra  23567  pjimai  23636  pjclem4a  23658  pjclem4  23659  pj3lem1  23666  pj3si  23667  jpi  23730  sumdmdii  23875  sumdmdlem  23878  sumdmdlem2  23879  cdjreui  23892  cdj3lem1  23894  disjorf  23978  ofpreima  24038  1stpreima  24052  2ndpreima  24053  iocinioc2  24099  ssnnssfz  24105  xrge0tsmsd  24180  kerunit  24218  cnre2csqima  24266  pnfneige0  24293  lmxrge0  24294  qqhucn  24333  esum0  24401  gsumesum  24408  esumcst  24412  esumpcvgval  24425  esumcvg  24433  sigainb  24476  measvuni  24525  cnllyscon  24889  rellyscon  24895  cvmsss2  24918  cvmcov2  24919  cvmopnlem  24922  fprod2dlem  25261  dfres3  25334  dfon2lem4  25360  predel  25401  wfrlem5  25478  frrlem5  25503  ellimits  25668  dfom5b  25670  brapply  25695  brcap  25697  dfrdg4  25707  tfrqfree  25708  onsucconi  26095  onintopsscon  26098  onsucsuccmpi  26101  limsucncmpi  26103  onint1  26107  mblfinlem  26147  mbfposadd  26157  itg2gt0cn  26163  finminlem  26215  comppfsc  26281  neibastop2lem  26283  neibastop2  26284  neifg  26294  tailfb  26300  inixp  26324  0totbnd  26376  sstotbnd3  26379  blbnd  26390  ssbnd  26391  heibor1lem  26412  heibor1  26413  heiborlem1  26414  heiborlem6  26419  heiborlem8  26421  heibor  26424  exidresid  26448  isfld2  26509  prtlem14  26617  elrfi  26642  elrfirn  26643  cmpfiiin  26645  mrefg2  26655  fz1eqin  26721  fnwe2lem2  27020  dfac11  27032  kelac1  27033  kelac2lem  27034  dfac21  27036  islmodfg  27039  islssfg2  27041  islssfgi  27042  filnm  27064  lnr2i  27192  lpirlnr  27193  hbtlem6  27205  hbt  27206  acsfn1p  27379  subrgacs  27380  sdrgacs  27381  cntzsdrg  27382  stoweidlem39  27659  stoweidlem44  27664  stoweidlem50  27670  stoweidlem57  27677  eldmressn  27855  afvres  27907  frgrancvvdeqlem4  28140  frgrancvvdeqlem7  28143  frgrancvvdeqlemA  28144  frgrancvvdeqlemC  28146  onfrALTlem2  28347  onfrALTlem2VD  28714  bnj521  28814  bnj1153  28874  bnj1172  29080  bnj1173  29081  bnj1174  29082  bnj1279  29097  lshpdisj  29474  lkrin  29651  ishlat1  29839  pmodlem1  30332  pmodlem2  30333  pclfinN  30386  pclcmpatN  30387  osumcllem4N  30445  pexmidlem1N  30456  dihmeetlem1N  31777  dihglblem5apreN  31778  dihmeetlem4preN  31793  dihmeetlem13N  31806  dochnel2  31879  lcdlss  32106  mapd1o  32135  mapdunirnN  32137  baerlem3lem2  32197  baerlem5alem2  32198  baerlem5blem2  32199  hdmaprnlem9N  32347
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-v 2922  df-in 3291
  Copyright terms: Public domain W3C validator