Theorem elin 3650

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 3091	. 2 |- ( A e. ( B i^i C ) -> A e. _V )
2		elex 3091	. . 3 |- ( A e. C -> A e. _V )
3	2	adantl 468	. 2 |- ( ( A e. B /\ A e. C ) -> A e. _V )
4		eleq1 2495	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2495	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
6	4, 5	anbi12d 716	. . 3 |- ( x = A -> ( ( x e. B /\ x e. C ) <-> ( A e. B /\ A e. C ) ) )
7		df-in 3444	. . 3 |- ( B i^i C ) = { x | ( x e. B /\ x e. C ) }
8	6, 7	elab2g 3221	. 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 1438   e. wcel 1869   _Vcvv 3082   i^i cin 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-v 3084  df-in 3444

This theorem is referenced by:  elind  3651  elinel1  3652  elinel2  3653  elin2  3654  elin3  3655  incom  3656  ineqri  3657  ineq1  3658  inass  3673  inss1  3683  ssin  3685  ssrin  3688  dfss4  3708  difin  3711  indi  3720  undi  3721  unineq  3724  indifdir  3730  difin2  3736  inrab2  3747  inelcm  3848  difin0ss  3862  inssdif0  3863  inundif  3874  uniin  4237  intun  4286  intpr  4287  elrint  4295  iunin2  4361  iinin2  4367  elriin  4370  disjor  4406  disjiun  4412  brin  4471  trin  4526  inex1  4563  inuni  4584  wefrc  4845  inopab  4982  inxp  4984  dmin  5059  opelres  5127  eldmeldmressn  5162  intasym  5232  asymref  5233  dminss  5267  imainss  5268  inimasn  5270  ssrnres  5292  cnvresima  5341  dfco2a  5352  predel  5414  ordtri3or  5472  2elresin  5703  respreima  6022  fvcofneq  6043  tpres  6130  isomin  6241  isoini  6242  offval  6550  ordpwsuc  6654  ressuppss  6943  wfrlem5  7046  erdisj  7417  uniinqs  7449  mapval2  7507  ixpin  7553  boxriin  7570  disjen  7733  ssenen  7750  onfin2  7768  elfpw  7880  fiin  7940  inf3lem2  8138  epfrs  8218  cp  8365  bnd2  8367  dfac5lem1  8556  dfac5lem5  8560  dfac5  8561  kmlem3  8584  kmlem14  8595  kmlem15  8596  fin23lem26  8757  isfin1-3  8818  pwxpndom2  9092  ingru  9242  gruina  9245  grur1  9247  axgroth4  9259  grothprim  9261  ixxdisj  11652  icodisj  11759  fzdisj  11828  uzdisj  11869  nn0disj  11909  fzouzdisj  11956  xpcogend  13032  cotr2g  13034  limsupgle  13528  ello12  13573  elo12  13584  lo1resb  13621  rlimresb  13622  o1resb  13623  lo1eq  13625  rlimeq  13626  fsumsplit  13799  sumsplit  13822  fsum2dlem  13824  explecnv  13916  fprod2dlem  14027  bitsmod  14403  saddisjlem  14431  sadadd  14434  sadass  14438  smuval2  14449  smupval  14455  smueqlem  14457  smumul  14460  prmreclem5  14857  prmrec  14859  4sqlem12  14893  vdwmc  14921  acsfn  15558  iszeroo  15890  iszeroi  15897  isdrs2  16177  fpwipodrs  16403  psss  16453  subgacs  16845  nsgacs  16846  resscntz  16978  gsmsymgreq  17066  sylow2a  17264  lsmmod  17318  lsmdisj2  17325  gsumzsplit  17553  subgdmdprd  17660  dprdcntz2  17664  dprddisj2  17665  pgpfac1lem3  17703  isrhm  17942  subsubrg2  18028  lssacs  18183  lspdisj  18341  lspdisjb  18342  isassa  18532  aspid  18547  aspval2  18564  dfprm2  19057  ocvin  19229  unocv  19235  iunocv  19236  obselocv  19283  pmatcoe1fsupp  19717  isbasis2g  19955  tgval2  19963  tgcl  19977  ppttop  20014  epttop  20016  clsval2  20057  ssntr  20065  ntreq0  20085  isclo  20095  restntr  20190  restlp  20191  cnpresti  20296  cnprest  20297  cnprest2  20298  lmss  20306  haust1  20360  nrmsep3  20363  isnrm2  20366  lmmo  20388  fincmp  20400  0cmp  20401  discmp  20405  cmpsublem  20406  cmpsub  20407  uncmp  20410  hauscmplem  20413  dfcon2  20426  iunconlem  20434  uncon  20436  is1stc2  20449  1stcrest  20460  1stcelcls  20468  llyi  20481  nllyi  20482  subislly  20488  lly1stc  20503  comppfsc  20539  txcnp  20627  txcnmpt  20631  hausdiag  20652  kqcldsat  20740  ptcmpfi  20820  isfbas2  20842  isfil2  20863  fbasfip  20875  elfg  20878  filcon  20890  rnelfmlem  20959  rnelfm  20960  fmfnfmlem2  20962  fmfnfmlem4  20964  fmfnfm  20965  flimrest  20990  hauspwpwf1  20994  fclsrest  21031  alexsubALTlem2  21055  alexsubALTlem3  21056  alexsubALTlem4  21057  alexsubALT  21058  ptcmp  21065  istmd  21081  istgp  21084  tsmssubm  21149  tsmssplit  21158  istrg  21170  istdrg  21172  istlm  21191  ustfilxp  21219  utoptop  21241  utop3cls  21258  bldisj  21405  blin  21428  blin2  21436  blres  21438  lpbl  21510  metrest  21531  restmetu  21577  isngp  21602  isnlm  21670  isnmhm  21759  xrtgioo  21816  xrsmopn  21822  icccmplem2  21833  reconnlem2  21837  icoopnst  21959  iocopnst  21960  bndth  21978  iscph  22140  tchcph  22203  cfilfcls  22236  cmetcaulem  22250  cmetss  22276  isbn  22298  cldcss2  22388  hlhil  22389  ovolfcl  22411  ovolicc1  22461  ovolicc2lem2  22463  ovolicc2lem4OLD  22465  ovolicc2lem4  22466  ovolicc2lem5  22467  ovolicc2  22468  shftmbl  22484  volfiniun  22492  ioorf  22517  ioorfOLD  22522  mbfmax  22597  mbfimaopnlem  22603  mbfaddlem  22608  mbfadd  22609  mbfsub  22610  i1faddlem  22643  i1fmullem  22644  i1fres  22655  itg1climres  22664  mbfi1fseqlem4  22668  mbfmul  22676  itg2splitlem  22698  itg2split  22699  itgresr  22728  bddmulibl  22788  ellimc2  22824  ellimc3  22826  limcun  22842  dvreslem  22856  dvne0  22955  itgsubstlem  22992  ig1pval3  23118  ig1pval3OLD  23124  aaliou2  23288  aaliou2b  23289  pilem1  23398  rlimcnp2  23884  fsumharmonic  23929  ppisval2  24023  prmorcht  24097  fsumvma2  24134  pclogsum  24135  vmasum  24136  chpchtsum  24139  chpub  24140  chebbnd1lem1  24299  rpvmasum2  24342  tglineineq  24680  frgrancvvdeqlem4  25753  frgrancvvdeqlem7  25756  frgrancvvdeqlemA  25757  frgrancvvdeqlemC  25759  issubgo  26023  isexid2  26045  smgrpismgmOLD  26052  smgrpisass  26053  issmgrpOLD  26054  mndoissmgrpOLD  26059  mndoisexid  26060  ismndo  26063  rngo1cl  26149  minvecolem1  26508  minvecolem4a  26511  minvecolem4b  26512  minvecolem4  26514  minvecolem4aOLD  26521  minvecolem4bOLD  26522  minvecolem4OLD  26524  h2hcau  26624  axhcompl-zf  26643  hhcmpl  26845  hhcms  26848  ocin  26941  ocnel  26943  shmodsi  27034  pjhthlem2  27037  omlsilem  27047  pjoc1i  27076  spansnm0i  27295  nonbooli  27296  5oalem7  27305  3oalem3  27309  pjssmii  27326  mayete3i  27373  nmcopex  27674  nmcoplb  27675  lncnopbd  27682  nmcfnex  27698  nmcfnlb  27699  riesz4  27709  riesz1  27710  riesz2  27711  cnlnadjlem3  27714  cnlnadjlem5  27716  cnlnadjlem9  27720  cnlnadjeu  27723  rnbra  27752  pjimai  27821  pjclem4a  27843  pj3lem1  27851  jpi  27915  sumdmdii  28060  sumdmdlem  28063  sumdmdlem2  28064  cdjreui  28077  cdj3lem1  28079  elin1d  28146  elin2d  28147  iunin1f  28167  disjorf  28185  ofpreima  28264  1stpreima  28283  2ndpreima  28284  iocinioc2  28361  ssnnssfz  28367  isorng  28564  kerunit  28588  crefdf  28677  cmpcref  28679  cmppcmp  28687  pcmplfin  28689  cnre2csqima  28719  ordtconlem1  28732  lmxrge0  28760  isrrext  28806  esum0  28872  esumcst  28886  esumpcvgval  28901  esumcvg  28909  measvuni  29038  eulerpartlemt0  29204  eulerpartlemr  29209  eulerpartlemgf  29214  eulerpartlemgs2  29215  eulerpartlemn  29216  sseqf  29227  fiblem  29233  bnj521  29547  bnj1172  29812  bnj1173  29813  bnj1174  29814  bnj1279  29829  dfres3  30400  elima4  30422  dfon2lem4  30433  frrlem5  30519  ellimits  30676  dfom5b  30678  brapply  30704  brcap  30706  dfrecs2  30716  dfrdg4  30717  finminlem  30973  neibastop2lem  31015  neibastop2  31016  neifg  31026  tailfb  31032  onsucconi  31096  onintopsscon  31099  onsucsuccmpi  31102  limsucncmpi  31104  onint1  31108  bj-inrab  31493  bj-eldiag  31604  bj-eldiag2  31605  bj-ccinftydisj  31613  taupilem3  31678  isbasisrelowllem1  31716  isbasisrelowllem2  31717  ptrest  31897  poimirlem29  31927  poimirlem30  31928  mblfinlem2  31936  mbfposadd  31946  itg2gt0cn  31955  dvasin  31986  inixp  32013  0totbnd  32063  sstotbnd3  32066  heibor1lem  32099  heibor1  32100  heiborlem6  32106  exidresid  32135  isfld2  32196  prtlem14  32408  lshpdisj  32516  lkrin  32693  ishlat1  32881  pmodlem2  33375  pclfinN  33428  pclcmpatN  33429  osumcllem4N  33487  pexmidlem1N  33498  dihmeetlem1N  34821  dihglblem5apreN  34822  dihmeetlem4preN  34837  dihmeetlem13N  34850  dochnel2  34923  lcdlss  35150  mapd1o  35179  baerlem3lem2  35241  baerlem5alem2  35242  baerlem5blem2  35243  cmpfiiin  35502  mrefg2  35512  fz1eqin  35574  fnwe2lem2  35873  islmodfg  35891  islssfg2  35893  lnr2i  35939  acsfn1p  36029  subrgacs  36030  sdrgacs  36031  rp-fakeinunass  36124  fiinfi  36141  ndisj  36266  isprm7  36562  radcnvrat  36565  nzin  36569  onfrALTlem2  36814  onfrALTlem2VD  37191  elini  37285  iooabslt  37471  iccintsng  37499  lptioo2cn  37590  lptioo1cn  37591  cncfuni  37628  icccncfext  37629  stoweidlem44  37769  fourierdlem42  37876  fourierdlem42OLD  37877  fourierdlem80  37914  sge00  38050  eldmressn  38381  afvres  38430  rnghmval2  39237  rnghmsubcsetclem1  39319  rngccatidALTV  39333  funcrngcsetcALT  39343  zrinitorngc  39344  zrtermorngc  39345  rhmsubcsetclem1  39365  rhmsubcrngclem1  39371  ringcbasbas  39378  funcringcsetcALTV2lem7  39386  ringccatidALTV  39396  ringcbasbasALTV  39402  funcringcsetclem7ALTV  39409  irinitoringc  39413  zrtermoringc  39414  srhmsubclem1  39417  fldhmsubc  39428  srhmsubcALTVlem1  39436  fldhmsubcALTV  39447  rhmsubcALTVlem3  39451  ssnn0ssfz  39474  elbigo2  39707