Theorem elin 3490

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.

Step	Hyp	Ref	Expression
1		elex 2924	. 2 |- ( A e. ( B i^i C ) -> A e. _V )
2		elex 2924	. . 3 |- ( A e. C -> A e. _V )
3	2	adantl 453	. 2 |- ( ( A e. B /\ A e. C ) -> A e. _V )
4		eleq1 2464	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2464	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
6	4, 5	anbi12d 692	. . 3 |- ( x = A -> ( ( x e. B /\ x e. C ) <-> ( A e. B /\ A e. C ) ) )
7		df-in 3287	. . 3 |- ( B i^i C ) = { x | ( x e. B /\ x e. C ) }
8	6, 7	elab2g 3044	. 2 |- ( A e. _V -> ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) ) )
9	1, 3, 8	pm5.21nii 343	1 |- ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) )

Syntax hints:   <-> wb 177   /\ wa 359   = wceq 1649   e. wcel 1721   _Vcvv 2916   i^i cin 3279

This theorem is referenced by:  elin2  3491  elin3  3492  incom  3493  ineqri  3494  ineq1  3495  inass  3511  inss1  3521  ssin  3523  ssrin  3526  dfss4  3535  difin  3538  indi  3547  undi  3548  unineq  3551  indifdir  3557  difin2  3563  inrab2  3574  inelcm  3642  difin0ss  3654  inssdif0  3655  inundif  3666  uniin  3995  intun  4042  intpr  4043  elrint  4051  iunin2  4115  iinin2  4121  elriin  4123  disjor  4156  disjiun  4162  brin  4219  trin  4272  inex1  4304  inuni  4322  wefrc  4536  ordtri3or  4573  ordpwsuc  4754  inopab  4964  inxp  4966  dmin  5036  opelres  5110  intasym  5208  asymref  5209  dminss  5245  imainss  5246  inimasn  5248  ssrnres  5268  cnvresima  5318  dfco2a  5329  2elresin  5515  respreima  5818  isomin  6016  isoini  6017  offval  6271  tfrlem5  6600  erdisj  6911  uniinqs  6943  mapval2  7002  ixpin  7046  boxriin  7063  disjen  7223  ssenen  7240  onfin2  7257  elfpw  7366  unifpw  7367  f1opwfi  7368  fissuni  7369  fipreima  7370  elfir  7378  inelfi  7381  fiin  7385  inf3lem2  7540  cantnfcl  7578  epfrs  7623  cp  7771  bnd2  7773  tskwe  7793  infpwfidom  7865  infpwfien  7899  dfac5lem1  7960  dfac5lem5  7964  dfac5  7965  kmlem3  7988  kmlem14  7999  kmlem15  8000  ackbij2lem1  8055  ackbij1lem3  8058  ackbij1lem4  8059  ackbij1lem6  8061  ackbij1lem11  8066  fin23lem24  8158  fin23lem26  8161  isfin1-3  8222  fpwwe2lem12  8472  fpwwe  8477  canthnumlem  8479  pwxpndom2  8496  ingru  8646  gruina  8649  grur1  8651  axgroth4  8663  grothprim  8665  ixxdisj  10887  icodisj  10978  fzdisj  11034  uzdisj  11074  fzouzdisj  11124  fz1isolem  11665  limsupgle  12226  ello12  12265  elo12  12276  lo1resb  12313  rlimresb  12314  o1resb  12315  lo1eq  12317  rlimeq  12318  fsumsplit  12488  sumsplit  12507  fsum2dlem  12509  explecnv  12599  bitsmod  12903  saddisjlem  12931  sadadd  12934  sadass  12938  smuval2  12949  smupval  12955  smueqlem  12957  smumul  12960  prmreclem5  13243  prmrec  13245  4sqlem12  13279  vdwmc  13301  strfv2d  13454  submre  13785  submrc  13808  isacs2  13833  acsfn  13839  coffth  14088  catcoppccl  14218  catcfuccl  14219  catcxpccl  14259  isdrs2  14351  fpwipodrs  14545  psss  14601  subgacs  14930  nsgacs  14931  resscntz  15085  sylow2a  15208  lsmmod  15262  lsmdisj  15268  lsmdisj2  15269  subgdisj1  15278  frgpnabllem1  15439  gsumzsplit  15484  dmdprdd  15515  dprdfeq0  15535  dprdres  15541  subgdmdprd  15547  dprdcntz2  15551  dprddisj2  15552  dprd2da  15555  dmdprdsplit2lem  15558  ablfacrp  15579  pgpfac1lem3a  15589  pgpfac1lem3  15590  pgpfaclem1  15594  isrhm  15779  subsubrg2  15850  lssacs  15998  lspdisj  16152  lspdisjb  16153  isassa  16330  aspval  16342  aspid  16344  aspval2  16360  mplind  16517  zlpirlem1  16723  zlpirlem3  16725  dfprm2  16729  ocvin  16856  unocv  16862  iunocv  16863  obselocv  16910  isbasis2g  16968  baspartn  16974  tgval2  16976  bastg  16986  tgcl  16989  ppttop  17026  epttop  17028  clsval2  17069  ssntr  17077  isopn3  17085  ntreq0  17096  isclo  17106  restbas  17176  restntr  17200  restlp  17201  cnpresti  17306  cnprest  17307  cnprest2  17308  lmss  17316  haust1  17370  nrmsep3  17373  isnrm2  17376  lmmo  17398  cmpcovf  17408  fincmp  17410  0cmp  17411  discmp  17415  cmpsublem  17416  cmpsub  17417  uncmp  17420  hauscmplem  17423  iscon2  17430  conclo  17431  dfcon2  17435  iunconlem  17443  uncon  17445  is1stc2  17458  1stcrest  17469  1stcelcls  17477  llyi  17490  nllyi  17491  llynlly  17493  subislly  17497  restnlly  17498  restlly  17499  islly2  17500  llyrest  17501  nllyrest  17502  llyidm  17504  nllyidm  17505  hausllycmp  17510  cldllycmp  17511  lly1stc  17512  dislly  17513  llycmpkgen2  17535  1stckgenlem  17538  txcnp  17605  txcnmpt  17609  txlly  17621  txnlly  17622  txtube  17625  txcmplem1  17626  txcmplem2  17627  hausdiag  17630  xkococnlem  17644  basqtop  17696  tgqtop  17697  kqcldsat  17718  ptcmpfi  17798  isfbas2  17820  isfil2  17841  infil  17848  fbasfip  17853  elfg  17856  filcon  17868  rnelfmlem  17937  rnelfm  17938  fmfnfmlem2  17940  fmfnfmlem4  17942  fmfnfm  17943  flimrest  17968  hauspwpwf1  17972  fclsrest  18009  alexsubALTlem2  18032  alexsubALTlem3  18033  alexsubALTlem4  18034  alexsubALT  18035  ptcmp  18042  istmd  18057  istgp  18060  tgpconcompss  18096  tsmssubm  18125  tsmssplit  18134  istrg  18146  istdrg  18148  istlm  18167  ustfilxp  18195  utoptop  18217  utop3cls  18234  bldisj  18381  blin  18404  blin2  18412  blres  18414  lpbl  18486  metrest  18507  restmetu  18570  isngp  18596  isnlm  18664  isnmhm  18733  tgioo  18780  xrtgioo  18790  xrsmopn  18796  zdis  18800  icccmplem1  18806  icccmplem2  18807  reconnlem2  18811  xrge0tsms  18818  icoopnst  18917  iocopnst  18918  cnheibor  18933  cnllycmp  18934  bndth  18936  iscph  19086  cphsqrcl  19100  tchcph  19147  cfilfcls  19180  cmetcaulem  19194  cmetss  19220  isbn  19244  cldcss2  19296  hlhil  19297  ovolfcl  19316  ovollb2lem  19337  ovolctb  19339  ovolshftlem1  19358  ovolscalem1  19362  ovolicc1  19365  ovolicc2lem2  19367  ovolicc2lem4  19369  ovolicc2lem5  19370  ovolicc2  19371  shftmbl  19386  volfiniun  19394  ioombl1lem1  19405  ioorf  19418  ioorcl  19422  dyadf  19436  vitalilem2  19454  vitali  19458  mbfmax  19494  mbfimaopnlem  19500  mbfaddlem  19505  mbfadd  19506  mbfsub  19507  i1faddlem  19538  i1fmullem  19539  i1fres  19550  itg1climres  19559  mbfi1fseqlem4  19563  mbfmul  19571  itg2splitlem  19593  itg2split  19594  itgresr  19623  bddmulibl  19683  ellimc2  19717  ellimc3  19719  limcun  19735  dvreslem  19749  dvres2lem  19750  dvaddbr  19777  dvmulbr  19778  dvne0  19848  lhop1lem  19850  lhop  19853  dvcnvrelem2  19855  itgsubstlem  19885  ig1peu  20047  ig1pval3  20050  aaliou2  20210  aaliou2b  20211  tayl0  20231  pilem1  20320  rlimcnp2  20758  xrlimcnp  20760  fsumharmonic  20803  ppisval  20839  ppisval2  20840  ppinprm  20888  chtnprm  20890  prmorcht  20914  fsumvma2  20951  pclogsum  20952  vmasum  20953  chpchtsum  20956  chpub  20957  2sqlem7  21107  chebbnd1lem1  21116  rpvmasum2  21159  issubgo  21844  isexid2  21866  smgrpismgm  21873  smgrpisass  21874  issmgrp  21875  mndoissmgrp  21880  mndoisexid  21881  mndomgmid  21883  ismndo  21884  rngo1cl  21970  minvecolem1  22329  minvecolem4a  22332  minvecolem4b  22333  minvecolem4  22335  h2hcau  22435  axhcompl-zf  22454  hhcmpl  22655  hhcms  22658  ocin  22751  ocnel  22753  shuni  22755  shmodsi  22844  pjhthlem2  22847  omlsilem  22857  pjoc1i  22886  spansnm0i  23105  nonbooli  23106  5oalem1  23109  5oalem2  23110  5oalem4  23112  5oalem5  23113  5oalem7  23115  3oalem2  23118  3oalem3  23119  pjssmii  23136  mayete3i  23183  mayete3iOLD  23184  nmcopex  23485  nmcoplb  23486  lncnopbd  23493  nmcfnex  23509  nmcfnlb  23510  riesz4  23520  riesz1  23521  riesz2  23522  cnlnadjlem3  23525  cnlnadjlem5  23527  cnlnadjlem9  23531  cnlnadjeu  23534  rnbra  23563  pjimai  23632  pjclem4a  23654  pjclem4  23655  pj3lem1  23662  pj3si  23663  jpi  23726  sumdmdii  23871  sumdmdlem  23874  sumdmdlem2  23875  cdjreui  23888  cdj3lem1  23890  disjorf  23974  ofpreima  24034  1stpreima  24048  2ndpreima  24049  iocinioc2  24095  ssnnssfz  24101  xrge0tsmsd  24176  kerunit  24214  cnre2csqima  24262  pnfneige0  24289  lmxrge0  24290  qqhucn  24329  esum0  24397  gsumesum  24404  esumcst  24408  esumpcvgval  24421  esumcvg  24429  sigainb  24472  measvuni  24521  cnllyscon  24885  rellyscon  24891  cvmsss2  24914  cvmcov2  24915  cvmopnlem  24918  fprod2dlem  25257  dfres3  25330  dfon2lem4  25356  predel  25397  wfrlem5  25474  frrlem5  25499  ellimits  25664  dfom5b  25666  brapply  25691  brcap  25693  dfrdg4  25703  tfrqfree  25704  onsucconi  26091  onintopsscon  26094  onsucsuccmpi  26097  limsucncmpi  26099  onint1  26103  mblfinlem  26143  mbfposadd  26153  itg2gt0cn  26159  finminlem  26211  comppfsc  26277  neibastop2lem  26279  neibastop2  26280  neifg  26290  tailfb  26296  inixp  26320  0totbnd  26372  sstotbnd3  26375  blbnd  26386  ssbnd  26387  heibor1lem  26408  heibor1  26409  heiborlem1  26410  heiborlem6  26415  heiborlem8  26417  heibor  26420  exidresid  26444  isfld2  26505  prtlem14  26613  elrfi  26638  elrfirn  26639  cmpfiiin  26641  mrefg2  26651  fz1eqin  26717  fnwe2lem2  27016  dfac11  27028  kelac1  27029  kelac2lem  27030  dfac21  27032  islmodfg  27035  islssfg2  27037  islssfgi  27038  filnm  27060  lnr2i  27188  lpirlnr  27189  hbtlem6  27201  hbt  27202  acsfn1p  27375  subrgacs  27376  sdrgacs  27377  cntzsdrg  27378  stoweidlem39  27655  stoweidlem44  27660  stoweidlem50  27666  stoweidlem57  27673  eldmressn  27851  afvres  27903  frgrancvvdeqlem4  28136  frgrancvvdeqlem7  28139  frgrancvvdeqlemA  28140  frgrancvvdeqlemC  28142  onfrALTlem2  28343  onfrALTlem2VD  28710  bnj521  28810  bnj1153  28870  bnj1172  29076  bnj1173  29077  bnj1174  29078  bnj1279  29093  lshpdisj  29470  lkrin  29647  ishlat1  29835  pmodlem1  30328  pmodlem2  30329  pclfinN  30382  pclcmpatN  30383  osumcllem4N  30441  pexmidlem1N  30452  dihmeetlem1N  31773  dihglblem5apreN  31774  dihmeetlem4preN  31789  dihmeetlem13N  31802  dochnel2  31875  lcdlss  32102  mapd1o  32131  mapdunirnN  32133  baerlem3lem2  32193  baerlem5alem2  32194  baerlem5blem2  32195  hdmaprnlem9N  32343

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 2385

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 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287