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

Theorem elin 3530
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 2964 . 2  |-  ( A  e.  ( B  i^i  C )  ->  A  e.  _V )
2 elex 2964 . . 3  |-  ( A  e.  C  ->  A  e.  _V )
32adantl 453 . 2  |-  ( ( A  e.  B  /\  A  e.  C )  ->  A  e.  _V )
4 eleq1 2496 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
5 eleq1 2496 . . . 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 3327 . . 3  |-  ( B  i^i  C )  =  { x  |  ( x  e.  B  /\  x  e.  C ) }
86, 7elab2g 3084 . 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 1652    e. wcel 1725   _Vcvv 2956    i^i cin 3319
This theorem is referenced by:  elin2  3531  elin3  3532  incom  3533  ineqri  3534  ineq1  3535  inass  3551  inss1  3561  ssin  3563  ssrin  3566  dfss4  3575  difin  3578  indi  3587  undi  3588  unineq  3591  indifdir  3597  difin2  3603  inrab2  3614  inelcm  3682  difin0ss  3694  inssdif0  3695  inundif  3706  uniin  4035  intun  4082  intpr  4083  elrint  4091  iunin2  4155  iinin2  4161  elriin  4163  disjor  4196  disjiun  4202  brin  4259  trin  4312  inex1  4344  inuni  4362  wefrc  4576  ordtri3or  4613  ordpwsuc  4795  inopab  5005  inxp  5007  dmin  5077  opelres  5151  intasym  5249  asymref  5250  dminss  5286  imainss  5287  inimasn  5289  ssrnres  5309  cnvresima  5359  dfco2a  5370  2elresin  5556  respreima  5859  isomin  6057  isoini  6058  offval  6312  tfrlem5  6641  erdisj  6952  uniinqs  6984  mapval2  7043  ixpin  7087  boxriin  7104  disjen  7264  ssenen  7281  onfin2  7298  elfpw  7408  unifpw  7409  f1opwfi  7410  fissuni  7411  fipreima  7412  elfir  7420  inelfi  7423  fiin  7427  inf3lem2  7584  cantnfcl  7622  epfrs  7667  cp  7815  bnd2  7817  tskwe  7837  infpwfidom  7909  infpwfien  7943  dfac5lem1  8004  dfac5lem5  8008  dfac5  8009  kmlem3  8032  kmlem14  8043  kmlem15  8044  ackbij2lem1  8099  ackbij1lem3  8102  ackbij1lem4  8103  ackbij1lem6  8105  ackbij1lem11  8110  fin23lem24  8202  fin23lem26  8205  isfin1-3  8266  fpwwe2lem12  8516  fpwwe  8521  canthnumlem  8523  pwxpndom2  8540  ingru  8690  gruina  8693  grur1  8695  axgroth4  8707  grothprim  8709  ixxdisj  10931  icodisj  11022  fzdisj  11078  uzdisj  11119  fzouzdisj  11169  fz1isolem  11710  limsupgle  12271  ello12  12310  elo12  12321  lo1resb  12358  rlimresb  12359  o1resb  12360  lo1eq  12362  rlimeq  12363  fsumsplit  12533  sumsplit  12552  fsum2dlem  12554  explecnv  12644  bitsmod  12948  saddisjlem  12976  sadadd  12979  sadass  12983  smuval2  12994  smupval  13000  smueqlem  13002  smumul  13005  prmreclem5  13288  prmrec  13290  4sqlem12  13324  vdwmc  13346  strfv2d  13499  submre  13830  submrc  13853  isacs2  13878  acsfn  13884  coffth  14133  catcoppccl  14263  catcfuccl  14264  catcxpccl  14304  isdrs2  14396  fpwipodrs  14590  psss  14646  subgacs  14975  nsgacs  14976  resscntz  15130  sylow2a  15253  lsmmod  15307  lsmdisj  15313  lsmdisj2  15314  subgdisj1  15323  frgpnabllem1  15484  gsumzsplit  15529  dmdprdd  15560  dprdfeq0  15580  dprdres  15586  subgdmdprd  15592  dprdcntz2  15596  dprddisj2  15597  dprd2da  15600  dmdprdsplit2lem  15603  ablfacrp  15624  pgpfac1lem3a  15634  pgpfac1lem3  15635  pgpfaclem1  15639  isrhm  15824  subsubrg2  15895  lssacs  16043  lspdisj  16197  lspdisjb  16198  isassa  16375  aspval  16387  aspid  16389  aspval2  16405  mplind  16562  zlpirlem1  16768  zlpirlem3  16770  dfprm2  16774  ocvin  16901  unocv  16907  iunocv  16908  obselocv  16955  isbasis2g  17013  baspartn  17019  tgval2  17021  bastg  17031  tgcl  17034  ppttop  17071  epttop  17073  clsval2  17114  ssntr  17122  isopn3  17130  ntreq0  17141  isclo  17151  restbas  17222  restntr  17246  restlp  17247  cnpresti  17352  cnprest  17353  cnprest2  17354  lmss  17362  haust1  17416  nrmsep3  17419  isnrm2  17422  lmmo  17444  cmpcovf  17454  fincmp  17456  0cmp  17457  discmp  17461  cmpsublem  17462  cmpsub  17463  uncmp  17466  hauscmplem  17469  bwth  17473  iscon2  17477  conclo  17478  dfcon2  17482  iunconlem  17490  uncon  17492  is1stc2  17505  1stcrest  17516  1stcelcls  17524  llyi  17537  nllyi  17538  llynlly  17540  subislly  17544  restnlly  17545  restlly  17546  islly2  17547  llyrest  17548  nllyrest  17549  llyidm  17551  nllyidm  17552  hausllycmp  17557  cldllycmp  17558  lly1stc  17559  dislly  17560  llycmpkgen2  17582  1stckgenlem  17585  txcnp  17652  txcnmpt  17656  txlly  17668  txnlly  17669  txtube  17672  txcmplem1  17673  txcmplem2  17674  hausdiag  17677  xkococnlem  17691  basqtop  17743  tgqtop  17744  kqcldsat  17765  ptcmpfi  17845  isfbas2  17867  isfil2  17888  infil  17895  fbasfip  17900  elfg  17903  filcon  17915  rnelfmlem  17984  rnelfm  17985  fmfnfmlem2  17987  fmfnfmlem4  17989  fmfnfm  17990  flimrest  18015  hauspwpwf1  18019  fclsrest  18056  alexsubALTlem2  18079  alexsubALTlem3  18080  alexsubALTlem4  18081  alexsubALT  18082  ptcmp  18089  istmd  18104  istgp  18107  tgpconcompss  18143  tsmssubm  18172  tsmssplit  18181  istrg  18193  istdrg  18195  istlm  18214  ustfilxp  18242  utoptop  18264  utop3cls  18281  bldisj  18428  blin  18451  blin2  18459  blres  18461  lpbl  18533  metrest  18554  restmetu  18617  isngp  18643  isnlm  18711  isnmhm  18780  tgioo  18827  xrtgioo  18837  xrsmopn  18843  zdis  18847  icccmplem1  18853  icccmplem2  18854  reconnlem2  18858  xrge0tsms  18865  icoopnst  18964  iocopnst  18965  cnheibor  18980  cnllycmp  18981  bndth  18983  iscph  19133  cphsqrcl  19147  tchcph  19194  cfilfcls  19227  cmetcaulem  19241  cmetss  19267  isbn  19291  cldcss2  19343  hlhil  19344  ovolfcl  19363  ovollb2lem  19384  ovolctb  19386  ovolshftlem1  19405  ovolscalem1  19409  ovolicc1  19412  ovolicc2lem2  19414  ovolicc2lem4  19416  ovolicc2lem5  19417  ovolicc2  19418  shftmbl  19433  volfiniun  19441  ioombl1lem1  19452  ioorf  19465  ioorcl  19469  dyadf  19483  vitalilem2  19501  vitali  19505  mbfmax  19541  mbfimaopnlem  19547  mbfaddlem  19552  mbfadd  19553  mbfsub  19554  i1faddlem  19585  i1fmullem  19586  i1fres  19597  itg1climres  19606  mbfi1fseqlem4  19610  mbfmul  19618  itg2splitlem  19640  itg2split  19641  itgresr  19670  bddmulibl  19730  ellimc2  19764  ellimc3  19766  limcun  19782  dvreslem  19796  dvres2lem  19797  dvaddbr  19824  dvmulbr  19825  dvne0  19895  lhop1lem  19897  lhop  19900  dvcnvrelem2  19902  itgsubstlem  19932  ig1peu  20094  ig1pval3  20097  aaliou2  20257  aaliou2b  20258  tayl0  20278  pilem1  20367  rlimcnp2  20805  xrlimcnp  20807  fsumharmonic  20850  ppisval  20886  ppisval2  20887  ppinprm  20935  chtnprm  20937  prmorcht  20961  fsumvma2  20998  pclogsum  20999  vmasum  21000  chpchtsum  21003  chpub  21004  2sqlem7  21154  chebbnd1lem1  21163  rpvmasum2  21206  issubgo  21891  isexid2  21913  smgrpismgm  21920  smgrpisass  21921  issmgrp  21922  mndoissmgrp  21927  mndoisexid  21928  mndomgmid  21930  ismndo  21931  rngo1cl  22017  minvecolem1  22376  minvecolem4a  22379  minvecolem4b  22380  minvecolem4  22382  h2hcau  22482  axhcompl-zf  22501  hhcmpl  22702  hhcms  22705  ocin  22798  ocnel  22800  shuni  22802  shmodsi  22891  pjhthlem2  22894  omlsilem  22904  pjoc1i  22933  spansnm0i  23152  nonbooli  23153  5oalem1  23156  5oalem2  23157  5oalem4  23159  5oalem5  23160  5oalem7  23162  3oalem2  23165  3oalem3  23166  pjssmii  23183  mayete3i  23230  mayete3iOLD  23231  nmcopex  23532  nmcoplb  23533  lncnopbd  23540  nmcfnex  23556  nmcfnlb  23557  riesz4  23567  riesz1  23568  riesz2  23569  cnlnadjlem3  23572  cnlnadjlem5  23574  cnlnadjlem9  23578  cnlnadjeu  23581  rnbra  23610  pjimai  23679  pjclem4a  23701  pjclem4  23702  pj3lem1  23709  pj3si  23710  jpi  23773  sumdmdii  23918  sumdmdlem  23921  sumdmdlem2  23922  cdjreui  23935  cdj3lem1  23937  disjorf  24021  ofpreima  24081  1stpreima  24095  2ndpreima  24096  iocinioc2  24142  ssnnssfz  24148  xrge0tsmsd  24223  kerunit  24261  cnre2csqima  24309  pnfneige0  24336  lmxrge0  24337  qqhucn  24376  esum0  24444  gsumesum  24451  esumcst  24455  esumpcvgval  24468  esumcvg  24476  sigainb  24519  measvuni  24568  cnllyscon  24932  rellyscon  24938  cvmsss2  24961  cvmcov2  24962  cvmopnlem  24965  fprod2dlem  25304  dfres3  25382  elima4  25404  dfon2lem4  25413  predel  25458  wfrlem5  25542  frrlem5  25586  ellimits  25755  dfom5b  25757  brapply  25783  brcap  25785  dfrdg4  25795  tfrqfree  25796  onsucconi  26187  onintopsscon  26190  onsucsuccmpi  26193  limsucncmpi  26195  onint1  26199  mblfinlem2  26244  mbfposadd  26254  itg2gt0cn  26260  finminlem  26321  comppfsc  26387  neibastop2lem  26389  neibastop2  26390  neifg  26400  tailfb  26406  inixp  26430  0totbnd  26482  sstotbnd3  26485  blbnd  26496  ssbnd  26497  heibor1lem  26518  heibor1  26519  heiborlem1  26520  heiborlem6  26525  heiborlem8  26527  heibor  26530  exidresid  26554  isfld2  26615  prtlem14  26723  elrfi  26748  elrfirn  26749  cmpfiiin  26751  mrefg2  26761  fz1eqin  26827  fnwe2lem2  27126  dfac11  27137  kelac1  27138  kelac2lem  27139  dfac21  27141  islmodfg  27144  islssfg2  27146  islssfgi  27147  filnm  27169  lnr2i  27297  lpirlnr  27298  hbtlem6  27310  hbt  27311  acsfn1p  27484  subrgacs  27485  sdrgacs  27486  cntzsdrg  27487  stoweidlem39  27764  stoweidlem44  27769  stoweidlem50  27775  stoweidlem57  27782  eldmressn  27960  afvres  28012  frgrancvvdeqlem4  28422  frgrancvvdeqlem7  28425  frgrancvvdeqlemA  28426  frgrancvvdeqlemC  28428  onfrALTlem2  28632  onfrALTlem2VD  29001  bnj521  29104  bnj1153  29164  bnj1172  29370  bnj1173  29371  bnj1174  29372  bnj1279  29387  lshpdisj  29785  lkrin  29962  ishlat1  30150  pmodlem1  30643  pmodlem2  30644  pclfinN  30697  pclcmpatN  30698  osumcllem4N  30756  pexmidlem1N  30767  dihmeetlem1N  32088  dihglblem5apreN  32089  dihmeetlem4preN  32104  dihmeetlem13N  32117  dochnel2  32190  lcdlss  32417  mapd1o  32446  mapdunirnN  32448  baerlem3lem2  32508  baerlem5alem2  32509  baerlem5blem2  32510  hdmaprnlem9N  32658
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-in 3327
  Copyright terms: Public domain W3C validator