Theorem elin 3527

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 2971	. 2 |- ( A e. ( B i^i C ) -> A e. _V )
2		elex 2971	. . 3 |- ( A e. C -> A e. _V )
3	2	adantl 463	. 2 |- ( ( A e. B /\ A e. C ) -> A e. _V )
4		eleq1 2493	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2493	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
6	4, 5	anbi12d 703	. . 3 |- ( x = A -> ( ( x e. B /\ x e. C ) <-> ( A e. B /\ A e. C ) ) )
7		df-in 3323	. . 3 |- ( B i^i C ) = { x | ( x e. B /\ x e. C ) }
8	6, 7	elab2g 3097	. 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 1362   e. wcel 1755   _Vcvv 2962   i^i cin 3315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-in 3323

This theorem is referenced by:  elind  3528  elin2  3529  elin3  3530  incom  3531  ineqri  3532  ineq1  3533  inass  3548  inss1  3558  ssin  3560  ssrin  3563  dfss4  3572  difin  3575  indi  3584  undi  3585  unineq  3588  indifdir  3594  difin2  3600  inrab2  3611  inelcm  3721  difin0ss  3733  inssdif0  3734  inundif  3745  uniin  4099  intun  4148  intpr  4149  elrint  4157  iunin2  4222  iinin2  4228  elriin  4231  disjor  4264  disjiun  4270  brin  4329  trin  4383  inex1  4421  inuni  4442  wefrc  4701  ordtri3or  4738  inopab  4957  inxp  4959  dmin  5034  opelres  5103  intasym  5201  asymref  5202  dminss  5239  imainss  5240  inimasn  5242  ssrnres  5264  cnvresima  5315  dfco2a  5326  2elresin  5510  respreima  5820  fvcofneq  5839  isomin  6015  isoini  6016  offval  6316  ordpwsuc  6415  ressuppss  6697  erdisj  7136  uniinqs  7168  mapval2  7230  ixpin  7276  boxriin  7293  disjen  7456  ssenen  7473  onfin2  7490  elfpw  7601  fiin  7660  inf3lem2  7823  epfrs  7939  cp  8086  bnd2  8088  dfac5lem1  8281  dfac5lem5  8285  dfac5  8286  kmlem3  8309  kmlem14  8320  kmlem15  8321  fin23lem26  8482  isfin1-3  8543  pwxpndom2  8820  ingru  8970  gruina  8973  grur1  8975  axgroth4  8987  grothprim  8989  ixxdisj  11303  icodisj  11397  fzdisj  11463  uzdisj  11515  fzouzdisj  11569  limsupgle  12939  ello12  12978  elo12  12989  lo1resb  13026  rlimresb  13027  o1resb  13028  lo1eq  13030  rlimeq  13031  fsumsplit  13200  sumsplit  13219  fsum2dlem  13221  explecnv  13310  bitsmod  13615  saddisjlem  13643  sadadd  13646  sadass  13650  smuval2  13661  smupval  13667  smueqlem  13669  smumul  13672  prmreclem5  13964  prmrec  13966  4sqlem12  14000  vdwmc  14022  acsfn  14580  isdrs2  15092  fpwipodrs  15317  psss  15367  subgacs  15696  nsgacs  15697  resscntz  15829  gsmsymgreq  15917  sylow2a  16098  lsmmod  16152  lsmdisj2  16159  gsumzsplit  16398  gsumzsplitOLD  16399  subgdmdprd  16505  dprdcntz2  16510  dprddisj2  16511  dprddisj2OLD  16512  pgpfac1lem3  16552  isrhm  16745  subsubrg2  16816  lssacs  16970  lspdisj  17128  lspdisjb  17129  isassa  17309  aspid  17323  aspval2  17339  dfprm2  17760  dfprm2OLD  17763  ocvin  17941  unocv  17947  iunocv  17948  obselocv  17995  isbasis2g  18395  tgval2  18403  tgcl  18416  ppttop  18453  epttop  18455  clsval2  18496  ssntr  18504  ntreq0  18523  isclo  18533  restntr  18628  restlp  18629  cnpresti  18734  cnprest  18735  cnprest2  18736  lmss  18744  haust1  18798  nrmsep3  18801  isnrm2  18804  lmmo  18826  fincmp  18838  0cmp  18839  discmp  18843  cmpsublem  18844  cmpsub  18845  uncmp  18848  hauscmplem  18851  bwthOLD  18856  dfcon2  18865  iunconlem  18873  uncon  18875  is1stc2  18888  1stcrest  18899  1stcelcls  18907  llyi  18920  nllyi  18921  subislly  18927  lly1stc  18942  txcnp  19035  txcnmpt  19039  hausdiag  19060  kqcldsat  19148  ptcmpfi  19228  isfbas2  19250  isfil2  19271  fbasfip  19283  elfg  19286  filcon  19298  rnelfmlem  19367  rnelfm  19368  fmfnfmlem2  19370  fmfnfmlem4  19372  fmfnfm  19373  flimrest  19398  hauspwpwf1  19402  fclsrest  19439  alexsubALTlem2  19462  alexsubALTlem3  19463  alexsubALTlem4  19464  alexsubALT  19465  ptcmp  19472  istmd  19487  istgp  19490  tsmssubm  19558  tsmssplit  19568  istrg  19580  istdrg  19582  istlm  19601  ustfilxp  19629  utoptop  19651  utop3cls  19668  bldisj  19815  blin  19838  blin2  19846  blres  19848  lpbl  19920  metrest  19941  restmetu  20004  isngp  20030  isnlm  20098  isnmhm  20167  xrtgioo  20225  xrsmopn  20231  icccmplem2  20242  reconnlem2  20246  icoopnst  20353  iocopnst  20354  bndth  20372  iscph  20531  tchcph  20594  cfilfcls  20627  cmetcaulem  20641  cmetss  20667  isbn  20691  cldcss2  20771  hlhil  20772  ovolfcl  20792  ovolicc1  20841  ovolicc2lem2  20843  ovolicc2lem4  20845  ovolicc2lem5  20846  ovolicc2  20847  shftmbl  20862  volfiniun  20870  ioorf  20895  mbfmax  20969  mbfimaopnlem  20975  mbfaddlem  20980  mbfadd  20981  mbfsub  20982  i1faddlem  21013  i1fmullem  21014  i1fres  21025  itg1climres  21034  mbfi1fseqlem4  21038  mbfmul  21046  itg2splitlem  21068  itg2split  21069  itgresr  21098  bddmulibl  21158  ellimc2  21194  ellimc3  21196  limcun  21212  dvreslem  21226  dvne0  21325  itgsubstlem  21362  ig1pval3  21531  aaliou2  21691  aaliou2b  21692  pilem1  21801  rlimcnp2  22245  fsumharmonic  22290  ppisval2  22327  prmorcht  22401  fsumvma2  22438  pclogsum  22439  vmasum  22440  chpchtsum  22443  chpub  22444  chebbnd1lem1  22603  rpvmasum2  22646  issubgo  23613  isexid2  23635  smgrpismgm  23642  smgrpisass  23643  issmgrp  23644  mndoissmgrp  23649  mndoisexid  23650  ismndo  23653  rngo1cl  23739  minvecolem1  24098  minvecolem4a  24101  minvecolem4b  24102  minvecolem4  24104  h2hcau  24204  axhcompl-zf  24223  hhcmpl  24425  hhcms  24428  ocin  24522  ocnel  24524  shmodsi  24615  pjhthlem2  24618  omlsilem  24628  pjoc1i  24657  spansnm0i  24876  nonbooli  24877  5oalem7  24886  3oalem3  24890  pjssmii  24907  mayete3i  24954  mayete3iOLD  24955  nmcopex  25256  nmcoplb  25257  lncnopbd  25264  nmcfnex  25280  nmcfnlb  25281  riesz4  25291  riesz1  25292  riesz2  25293  cnlnadjlem3  25296  cnlnadjlem5  25298  cnlnadjlem9  25302  cnlnadjeu  25305  rnbra  25334  pjimai  25403  pjclem4a  25425  pj3lem1  25433  jpi  25497  sumdmdii  25642  sumdmdlem  25645  sumdmdlem2  25646  cdjreui  25659  cdj3lem1  25661  disjorf  25747  ofpreima  25808  1stpreima  25825  2ndpreima  25826  iocinioc2  25892  ssnnssfz  25899  isorng  26120  kerunit  26144  cnre2csqima  26195  ordtconlem1  26208  lmxrge0  26236  isrrext  26283  esum0  26357  esumcst  26368  esumpcvgval  26381  esumcvg  26389  measvuni  26482  eulerpartlemt0  26600  eulerpartlemr  26605  eulerpartlemgf  26610  eulerpartlemgs2  26611  eulerpartlemn  26612  sseqf  26623  fiblem  26629  fprod2dlem  27338  dfres3  27416  elima4  27437  dfon2lem4  27446  predel  27491  wfrlem5  27575  frrlem5  27619  ellimits  27788  dfom5b  27790  brapply  27816  brcap  27818  dfrdg4  27828  tfrqfree  27829  onsucconi  28131  onintopsscon  28134  onsucsuccmpi  28137  limsucncmpi  28139  onint1  28143  ptrest  28269  mblfinlem2  28273  mbfposadd  28283  itg2gt0cn  28291  dvasin  28324  finminlem  28357  comppfsc  28423  neibastop2lem  28425  neibastop2  28426  neifg  28436  tailfb  28442  inixp  28466  0totbnd  28516  sstotbnd3  28519  heibor1lem  28552  heibor1  28553  heiborlem6  28559  exidresid  28588  isfld2  28649  prtlem14  28864  cmpfiiin  28878  mrefg2  28888  fz1eqin  28952  fnwe2lem2  29249  islmodfg  29267  islssfg2  29269  lnr2i  29317  acsfn1p  29401  subrgacs  29402  sdrgacs  29403  stoweidlem39  29680  stoweidlem44  29685  stoweidlem50  29691  stoweidlem57  29698  eldmressn  29873  afvres  29924  eldmeldmressn  29986  frgrancvvdeqlem4  30472  frgrancvvdeqlem7  30475  frgrancvvdeqlemA  30476  frgrancvvdeqlemC  30478  onfrALTlem2  30955  onfrALTlem2VD  31327  bnj521  31430  bnj1172  31694  bnj1173  31695  bnj1174  31696  bnj1279  31711  bj-inrab  32016  bj-eldiag  32106  bj-ccinftydisj  32116  lshpdisj  32205  lkrin  32382  ishlat1  32570  pmodlem2  33064  pclfinN  33117  pclcmpatN  33118  osumcllem4N  33176  pexmidlem1N  33187  dihmeetlem1N  34508  dihglblem5apreN  34509  dihmeetlem4preN  34524  dihmeetlem13N  34537  dochnel2  34610  lcdlss  34837  mapd1o  34866  baerlem3lem2  34928  baerlem5alem2  34929  baerlem5blem2  34930  taupilem3  35185