Theorem elin 3560

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 3002	. 2 |- ( A e. ( B i^i C ) -> A e. _V )
2		elex 3002	. . 3 |- ( A e. C -> A e. _V )
3	2	adantl 466	. 2 |- ( ( A e. B /\ A e. C ) -> A e. _V )
4		eleq1 2503	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2503	. . . 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 3356	. . 3 |- ( B i^i C ) = { x | ( x e. B /\ x e. C ) }
8	6, 7	elab2g 3129	. 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 1369   e. wcel 1756   _Vcvv 2993   i^i cin 3348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2995  df-in 3356

This theorem is referenced by:  elind  3561  elin2  3562  elin3  3563  incom  3564  ineqri  3565  ineq1  3566  inass  3581  inss1  3591  ssin  3593  ssrin  3596  dfss4  3605  difin  3608  indi  3617  undi  3618  unineq  3621  indifdir  3627  difin2  3633  inrab2  3644  inelcm  3754  difin0ss  3766  inssdif0  3767  inundif  3778  uniin  4132  intun  4181  intpr  4182  elrint  4190  iunin2  4255  iinin2  4261  elriin  4264  disjor  4297  disjiun  4303  brin  4362  trin  4416  inex1  4454  inuni  4475  wefrc  4735  ordtri3or  4772  inopab  4991  inxp  4993  dmin  5068  opelres  5137  intasym  5234  asymref  5235  dminss  5272  imainss  5273  inimasn  5275  ssrnres  5297  cnvresima  5348  dfco2a  5359  2elresin  5543  respreima  5853  fvcofneq  5872  isomin  6049  isoini  6050  offval  6348  ordpwsuc  6447  ressuppss  6729  erdisj  7169  uniinqs  7201  mapval2  7263  ixpin  7309  boxriin  7326  disjen  7489  ssenen  7506  onfin2  7523  elfpw  7634  fiin  7693  inf3lem2  7856  epfrs  7972  cp  8119  bnd2  8121  dfac5lem1  8314  dfac5lem5  8318  dfac5  8319  kmlem3  8342  kmlem14  8353  kmlem15  8354  fin23lem26  8515  isfin1-3  8576  pwxpndom2  8853  ingru  9003  gruina  9006  grur1  9008  axgroth4  9020  grothprim  9022  ixxdisj  11336  icodisj  11431  fzdisj  11497  uzdisj  11552  fzouzdisj  11606  limsupgle  12976  ello12  13015  elo12  13026  lo1resb  13063  rlimresb  13064  o1resb  13065  lo1eq  13067  rlimeq  13068  fsumsplit  13237  sumsplit  13256  fsum2dlem  13258  explecnv  13348  bitsmod  13653  saddisjlem  13681  sadadd  13684  sadass  13688  smuval2  13699  smupval  13705  smueqlem  13707  smumul  13710  prmreclem5  14002  prmrec  14004  4sqlem12  14038  vdwmc  14060  acsfn  14618  isdrs2  15130  fpwipodrs  15355  psss  15405  subgacs  15737  nsgacs  15738  resscntz  15870  gsmsymgreq  15958  sylow2a  16139  lsmmod  16193  lsmdisj2  16200  gsumzsplit  16439  gsumzsplitOLD  16440  subgdmdprd  16553  dprdcntz2  16558  dprddisj2  16559  dprddisj2OLD  16560  pgpfac1lem3  16600  isrhm  16833  subsubrg2  16914  lssacs  17070  lspdisj  17228  lspdisjb  17229  isassa  17409  aspid  17423  aspval2  17439  dfprm2  17940  dfprm2OLD  17943  ocvin  18121  unocv  18127  iunocv  18128  obselocv  18175  isbasis2g  18575  tgval2  18583  tgcl  18596  ppttop  18633  epttop  18635  clsval2  18676  ssntr  18684  ntreq0  18703  isclo  18713  restntr  18808  restlp  18809  cnpresti  18914  cnprest  18915  cnprest2  18916  lmss  18924  haust1  18978  nrmsep3  18981  isnrm2  18984  lmmo  19006  fincmp  19018  0cmp  19019  discmp  19023  cmpsublem  19024  cmpsub  19025  uncmp  19028  hauscmplem  19031  bwthOLD  19036  dfcon2  19045  iunconlem  19053  uncon  19055  is1stc2  19068  1stcrest  19079  1stcelcls  19087  llyi  19100  nllyi  19101  subislly  19107  lly1stc  19122  txcnp  19215  txcnmpt  19219  hausdiag  19240  kqcldsat  19328  ptcmpfi  19408  isfbas2  19430  isfil2  19451  fbasfip  19463  elfg  19466  filcon  19478  rnelfmlem  19547  rnelfm  19548  fmfnfmlem2  19550  fmfnfmlem4  19552  fmfnfm  19553  flimrest  19578  hauspwpwf1  19582  fclsrest  19619  alexsubALTlem2  19642  alexsubALTlem3  19643  alexsubALTlem4  19644  alexsubALT  19645  ptcmp  19652  istmd  19667  istgp  19670  tsmssubm  19738  tsmssplit  19748  istrg  19760  istdrg  19762  istlm  19781  ustfilxp  19809  utoptop  19831  utop3cls  19848  bldisj  19995  blin  20018  blin2  20026  blres  20028  lpbl  20100  metrest  20121  restmetu  20184  isngp  20210  isnlm  20278  isnmhm  20347  xrtgioo  20405  xrsmopn  20411  icccmplem2  20422  reconnlem2  20426  icoopnst  20533  iocopnst  20534  bndth  20552  iscph  20711  tchcph  20774  cfilfcls  20807  cmetcaulem  20821  cmetss  20847  isbn  20871  cldcss2  20951  hlhil  20952  ovolfcl  20972  ovolicc1  21021  ovolicc2lem2  21023  ovolicc2lem4  21025  ovolicc2lem5  21026  ovolicc2  21027  shftmbl  21042  volfiniun  21050  ioorf  21075  mbfmax  21149  mbfimaopnlem  21155  mbfaddlem  21160  mbfadd  21161  mbfsub  21162  i1faddlem  21193  i1fmullem  21194  i1fres  21205  itg1climres  21214  mbfi1fseqlem4  21218  mbfmul  21226  itg2splitlem  21248  itg2split  21249  itgresr  21278  bddmulibl  21338  ellimc2  21374  ellimc3  21376  limcun  21392  dvreslem  21406  dvne0  21505  itgsubstlem  21542  ig1pval3  21668  aaliou2  21828  aaliou2b  21829  pilem1  21938  rlimcnp2  22382  fsumharmonic  22427  ppisval2  22464  prmorcht  22538  fsumvma2  22575  pclogsum  22576  vmasum  22577  chpchtsum  22580  chpub  22581  chebbnd1lem1  22740  rpvmasum2  22783  tglineineq  23070  footex  23131  issubgo  23812  isexid2  23834  smgrpismgm  23841  smgrpisass  23842  issmgrp  23843  mndoissmgrp  23848  mndoisexid  23849  ismndo  23852  rngo1cl  23938  minvecolem1  24297  minvecolem4a  24300  minvecolem4b  24301  minvecolem4  24303  h2hcau  24403  axhcompl-zf  24422  hhcmpl  24624  hhcms  24627  ocin  24721  ocnel  24723  shmodsi  24814  pjhthlem2  24817  omlsilem  24827  pjoc1i  24856  spansnm0i  25075  nonbooli  25076  5oalem7  25085  3oalem3  25089  pjssmii  25106  mayete3i  25153  mayete3iOLD  25154  nmcopex  25455  nmcoplb  25456  lncnopbd  25463  nmcfnex  25479  nmcfnlb  25480  riesz4  25490  riesz1  25491  riesz2  25492  cnlnadjlem3  25495  cnlnadjlem5  25497  cnlnadjlem9  25501  cnlnadjeu  25504  rnbra  25533  pjimai  25602  pjclem4a  25624  pj3lem1  25632  jpi  25696  sumdmdii  25841  sumdmdlem  25844  sumdmdlem2  25845  cdjreui  25858  cdj3lem1  25860  disjorf  25945  ofpreima  26006  1stpreima  26023  2ndpreima  26024  iocinioc2  26091  ssnnssfz  26098  isorng  26289  kerunit  26313  cnre2csqima  26363  ordtconlem1  26376  lmxrge0  26404  isrrext  26451  esum0  26525  esumcst  26536  esumpcvgval  26549  esumcvg  26557  measvuni  26650  eulerpartlemt0  26774  eulerpartlemr  26779  eulerpartlemgf  26784  eulerpartlemgs2  26785  eulerpartlemn  26786  sseqf  26797  fiblem  26803  fprod2dlem  27513  dfres3  27591  elima4  27612  dfon2lem4  27621  predel  27666  wfrlem5  27750  frrlem5  27794  ellimits  27963  dfom5b  27965  brapply  27991  brcap  27993  dfrdg4  28003  tfrqfree  28004  onsucconi  28305  onintopsscon  28308  onsucsuccmpi  28311  limsucncmpi  28313  onint1  28317  ptrest  28451  mblfinlem2  28455  mbfposadd  28465  itg2gt0cn  28473  dvasin  28506  finminlem  28539  comppfsc  28605  neibastop2lem  28607  neibastop2  28608  neifg  28618  tailfb  28624  inixp  28648  0totbnd  28698  sstotbnd3  28701  heibor1lem  28734  heibor1  28735  heiborlem6  28741  exidresid  28770  isfld2  28831  prtlem14  29045  cmpfiiin  29059  mrefg2  29069  fz1eqin  29133  fnwe2lem2  29430  islmodfg  29448  islssfg2  29450  lnr2i  29498  acsfn1p  29582  subrgacs  29583  sdrgacs  29584  stoweidlem39  29860  stoweidlem44  29865  stoweidlem50  29871  stoweidlem57  29878  eldmressn  30053  afvres  30104  eldmeldmressn  30166  frgrancvvdeqlem4  30652  frgrancvvdeqlem7  30655  frgrancvvdeqlemA  30656  frgrancvvdeqlemC  30658  nn0disj  30765  ssnn0ssfz  30770  pmatcoe1fsupp  31107  onfrALTlem2  31350  onfrALTlem2VD  31721  bnj521  31824  bnj1172  32088  bnj1173  32089  bnj1174  32090  bnj1279  32105  bj-inrab  32526  bj-eldiag  32622  bj-ccinftydisj  32632  lshpdisj  32728  lkrin  32905  ishlat1  33093  pmodlem2  33587  pclfinN  33640  pclcmpatN  33641  osumcllem4N  33699  pexmidlem1N  33710  dihmeetlem1N  35031  dihglblem5apreN  35032  dihmeetlem4preN  35047  dihmeetlem13N  35060  dochnel2  35133  lcdlss  35360  mapd1o  35389  baerlem3lem2  35451  baerlem5alem2  35452  baerlem5blem2  35453  taupilem3  35708