Theorem elin 3669

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 3102	. 2 |- ( A e. ( B i^i C ) -> A e. _V )
2		elex 3102	. . 3 |- ( A e. C -> A e. _V )
3	2	adantl 466	. 2 |- ( ( A e. B /\ A e. C ) -> A e. _V )
4		eleq1 2513	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2513	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
6	4, 5	anbi12d 710	. . 3 |- ( x = A -> ( ( x e. B /\ x e. C ) <-> ( A e. B /\ A e. C ) ) )
7		df-in 3465	. . 3 |- ( B i^i C ) = { x | ( x e. B /\ x e. C ) }
8	6, 7	elab2g 3232	. 2 |- ( A e. _V -> ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) ) )
9	1, 3, 8	pm5.21nii 353	1 |- ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) )

Syntax hints:   <-> wb 184   /\ wa 369   = wceq 1381   e. wcel 1802   _Vcvv 3093   i^i cin 3457

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-in 3465

This theorem is referenced by:  elind  3670  elin2  3671  elin3  3672  incom  3673  ineqri  3674  ineq1  3675  inass  3690  inss1  3700  ssin  3702  ssrin  3705  dfss4  3714  difin  3717  indi  3726  undi  3727  unineq  3730  indifdir  3736  difin2  3742  inrab2  3753  inelcm  3863  difin0ss  3876  inssdif0  3877  inundif  3888  uniin  4250  intun  4300  intpr  4301  elrint  4309  iunin2  4375  iinin2  4381  elriin  4384  disjor  4417  disjiun  4423  brin  4482  trin  4536  inex1  4574  inuni  4595  wefrc  4859  ordtri3or  4896  inopab  5119  inxp  5121  dmin  5196  opelres  5265  eldmeldmressn  5300  intasym  5368  asymref  5369  dminss  5406  imainss  5407  inimasn  5409  ssrnres  5431  cnvresima  5482  dfco2a  5493  2elresin  5678  respreima  5997  fvcofneq  6020  isomin  6214  isoini  6215  offval  6528  ordpwsuc  6631  ressuppss  6917  erdisj  7357  uniinqs  7389  mapval2  7446  ixpin  7492  boxriin  7509  disjen  7672  ssenen  7689  onfin2  7707  elfpw  7820  fiin  7880  inf3lem2  8044  epfrs  8160  cp  8307  bnd2  8309  dfac5lem1  8502  dfac5lem5  8506  dfac5  8507  kmlem3  8530  kmlem14  8541  kmlem15  8542  fin23lem26  8703  isfin1-3  8764  pwxpndom2  9041  ingru  9191  gruina  9194  grur1  9196  axgroth4  9208  grothprim  9210  ixxdisj  11548  icodisj  11649  fzdisj  11716  uzdisj  11755  nn0disj  11794  fzouzdisj  11835  limsupgle  13274  ello12  13313  elo12  13324  lo1resb  13361  rlimresb  13362  o1resb  13363  lo1eq  13365  rlimeq  13366  fsumsplit  13536  sumsplit  13557  fsum2dlem  13559  explecnv  13650  bitsmod  13958  saddisjlem  13986  sadadd  13989  sadass  13993  smuval2  14004  smupval  14010  smueqlem  14012  smumul  14015  prmreclem5  14310  prmrec  14312  4sqlem12  14346  vdwmc  14368  acsfn  14928  isdrs2  15437  fpwipodrs  15663  psss  15713  subgacs  16105  nsgacs  16106  resscntz  16238  gsmsymgreq  16326  sylow2a  16508  lsmmod  16562  lsmdisj2  16569  gsumzsplit  16813  gsumzsplitOLD  16814  subgdmdprd  16949  dprdcntz2  16954  dprddisj2  16955  dprddisj2OLD  16956  pgpfac1lem3  16996  isrhm  17238  subsubrg2  17324  lssacs  17481  lspdisj  17639  lspdisjb  17640  isassa  17832  aspid  17847  aspval2  17864  dfprm2  18391  dfprm2OLD  18394  ocvin  18572  unocv  18578  iunocv  18579  obselocv  18626  pmatcoe1fsupp  19069  isbasis2g  19316  tgval2  19324  tgcl  19337  ppttop  19374  epttop  19376  clsval2  19417  ssntr  19425  ntreq0  19444  isclo  19454  restntr  19549  restlp  19550  cnpresti  19655  cnprest  19656  cnprest2  19657  lmss  19665  haust1  19719  nrmsep3  19722  isnrm2  19725  lmmo  19747  fincmp  19759  0cmp  19760  discmp  19764  cmpsublem  19765  cmpsub  19766  uncmp  19769  hauscmplem  19772  bwthOLD  19777  dfcon2  19786  iunconlem  19794  uncon  19796  is1stc2  19809  1stcrest  19820  1stcelcls  19828  llyi  19841  nllyi  19842  subislly  19848  lly1stc  19863  comppfsc  19899  txcnp  19987  txcnmpt  19991  hausdiag  20012  kqcldsat  20100  ptcmpfi  20180  isfbas2  20202  isfil2  20223  fbasfip  20235  elfg  20238  filcon  20250  rnelfmlem  20319  rnelfm  20320  fmfnfmlem2  20322  fmfnfmlem4  20324  fmfnfm  20325  flimrest  20350  hauspwpwf1  20354  fclsrest  20391  alexsubALTlem2  20414  alexsubALTlem3  20415  alexsubALTlem4  20416  alexsubALT  20417  ptcmp  20424  istmd  20439  istgp  20442  tsmssubm  20510  tsmssplit  20520  istrg  20532  istdrg  20534  istlm  20553  ustfilxp  20581  utoptop  20603  utop3cls  20620  bldisj  20767  blin  20790  blin2  20798  blres  20800  lpbl  20872  metrest  20893  restmetu  20956  isngp  20982  isnlm  21050  isnmhm  21119  xrtgioo  21177  xrsmopn  21183  icccmplem2  21194  reconnlem2  21198  icoopnst  21305  iocopnst  21306  bndth  21324  iscph  21483  tchcph  21546  cfilfcls  21579  cmetcaulem  21593  cmetss  21619  isbn  21643  cldcss2  21723  hlhil  21724  ovolfcl  21744  ovolicc1  21793  ovolicc2lem2  21795  ovolicc2lem4  21797  ovolicc2lem5  21798  ovolicc2  21799  shftmbl  21815  volfiniun  21823  ioorf  21848  mbfmax  21922  mbfimaopnlem  21928  mbfaddlem  21933  mbfadd  21934  mbfsub  21935  i1faddlem  21966  i1fmullem  21967  i1fres  21978  itg1climres  21987  mbfi1fseqlem4  21991  mbfmul  21999  itg2splitlem  22021  itg2split  22022  itgresr  22051  bddmulibl  22111  ellimc2  22147  ellimc3  22149  limcun  22165  dvreslem  22179  dvne0  22278  itgsubstlem  22315  ig1pval3  22441  aaliou2  22601  aaliou2b  22602  pilem1  22711  rlimcnp2  23161  fsumharmonic  23206  ppisval2  23243  prmorcht  23317  fsumvma2  23354  pclogsum  23355  vmasum  23356  chpchtsum  23359  chpub  23360  chebbnd1lem1  23519  rpvmasum2  23562  tglineineq  23888  frgrancvvdeqlem4  24898  frgrancvvdeqlem7  24901  frgrancvvdeqlemA  24902  frgrancvvdeqlemC  24904  issubgo  25170  isexid2  25192  smgrpismgmOLD  25199  smgrpisass  25200  issmgrpOLD  25201  mndoissmgrpOLD  25206  mndoisexid  25207  ismndo  25210  rngo1cl  25296  minvecolem1  25655  minvecolem4a  25658  minvecolem4b  25659  minvecolem4  25661  h2hcau  25761  axhcompl-zf  25780  hhcmpl  25982  hhcms  25985  ocin  26079  ocnel  26081  shmodsi  26172  pjhthlem2  26175  omlsilem  26185  pjoc1i  26214  spansnm0i  26433  nonbooli  26434  5oalem7  26443  3oalem3  26447  pjssmii  26464  mayete3i  26511  mayete3iOLD  26512  nmcopex  26813  nmcoplb  26814  lncnopbd  26821  nmcfnex  26837  nmcfnlb  26838  riesz4  26848  riesz1  26849  riesz2  26850  cnlnadjlem3  26853  cnlnadjlem5  26855  cnlnadjlem9  26859  cnlnadjeu  26862  rnbra  26891  pjimai  26960  pjclem4a  26982  pj3lem1  26990  jpi  27054  sumdmdii  27199  sumdmdlem  27202  sumdmdlem2  27203  cdjreui  27216  cdj3lem1  27218  disjorf  27305  ofpreima  27372  1stpreima  27389  2ndpreima  27390  iocinioc2  27455  ssnnssfz  27462  isorng  27655  kerunit  27679  crefdf  27717  cmpcref  27719  cmppcmp  27727  pcmplfin  27729  cnre2csqima  27759  ordtconlem1  27772  lmxrge0  27800  isrrext  27847  esum0  27926  esumcst  27937  esumpcvgval  27950  esumcvg  27958  measvuni  28051  eulerpartlemt0  28174  eulerpartlemr  28179  eulerpartlemgf  28184  eulerpartlemgs2  28185  eulerpartlemn  28186  sseqf  28197  fiblem  28203  fprod2dlem  29078  dfres3  29156  elima4  29177  dfon2lem4  29186  predel  29231  wfrlem5  29315  frrlem5  29359  ellimits  29528  dfom5b  29530  brapply  29556  brcap  29558  dfrdg4  29568  tfrqfree  29569  onsucconi  29870  onintopsscon  29873  onsucsuccmpi  29876  limsucncmpi  29878  onint1  29882  ptrest  30016  mblfinlem2  30020  mbfposadd  30030  itg2gt0cn  30038  dvasin  30071  finminlem  30104  neibastop2lem  30146  neibastop2  30147  neifg  30157  tailfb  30163  inixp  30187  0totbnd  30237  sstotbnd3  30240  heibor1lem  30273  heibor1  30274  heiborlem6  30280  exidresid  30309  isfld2  30370  prtlem14  30583  cmpfiiin  30597  mrefg2  30607  fz1eqin  30670  fnwe2lem2  30965  islmodfg  30983  islssfg2  30985  lnr2i  31033  acsfn1p  31117  subrgacs  31118  sdrgacs  31119  isprm7  31161  radcnvrat  31164  nzin  31192  elinel2  31371  elinel1  31372  iooabslt  31464  iccintsng  31495  lptioo2cn  31555  lptioo1cn  31556  cncfuni  31592  icccncfext  31593  stoweidlem44  31711  fourierdlem42  31816  fourierdlem80  31854  eldmressn  32042  afvres  32091  tpres  32386  rnghmval2  32409  rnghmsubcsetclem1  32502  rngccatidOLD  32516  rhmsubcsetclem1  32542  rhmsubcrngclem1  32548  ringcbasbas  32555  funcringcsetclem7  32562  ringccatidOLD  32572  ringcbasbasOLD  32578  funcringcsetclem7OLD  32585  srhmsubclem1  32589  fldhmsubc  32600  srhmsubcOLDlem1  32608  fldhmsubcOLD  32619  rhmsubcOLDlem3  32623  ssnn0ssfz  32646  onfrALTlem2  33026  onfrALTlem2VD  33397  bnj521  33500  bnj1172  33764  bnj1173  33765  bnj1174  33766  bnj1279  33781  bj-inrab  34207  bj-eldiag  34309  bj-ccinftydisj  34318  lshpdisj  34414  lkrin  34591  ishlat1  34779  pmodlem2  35273  pclfinN  35326  pclcmpatN  35327  osumcllem4N  35385  pexmidlem1N  35396  dihmeetlem1N  36719  dihglblem5apreN  36720  dihmeetlem4preN  36735  dihmeetlem13N  36748  dochnel2  36821  lcdlss  37048  mapd1o  37077  baerlem3lem2  37139  baerlem5alem2  37140  baerlem5blem2  37141  taupilem3  37396  rp-fakeinunass  37405  fiinfi  37423  xpcogend  37428  cotr2g  37441