Theorem elin 3687

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 3122	. 2 |- ( A e. ( B i^i C ) -> A e. _V )
2		elex 3122	. . 3 |- ( A e. C -> A e. _V )
3	2	adantl 466	. 2 |- ( ( A e. B /\ A e. C ) -> A e. _V )
4		eleq1 2539	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2539	. . . 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 3483	. . 3 |- ( B i^i C ) = { x | ( x e. B /\ x e. C ) }
8	6, 7	elab2g 3252	. 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 1379   e. wcel 1767   _Vcvv 3113   i^i cin 3475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483

This theorem is referenced by:  elind  3688  elin2  3689  elin3  3690  incom  3691  ineqri  3692  ineq1  3693  inass  3708  inss1  3718  ssin  3720  ssrin  3723  dfss4  3732  difin  3735  indi  3744  undi  3745  unineq  3748  indifdir  3754  difin2  3760  inrab2  3771  inelcm  3881  difin0ss  3893  inssdif0  3894  inundif  3905  uniin  4265  intun  4314  intpr  4315  elrint  4323  iunin2  4389  iinin2  4395  elriin  4398  disjor  4431  disjiun  4437  brin  4496  trin  4550  inex1  4588  inuni  4609  wefrc  4873  ordtri3or  4910  inopab  5133  inxp  5135  dmin  5210  opelres  5279  eldmeldmressn  5314  intasym  5382  asymref  5383  dminss  5420  imainss  5421  inimasn  5423  ssrnres  5445  cnvresima  5496  dfco2a  5507  2elresin  5692  respreima  6010  fvcofneq  6029  isomin  6221  isoini  6222  offval  6531  ordpwsuc  6634  ressuppss  6919  erdisj  7359  uniinqs  7391  mapval2  7448  ixpin  7494  boxriin  7511  disjen  7674  ssenen  7691  onfin2  7709  elfpw  7822  fiin  7882  inf3lem2  8046  epfrs  8162  cp  8309  bnd2  8311  dfac5lem1  8504  dfac5lem5  8508  dfac5  8509  kmlem3  8532  kmlem14  8543  kmlem15  8544  fin23lem26  8705  isfin1-3  8766  pwxpndom2  9043  ingru  9193  gruina  9196  grur1  9198  axgroth4  9210  grothprim  9212  ixxdisj  11544  icodisj  11645  fzdisj  11712  uzdisj  11751  nn0disj  11788  fzouzdisj  11829  limsupgle  13263  ello12  13302  elo12  13313  lo1resb  13350  rlimresb  13351  o1resb  13352  lo1eq  13354  rlimeq  13355  fsumsplit  13525  sumsplit  13546  fsum2dlem  13548  explecnv  13639  bitsmod  13945  saddisjlem  13973  sadadd  13976  sadass  13980  smuval2  13991  smupval  13997  smueqlem  13999  smumul  14002  prmreclem5  14297  prmrec  14299  4sqlem12  14333  vdwmc  14355  acsfn  14914  isdrs2  15426  fpwipodrs  15651  psss  15701  subgacs  16041  nsgacs  16042  resscntz  16174  gsmsymgreq  16262  sylow2a  16445  lsmmod  16499  lsmdisj2  16506  gsumzsplit  16747  gsumzsplitOLD  16748  subgdmdprd  16883  dprdcntz2  16888  dprddisj2  16889  dprddisj2OLD  16890  pgpfac1lem3  16930  isrhm  17171  subsubrg2  17256  lssacs  17413  lspdisj  17571  lspdisjb  17572  isassa  17763  aspid  17778  aspval2  17795  dfprm2  18319  dfprm2OLD  18322  ocvin  18500  unocv  18506  iunocv  18507  obselocv  18554  pmatcoe1fsupp  18997  isbasis2g  19244  tgval2  19252  tgcl  19265  ppttop  19302  epttop  19304  clsval2  19345  ssntr  19353  ntreq0  19372  isclo  19382  restntr  19477  restlp  19478  cnpresti  19583  cnprest  19584  cnprest2  19585  lmss  19593  haust1  19647  nrmsep3  19650  isnrm2  19653  lmmo  19675  fincmp  19687  0cmp  19688  discmp  19692  cmpsublem  19693  cmpsub  19694  uncmp  19697  hauscmplem  19700  bwthOLD  19705  dfcon2  19714  iunconlem  19722  uncon  19724  is1stc2  19737  1stcrest  19748  1stcelcls  19756  llyi  19769  nllyi  19770  subislly  19776  lly1stc  19791  txcnp  19884  txcnmpt  19888  hausdiag  19909  kqcldsat  19997  ptcmpfi  20077  isfbas2  20099  isfil2  20120  fbasfip  20132  elfg  20135  filcon  20147  rnelfmlem  20216  rnelfm  20217  fmfnfmlem2  20219  fmfnfmlem4  20221  fmfnfm  20222  flimrest  20247  hauspwpwf1  20251  fclsrest  20288  alexsubALTlem2  20311  alexsubALTlem3  20312  alexsubALTlem4  20313  alexsubALT  20314  ptcmp  20321  istmd  20336  istgp  20339  tsmssubm  20407  tsmssplit  20417  istrg  20429  istdrg  20431  istlm  20450  ustfilxp  20478  utoptop  20500  utop3cls  20517  bldisj  20664  blin  20687  blin2  20695  blres  20697  lpbl  20769  metrest  20790  restmetu  20853  isngp  20879  isnlm  20947  isnmhm  21016  xrtgioo  21074  xrsmopn  21080  icccmplem2  21091  reconnlem2  21095  icoopnst  21202  iocopnst  21203  bndth  21221  iscph  21380  tchcph  21443  cfilfcls  21476  cmetcaulem  21490  cmetss  21516  isbn  21540  cldcss2  21620  hlhil  21621  ovolfcl  21641  ovolicc1  21690  ovolicc2lem2  21692  ovolicc2lem4  21694  ovolicc2lem5  21695  ovolicc2  21696  shftmbl  21712  volfiniun  21720  ioorf  21745  mbfmax  21819  mbfimaopnlem  21825  mbfaddlem  21830  mbfadd  21831  mbfsub  21832  i1faddlem  21863  i1fmullem  21864  i1fres  21875  itg1climres  21884  mbfi1fseqlem4  21888  mbfmul  21896  itg2splitlem  21918  itg2split  21919  itgresr  21948  bddmulibl  22008  ellimc2  22044  ellimc3  22046  limcun  22062  dvreslem  22076  dvne0  22175  itgsubstlem  22212  ig1pval3  22338  aaliou2  22498  aaliou2b  22499  pilem1  22608  rlimcnp2  23052  fsumharmonic  23097  ppisval2  23134  prmorcht  23208  fsumvma2  23245  pclogsum  23246  vmasum  23247  chpchtsum  23250  chpub  23251  chebbnd1lem1  23410  rpvmasum2  23453  tglineineq  23764  footex  23831  frgrancvvdeqlem4  24738  frgrancvvdeqlem7  24741  frgrancvvdeqlemA  24742  frgrancvvdeqlemC  24744  issubgo  25009  isexid2  25031  smgrpismgm  25038  smgrpisass  25039  issmgrp  25040  mndoissmgrp  25045  mndoisexid  25046  ismndo  25049  rngo1cl  25135  minvecolem1  25494  minvecolem4a  25497  minvecolem4b  25498  minvecolem4  25500  h2hcau  25600  axhcompl-zf  25619  hhcmpl  25821  hhcms  25824  ocin  25918  ocnel  25920  shmodsi  26011  pjhthlem2  26014  omlsilem  26024  pjoc1i  26053  spansnm0i  26272  nonbooli  26273  5oalem7  26282  3oalem3  26286  pjssmii  26303  mayete3i  26350  mayete3iOLD  26351  nmcopex  26652  nmcoplb  26653  lncnopbd  26660  nmcfnex  26676  nmcfnlb  26677  riesz4  26687  riesz1  26688  riesz2  26689  cnlnadjlem3  26692  cnlnadjlem5  26694  cnlnadjlem9  26698  cnlnadjeu  26701  rnbra  26730  pjimai  26799  pjclem4a  26821  pj3lem1  26829  jpi  26893  sumdmdii  27038  sumdmdlem  27041  sumdmdlem2  27042  cdjreui  27055  cdj3lem1  27057  disjorf  27141  ofpreima  27207  1stpreima  27224  2ndpreima  27225  iocinioc2  27286  ssnnssfz  27293  isorng  27480  kerunit  27504  cnre2csqima  27557  ordtconlem1  27570  lmxrge0  27598  isrrext  27645  esum0  27728  esumcst  27739  esumpcvgval  27752  esumcvg  27760  measvuni  27853  eulerpartlemt0  27976  eulerpartlemr  27981  eulerpartlemgf  27986  eulerpartlemgs2  27987  eulerpartlemn  27988  sseqf  27999  fiblem  28005  fprod2dlem  28715  dfres3  28793  elima4  28814  dfon2lem4  28823  predel  28868  wfrlem5  28952  frrlem5  28996  ellimits  29165  dfom5b  29167  brapply  29193  brcap  29195  dfrdg4  29205  tfrqfree  29206  onsucconi  29507  onintopsscon  29510  onsucsuccmpi  29513  limsucncmpi  29515  onint1  29519  ptrest  29653  mblfinlem2  29657  mbfposadd  29667  itg2gt0cn  29675  dvasin  29708  finminlem  29741  comppfsc  29807  neibastop2lem  29809  neibastop2  29810  neifg  29820  tailfb  29826  inixp  29850  0totbnd  29900  sstotbnd3  29903  heibor1lem  29936  heibor1  29937  heiborlem6  29943  exidresid  29972  isfld2  30033  prtlem14  30247  cmpfiiin  30261  mrefg2  30271  fz1eqin  30334  fnwe2lem2  30629  islmodfg  30647  islssfg2  30649  lnr2i  30697  acsfn1p  30781  subrgacs  30782  sdrgacs  30783  isprm7  30823  nzin  30851  elinel2  31030  elinel1  31031  iooabslt  31124  limciccioolb  31191  limcicciooub  31207  lptre2pt  31210  lptioo2cn  31215  lptioo1cn  31216  cncfuni  31253  icccncfext  31254  cncfiooicclem1  31260  itgiccshift  31326  itgperiod  31327  itgsbtaddcnst  31328  stoweidlem39  31367  stoweidlem44  31372  stoweidlem50  31378  stoweidlem57  31385  fourierdlem20  31455  fourierdlem32  31467  fourierdlem33  31468  fourierdlem42  31477  fourierdlem48  31483  fourierdlem49  31484  fourierdlem62  31497  fourierdlem71  31506  fourierdlem80  31515  eldmressn  31703  afvres  31752  ssnn0ssfz  32034  onfrALTlem2  32416  onfrALTlem2VD  32787  bnj521  32890  bnj1172  33154  bnj1173  33155  bnj1174  33156  bnj1279  33171  bj-inrab  33594  bj-eldiag  33696  bj-ccinftydisj  33706  lshpdisj  33802  lkrin  33979  ishlat1  34167  pmodlem2  34661  pclfinN  34714  pclcmpatN  34715  osumcllem4N  34773  pexmidlem1N  34784  dihmeetlem1N  36105  dihglblem5apreN  36106  dihmeetlem4preN  36121  dihmeetlem13N  36134  dochnel2  36207  lcdlss  36434  mapd1o  36463  baerlem3lem2  36525  baerlem5alem2  36526  baerlem5blem2  36527  taupilem3  36782  fiinfi  36796  xpcogend  36801