Theorem elin 3673

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 3115	. 2 |- ( A e. ( B i^i C ) -> A e. _V )
2		elex 3115	. . 3 |- ( A e. C -> A e. _V )
3	2	adantl 464	. 2 |- ( ( A e. B /\ A e. C ) -> A e. _V )
4		eleq1 2526	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2526	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
6	4, 5	anbi12d 708	. . 3 |- ( x = A -> ( ( x e. B /\ x e. C ) <-> ( A e. B /\ A e. C ) ) )
7		df-in 3468	. . 3 |- ( B i^i C ) = { x | ( x e. B /\ x e. C ) }
8	6, 7	elab2g 3245	. 2 |- ( A e. _V -> ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) ) )
9	1, 3, 8	pm5.21nii 351	1 |- ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) )

Syntax hints:   <-> wb 184   /\ wa 367   = wceq 1398   e. wcel 1823   _Vcvv 3106   i^i cin 3460

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-in 3468

This theorem is referenced by:  elind  3674  elin2  3675  elin3  3676  incom  3677  ineqri  3678  ineq1  3679  inass  3694  inss1  3704  ssin  3706  ssrin  3709  dfss4  3729  difin  3732  indi  3741  undi  3742  unineq  3745  indifdir  3751  difin2  3757  inrab2  3768  inelcm  3869  difin0ss  3882  inssdif0  3883  inundif  3894  uniin  4255  intun  4304  intpr  4305  elrint  4313  iunin2  4379  iinin2  4385  elriin  4388  disjor  4424  disjiun  4430  brin  4488  trin  4542  inex1  4578  inuni  4599  wefrc  4862  ordtri3or  4899  inopab  5122  inxp  5124  dmin  5199  opelres  5267  eldmeldmressn  5302  intasym  5370  asymref  5371  dminss  5405  imainss  5406  inimasn  5408  ssrnres  5430  cnvresima  5479  dfco2a  5490  2elresin  5674  respreima  5992  fvcofneq  6015  tpres  6100  isomin  6208  isoini  6209  offval  6520  ordpwsuc  6623  ressuppss  6911  erdisj  7351  uniinqs  7383  mapval2  7441  ixpin  7487  boxriin  7504  disjen  7667  ssenen  7684  onfin2  7702  elfpw  7814  fiin  7874  inf3lem2  8037  epfrs  8153  cp  8300  bnd2  8302  dfac5lem1  8495  dfac5lem5  8499  dfac5  8500  kmlem3  8523  kmlem14  8534  kmlem15  8535  fin23lem26  8696  isfin1-3  8757  pwxpndom2  9032  ingru  9182  gruina  9185  grur1  9187  axgroth4  9199  grothprim  9201  ixxdisj  11547  icodisj  11648  fzdisj  11715  uzdisj  11755  nn0disj  11795  fzouzdisj  11838  xpcogend  12892  cotr2g  12894  limsupgle  13382  ello12  13421  elo12  13432  lo1resb  13469  rlimresb  13470  o1resb  13471  lo1eq  13473  rlimeq  13474  fsumsplit  13644  sumsplit  13665  fsum2dlem  13667  explecnv  13758  fprod2dlem  13866  bitsmod  14170  saddisjlem  14198  sadadd  14201  sadass  14205  smuval2  14216  smupval  14222  smueqlem  14224  smumul  14227  prmreclem5  14522  prmrec  14524  4sqlem12  14558  vdwmc  14580  acsfn  15148  iszeroo  15480  iszeroi  15487  isdrs2  15767  fpwipodrs  15993  psss  16043  subgacs  16435  nsgacs  16436  resscntz  16568  gsmsymgreq  16656  sylow2a  16838  lsmmod  16892  lsmdisj2  16899  gsumzsplit  17143  gsumzsplitOLD  17144  subgdmdprd  17276  dprdcntz2  17281  dprddisj2  17282  dprddisj2OLD  17283  pgpfac1lem3  17323  isrhm  17565  subsubrg2  17651  lssacs  17808  lspdisj  17966  lspdisjb  17967  isassa  18159  aspid  18174  aspval2  18191  dfprm2  18706  ocvin  18878  unocv  18884  iunocv  18885  obselocv  18932  pmatcoe1fsupp  19369  isbasis2g  19616  tgval2  19624  tgcl  19638  ppttop  19675  epttop  19677  clsval2  19718  ssntr  19726  ntreq0  19745  isclo  19755  restntr  19850  restlp  19851  cnpresti  19956  cnprest  19957  cnprest2  19958  lmss  19966  haust1  20020  nrmsep3  20023  isnrm2  20026  lmmo  20048  fincmp  20060  0cmp  20061  discmp  20065  cmpsublem  20066  cmpsub  20067  uncmp  20070  hauscmplem  20073  dfcon2  20086  iunconlem  20094  uncon  20096  is1stc2  20109  1stcrest  20120  1stcelcls  20128  llyi  20141  nllyi  20142  subislly  20148  lly1stc  20163  comppfsc  20199  txcnp  20287  txcnmpt  20291  hausdiag  20312  kqcldsat  20400  ptcmpfi  20480  isfbas2  20502  isfil2  20523  fbasfip  20535  elfg  20538  filcon  20550  rnelfmlem  20619  rnelfm  20620  fmfnfmlem2  20622  fmfnfmlem4  20624  fmfnfm  20625  flimrest  20650  hauspwpwf1  20654  fclsrest  20691  alexsubALTlem2  20714  alexsubALTlem3  20715  alexsubALTlem4  20716  alexsubALT  20717  ptcmp  20724  istmd  20739  istgp  20742  tsmssubm  20810  tsmssplit  20820  istrg  20832  istdrg  20834  istlm  20853  ustfilxp  20881  utoptop  20903  utop3cls  20920  bldisj  21067  blin  21090  blin2  21098  blres  21100  lpbl  21172  metrest  21193  restmetu  21256  isngp  21282  isnlm  21350  isnmhm  21419  xrtgioo  21477  xrsmopn  21483  icccmplem2  21494  reconnlem2  21498  icoopnst  21605  iocopnst  21606  bndth  21624  iscph  21783  tchcph  21846  cfilfcls  21879  cmetcaulem  21893  cmetss  21919  isbn  21943  cldcss2  22023  hlhil  22024  ovolfcl  22044  ovolicc1  22093  ovolicc2lem2  22095  ovolicc2lem4  22097  ovolicc2lem5  22098  ovolicc2  22099  shftmbl  22115  volfiniun  22123  ioorf  22148  mbfmax  22222  mbfimaopnlem  22228  mbfaddlem  22233  mbfadd  22234  mbfsub  22235  i1faddlem  22266  i1fmullem  22267  i1fres  22278  itg1climres  22287  mbfi1fseqlem4  22291  mbfmul  22299  itg2splitlem  22321  itg2split  22322  itgresr  22351  bddmulibl  22411  ellimc2  22447  ellimc3  22449  limcun  22465  dvreslem  22479  dvne0  22578  itgsubstlem  22615  ig1pval3  22741  aaliou2  22902  aaliou2b  22903  pilem1  23012  rlimcnp2  23494  fsumharmonic  23539  ppisval2  23576  prmorcht  23650  fsumvma2  23687  pclogsum  23688  vmasum  23689  chpchtsum  23692  chpub  23693  chebbnd1lem1  23852  rpvmasum2  23895  tglineineq  24224  frgrancvvdeqlem4  25235  frgrancvvdeqlem7  25238  frgrancvvdeqlemA  25239  frgrancvvdeqlemC  25241  issubgo  25503  isexid2  25525  smgrpismgmOLD  25532  smgrpisass  25533  issmgrpOLD  25534  mndoissmgrpOLD  25539  mndoisexid  25540  ismndo  25543  rngo1cl  25629  minvecolem1  25988  minvecolem4a  25991  minvecolem4b  25992  minvecolem4  25994  h2hcau  26094  axhcompl-zf  26113  hhcmpl  26315  hhcms  26318  ocin  26412  ocnel  26414  shmodsi  26505  pjhthlem2  26508  omlsilem  26518  pjoc1i  26547  spansnm0i  26766  nonbooli  26767  5oalem7  26776  3oalem3  26780  pjssmii  26797  mayete3i  26844  mayete3iOLD  26845  nmcopex  27146  nmcoplb  27147  lncnopbd  27154  nmcfnex  27170  nmcfnlb  27171  riesz4  27181  riesz1  27182  riesz2  27183  cnlnadjlem3  27186  cnlnadjlem5  27188  cnlnadjlem9  27192  cnlnadjeu  27195  rnbra  27224  pjimai  27293  pjclem4a  27315  pj3lem1  27323  jpi  27387  sumdmdii  27532  sumdmdlem  27535  sumdmdlem2  27536  cdjreui  27549  cdj3lem1  27551  elin1d  27617  elin2d  27618  iunin1f  27633  disjorf  27650  ofpreima  27734  1stpreima  27753  2ndpreima  27754  iocinioc2  27824  ssnnssfz  27831  isorng  28024  kerunit  28048  crefdf  28086  cmpcref  28088  cmppcmp  28096  pcmplfin  28098  cnre2csqima  28128  ordtconlem1  28141  lmxrge0  28169  isrrext  28215  esum0  28278  esumcst  28292  esumpcvgval  28307  esumcvg  28315  measvuni  28422  eulerpartlemt0  28572  eulerpartlemr  28577  eulerpartlemgf  28582  eulerpartlemgs2  28583  eulerpartlemn  28584  sseqf  28595  fiblem  28601  dfres3  29429  elima4  29449  dfon2lem4  29458  predel  29503  wfrlem5  29587  frrlem5  29631  ellimits  29788  dfom5b  29790  brapply  29816  brcap  29818  dfrdg4  29828  tfrqfree  29829  onsucconi  30130  onintopsscon  30133  onsucsuccmpi  30136  limsucncmpi  30138  onint1  30142  ptrest  30288  mblfinlem2  30292  mbfposadd  30302  itg2gt0cn  30310  dvasin  30343  finminlem  30376  neibastop2lem  30418  neibastop2  30419  neifg  30429  tailfb  30435  inixp  30459  0totbnd  30509  sstotbnd3  30512  heibor1lem  30545  heibor1  30546  heiborlem6  30552  exidresid  30581  isfld2  30642  prtlem14  30855  cmpfiiin  30869  mrefg2  30879  fz1eqin  30941  fnwe2lem2  31236  islmodfg  31254  islssfg2  31256  lnr2i  31306  acsfn1p  31389  subrgacs  31390  sdrgacs  31391  isprm7  31433  radcnvrat  31436  nzin  31464  elinel2  31663  elinel1  31664  iooabslt  31771  iccintsng  31802  lptioo2cn  31890  lptioo1cn  31891  cncfuni  31928  icccncfext  31929  stoweidlem44  32065  fourierdlem42  32170  fourierdlem80  32208  eldmressn  32447  afvres  32496  rnghmval2  32955  rnghmsubcsetclem1  33037  rngccatidALTV  33051  funcrngcsetcALT  33061  zrinitorngc  33062  zrtermorngc  33063  rhmsubcsetclem1  33083  rhmsubcrngclem1  33089  ringcbasbas  33096  funcringcsetcALTV2lem7  33104  ringccatidALTV  33114  ringcbasbasALTV  33120  funcringcsetclem7ALTV  33127  irinitoringc  33131  zrtermoringc  33132  srhmsubclem1  33135  fldhmsubc  33146  srhmsubcALTVlem1  33154  fldhmsubcALTV  33165  rhmsubcALTVlem3  33169  ssnn0ssfz  33192  elbigo2  33427  onfrALTlem2  33712  onfrALTlem2VD  34090  bnj521  34193  bnj1172  34458  bnj1173  34459  bnj1174  34460  bnj1279  34475  bj-inrab  34896  bj-eldiag  35007  bj-eldiag2  35008  bj-ccinftydisj  35016  lshpdisj  35109  lkrin  35286  ishlat1  35474  pmodlem2  35968  pclfinN  36021  pclcmpatN  36022  osumcllem4N  36080  pexmidlem1N  36091  dihmeetlem1N  37414  dihglblem5apreN  37415  dihmeetlem4preN  37430  dihmeetlem13N  37443  dochnel2  37516  lcdlss  37743  mapd1o  37772  baerlem3lem2  37834  baerlem5alem2  37835  baerlem5blem2  37836  taupilem3  38091  rp-fakeinunass  38154  fiinfi  38171  ndisj  38243