Theorem elin 3617

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 3054	. 2 |- ( A e. ( B i^i C ) -> A e. _V )
2		elex 3054	. . 3 |- ( A e. C -> A e. _V )
3	2	adantl 468	. 2 |- ( ( A e. B /\ A e. C ) -> A e. _V )
4		eleq1 2517	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2517	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
6	4, 5	anbi12d 717	. . 3 |- ( x = A -> ( ( x e. B /\ x e. C ) <-> ( A e. B /\ A e. C ) ) )
7		df-in 3411	. . 3 |- ( B i^i C ) = { x | ( x e. B /\ x e. C ) }
8	6, 7	elab2g 3187	. 2 |- ( A e. _V -> ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) ) )
9	1, 3, 8	pm5.21nii 355	1 |- ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) )

Syntax hints:   <-> wb 188   /\ wa 371   = wceq 1444   e. wcel 1887   _Vcvv 3045   i^i cin 3403

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-v 3047  df-in 3411

This theorem is referenced by:  elind  3618  elinel1  3619  elinel2  3620  elin2  3621  elin1d  3622  elin2d  3623  elin3  3624  incom  3625  ineqri  3626  ineq1  3627  inass  3642  inss1  3652  ssin  3654  ssrin  3657  dfss4  3677  difin  3680  indi  3689  undi  3690  unineq  3693  indifdir  3699  difin2  3705  inrab2  3716  inelcm  3819  difin0ss  3833  inssdif0  3834  inundif  3845  uniin  4218  intun  4267  intpr  4268  elrint  4276  iunin2  4342  iinin2  4348  elriin  4351  disjor  4387  disjiun  4393  brin  4452  trin  4507  inex1  4544  inuni  4565  wefrc  4828  inopab  4965  inxp  4967  dmin  5042  opelres  5110  eldmeldmressn  5145  intasym  5215  asymref  5216  dminss  5250  imainss  5251  inimasn  5253  ssrnres  5275  cnvresima  5324  dfco2a  5335  predel  5397  ordtri3or  5455  2elresin  5687  respreima  6009  fvcofneq  6030  tpres  6117  isomin  6228  isoini  6229  offval  6538  ordpwsuc  6642  ressuppss  6934  wfrlem5  7040  erdisj  7411  uniinqs  7443  mapval2  7501  ixpin  7547  boxriin  7564  disjen  7729  ssenen  7746  onfin2  7764  elfpw  7876  fiin  7936  inf3lem2  8134  epfrs  8215  cp  8362  bnd2  8364  dfac5lem1  8554  dfac5lem5  8558  dfac5  8559  kmlem3  8582  kmlem14  8593  kmlem15  8594  fin23lem26  8755  isfin1-3  8816  pwxpndom2  9090  ingru  9240  gruina  9243  grur1  9245  axgroth4  9257  grothprim  9259  ixxdisj  11650  icodisj  11757  fzdisj  11826  uzdisj  11867  nn0disj  11907  fzouzdisj  11954  xpcogend  13038  cotr2g  13040  limsupgle  13535  ello12  13580  elo12  13591  lo1resb  13628  rlimresb  13629  o1resb  13630  lo1eq  13632  rlimeq  13633  fsumsplit  13806  sumsplit  13829  fsum2dlem  13831  explecnv  13923  fprod2dlem  14034  bitsmod  14410  saddisjlem  14438  sadadd  14441  sadass  14445  smuval2  14456  smupval  14462  smueqlem  14464  smumul  14467  prmreclem5  14864  prmrec  14866  4sqlem12  14900  vdwmc  14928  acsfn  15565  iszeroo  15897  iszeroi  15904  isdrs2  16184  fpwipodrs  16410  psss  16460  subgacs  16852  nsgacs  16853  resscntz  16985  gsmsymgreq  17073  sylow2a  17271  lsmmod  17325  lsmdisj2  17332  gsumzsplit  17560  subgdmdprd  17667  dprdcntz2  17671  dprddisj2  17672  pgpfac1lem3  17710  isrhm  17949  subsubrg2  18035  lssacs  18190  lspdisj  18348  lspdisjb  18349  isassa  18539  aspid  18554  aspval2  18571  dfprm2  19065  ocvin  19237  unocv  19243  iunocv  19244  obselocv  19291  pmatcoe1fsupp  19725  isbasis2g  19963  tgval2  19971  tgcl  19985  ppttop  20022  epttop  20024  clsval2  20065  ssntr  20073  ntreq0  20093  isclo  20103  restntr  20198  restlp  20199  cnpresti  20304  cnprest  20305  cnprest2  20306  lmss  20314  haust1  20368  nrmsep3  20371  isnrm2  20374  lmmo  20396  fincmp  20408  0cmp  20409  discmp  20413  cmpsublem  20414  cmpsub  20415  uncmp  20418  hauscmplem  20421  dfcon2  20434  iunconlem  20442  uncon  20444  is1stc2  20457  1stcrest  20468  1stcelcls  20476  llyi  20489  nllyi  20490  subislly  20496  lly1stc  20511  comppfsc  20547  txcnp  20635  txcnmpt  20639  hausdiag  20660  kqcldsat  20748  ptcmpfi  20828  isfbas2  20850  isfil2  20871  fbasfip  20883  elfg  20886  filcon  20898  rnelfmlem  20967  rnelfm  20968  fmfnfmlem2  20970  fmfnfmlem4  20972  fmfnfm  20973  flimrest  20998  hauspwpwf1  21002  fclsrest  21039  alexsubALTlem2  21063  alexsubALTlem3  21064  alexsubALTlem4  21065  alexsubALT  21066  ptcmp  21073  istmd  21089  istgp  21092  tsmssubm  21157  tsmssplit  21166  istrg  21178  istdrg  21180  istlm  21199  ustfilxp  21227  utoptop  21249  utop3cls  21266  bldisj  21413  blin  21436  blin2  21444  blres  21446  lpbl  21518  metrest  21539  restmetu  21585  isngp  21610  isnlm  21678  isnmhm  21767  xrtgioo  21824  xrsmopn  21830  icccmplem2  21841  reconnlem2  21845  icoopnst  21967  iocopnst  21968  bndth  21986  iscph  22148  tchcph  22211  cfilfcls  22244  cmetcaulem  22258  cmetss  22284  isbn  22306  cldcss2  22396  hlhil  22397  ovolfcl  22419  ovolicc1  22469  ovolicc2lem2  22471  ovolicc2lem4OLD  22473  ovolicc2lem4  22474  ovolicc2lem5  22475  ovolicc2  22476  shftmbl  22492  volfiniun  22500  ioorf  22525  ioorfOLD  22530  mbfmax  22605  mbfimaopnlem  22611  mbfaddlem  22616  mbfadd  22617  mbfsub  22618  i1faddlem  22651  i1fmullem  22652  i1fres  22663  itg1climres  22672  mbfi1fseqlem4  22676  mbfmul  22684  itg2splitlem  22706  itg2split  22707  itgresr  22736  bddmulibl  22796  ellimc2  22832  ellimc3  22834  limcun  22850  dvreslem  22864  dvne0  22963  itgsubstlem  23000  ig1pval3  23126  ig1pval3OLD  23132  aaliou2  23296  aaliou2b  23297  pilem1  23406  rlimcnp2  23892  fsumharmonic  23937  ppisval2  24031  prmorcht  24105  fsumvma2  24142  pclogsum  24143  vmasum  24144  chpchtsum  24147  chpub  24148  chebbnd1lem1  24307  rpvmasum2  24350  tglineineq  24688  frgrancvvdeqlem4  25761  frgrancvvdeqlem7  25764  frgrancvvdeqlemA  25765  frgrancvvdeqlemC  25767  issubgo  26031  isexid2  26053  smgrpismgmOLD  26060  smgrpisass  26061  issmgrpOLD  26062  mndoissmgrpOLD  26067  mndoisexid  26068  ismndo  26071  rngo1cl  26157  minvecolem1  26516  minvecolem4a  26519  minvecolem4b  26520  minvecolem4  26522  minvecolem4aOLD  26529  minvecolem4bOLD  26530  minvecolem4OLD  26532  h2hcau  26632  axhcompl-zf  26651  hhcmpl  26853  hhcms  26856  ocin  26949  ocnel  26951  shmodsi  27042  pjhthlem2  27045  omlsilem  27055  pjoc1i  27084  spansnm0i  27303  nonbooli  27304  5oalem7  27313  3oalem3  27317  pjssmii  27334  mayete3i  27381  nmcopex  27682  nmcoplb  27683  lncnopbd  27690  nmcfnex  27706  nmcfnlb  27707  riesz4  27717  riesz1  27718  riesz2  27719  cnlnadjlem3  27722  cnlnadjlem5  27724  cnlnadjlem9  27728  cnlnadjeu  27731  rnbra  27760  pjimai  27829  pjclem4a  27851  pj3lem1  27859  jpi  27923  sumdmdii  28068  sumdmdlem  28071  sumdmdlem2  28072  cdjreui  28085  cdj3lem1  28087  iunin1f  28171  disjorf  28189  ofpreima  28268  1stpreima  28287  2ndpreima  28288  iocinioc2  28361  ssnnssfz  28367  isorng  28562  kerunit  28586  crefdf  28675  cmpcref  28677  cmppcmp  28685  pcmplfin  28687  cnre2csqima  28717  ordtconlem1  28730  lmxrge0  28758  isrrext  28804  esum0  28870  esumcst  28884  esumpcvgval  28899  esumcvg  28907  measvuni  29036  eulerpartlemt0  29202  eulerpartlemr  29207  eulerpartlemgf  29212  eulerpartlemgs2  29213  eulerpartlemn  29214  sseqf  29225  fiblem  29231  bnj521  29545  bnj1172  29810  bnj1173  29811  bnj1174  29812  bnj1279  29827  dfres3  30399  elima4  30421  dfon2lem4  30432  frrlem5  30518  ellimits  30677  dfom5b  30679  brapply  30705  brcap  30707  dfrecs2  30717  dfrdg4  30718  finminlem  30974  neibastop2lem  31016  neibastop2  31017  neifg  31027  tailfb  31033  onsucconi  31097  onintopsscon  31100  onsucsuccmpi  31103  limsucncmpi  31105  onint1  31109  bj-inrab  31530  bj-eldiag  31646  bj-eldiag2  31647  bj-ccinftydisj  31655  taupilem3  31720  isbasisrelowllem1  31758  isbasisrelowllem2  31759  ptrest  31939  poimirlem29  31969  poimirlem30  31970  mblfinlem2  31978  mbfposadd  31988  itg2gt0cn  31997  dvasin  32028  inixp  32055  0totbnd  32105  sstotbnd3  32108  heibor1lem  32141  heibor1  32142  heiborlem6  32148  exidresid  32177  isfld2  32238  prtlem14  32446  lshpdisj  32553  lkrin  32730  ishlat1  32918  pmodlem2  33412  pclfinN  33465  pclcmpatN  33466  osumcllem4N  33524  pexmidlem1N  33535  dihmeetlem1N  34858  dihglblem5apreN  34859  dihmeetlem4preN  34874  dihmeetlem13N  34887  dochnel2  34960  lcdlss  35187  mapd1o  35216  baerlem3lem2  35278  baerlem5alem2  35279  baerlem5blem2  35280  cmpfiiin  35539  mrefg2  35549  fz1eqin  35611  fnwe2lem2  35909  islmodfg  35927  islssfg2  35929  lnr2i  35975  acsfn1p  36065  subrgacs  36066  sdrgacs  36067  rp-fakeinunass  36160  fiinfi  36177  elinintab  36181  elinintrab  36183  elinlem  36204  cnvcnvintabd  36206  ndisj  36364  isprm7  36660  radcnvrat  36663  nzin  36667  onfrALTlem2  36912  onfrALTlem2VD  37286  elini  37380  inn0f  37417  iooabslt  37596  iccintsng  37624  lptioo2cn  37726  lptioo1cn  37727  cncfuni  37764  icccncfext  37765  stoweidlem44  37905  fourierdlem42  38012  fourierdlem42OLD  38013  fourierdlem80  38050  sge00  38218  eldmressn  38624  afvres  38674  rnghmval2  39948  rnghmsubcsetclem1  40030  rngccatidALTV  40044  funcrngcsetcALT  40054  zrinitorngc  40055  zrtermorngc  40056  rhmsubcsetclem1  40076  rhmsubcrngclem1  40082  ringcbasbas  40089  funcringcsetcALTV2lem7  40097  ringccatidALTV  40107  ringcbasbasALTV  40113  funcringcsetclem7ALTV  40120  irinitoringc  40124  zrtermoringc  40125  srhmsubclem1  40128  fldhmsubc  40139  srhmsubcALTVlem1  40147  fldhmsubcALTV  40158  rhmsubcALTVlem3  40162  ssnn0ssfz  40183  elbigo2  40416