Theorem elin 3897

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	⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Proof of Theorem elin

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3459	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 3459	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	adantl 485	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2877	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
5		eleq1 2877	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐶 ↔ 𝑦 ∈ 𝐶))
6	4, 5	anbi12d 633	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
7		eleq1 2877	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
8		eleq1 2877	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
9	7, 8	anbi12d 633	. . 3 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
10		df-in 3888	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
11	6, 9, 10	elab2gw 3613	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
12	1, 3, 11	pm5.21nii 383	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  Vcvv 3441   ∩ cin 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888

This theorem is referenced by:  dfss2  3901  elini  4120  elind  4121  elinel1  4122  elinel2  4123  elin2  4124  elin3  4127  incomOLD  4129  ineqri  4130  ineq1OLD  4132  inass  4146  ssin  4157  ssrin  4160  rexin  4166  dfss4  4185  difin  4188  indi  4200  undi  4201  unineq  4204  indifdir  4210  difin2  4216  inrab2  4228  ndisj  4281  difin0ss  4282  inssdif0  4283  inelcm  4372  inundif  4385  elinsn  4606  uniin  4824  intun  4870  intpr  4871  elrint  4879  iunin2  4956  iinin2  4963  elriin  4966  disjor  5010  disjiun  5017  brin  5082  trin  5146  inex1  5185  inuni  5210  wefrc  5513  inopab  5665  inxp  5667  dmin  5744  dfres3  5823  intasym  5942  asymref  5943  dminss  5977  imainss  5978  inimasn  5980  cnvresima  6054  dfco2a  6066  ordtri3or  6191  2elresin  6440  respreima  6813  fvcofneq  6836  tpres  6940  isomin  7069  isoini  7070  offval  7396  ordpwsuc  7510  ressuppss  7832  wfrlem5  7942  uniinqs  8360  mapval2  8419  ixpin  8470  boxriin  8487  disjen  8658  ssenen  8675  onfin2  8695  elfpw  8810  fiin  8870  inf3lem2  9076  epfrs  9157  cp  9304  dfac5lem1  9534  dfac5lem5  9538  dfac5  9539  kmlem3  9563  kmlem14  9574  kmlem15  9575  fin23lem26  9736  pwxpndom2  10076  ingru  10226  gruina  10229  grur1  10231  axgroth4  10243  grothprim  10245  ixxdisj  12741  icodisj  12854  fzdisj  12929  nn0disj  13018  fzouzdisj  13068  cotr2g  14327  limsupgle  14826  ello12  14865  elo12  14876  lo1resb  14913  rlimresb  14914  o1resb  14915  lo1eq  14917  rlimeq  14918  fsumsplit  15089  sumsplit  15115  fsum2dlem  15117  fprod2dlem  15326  bitsmod  15775  saddisjlem  15803  sadadd  15806  sadass  15810  smuval2  15821  smupval  15827  smueqlem  15829  smumul  15832  isprm7  16042  prmreclem5  16246  prmrec  16248  4sqlem12  16282  vdwmc  16304  setsstruct2  16513  acsfn  16922  iszeroo  17254  iszeroi  17261  fpwipodrs  17766  psss  17816  insubm  17975  subgacs  18305  nsgacs  18306  resscntz  18454  gsmsymgreq  18552  sylow2a  18736  lsmmod  18793  lsmdisj2  18800  gsumzsplit  19040  subgdmdprd  19149  dprdcntz2  19153  dprddisj2  19154  pgpfac1lem3  19192  isrhm  19469  subsubrg2  19555  acsfn1p  19571  subrgacs  19572  sdrgacs  19573  lssacs  19732  lspdisj  19890  lspdisjb  19891  dfprm2  20187  ocvin  20363  unocv  20369  iunocv  20370  obselocv  20417  isassa  20545  aspid  20561  aspval2  20584  pmatcoe1fsupp  21306  isbasis2g  21553  tgval2  21561  tgcl  21574  ppttop  21612  epttop  21614  ssntr  21663  ntreq0  21682  isclo  21692  restntr  21787  restlp  21788  cnpresti  21893  cnprest  21894  cnprest2  21895  lmss  21903  haust1  21957  nrmsep3  21960  isnrm2  21963  lmmo  21985  fincmp  21998  cmpsublem  22004  cmpsub  22005  uncmp  22008  hauscmplem  22011  dfconn2  22024  iunconnlem  22032  unconn  22034  is1stc2  22047  1stcrest  22058  1stcelcls  22066  llyi  22079  nllyi  22080  subislly  22086  lly1stc  22101  txcnp  22225  txcnmpt  22229  hausdiag  22250  kqcldsat  22338  isfbas2  22440  isfil2  22461  fbasfip  22473  elfg  22476  filconn  22488  rnelfmlem  22557  rnelfm  22558  fmfnfmlem2  22560  fmfnfmlem4  22562  fmfnfm  22563  flimrest  22588  hauspwpwf1  22592  fclsrest  22629  alexsubALTlem2  22653  alexsubALTlem3  22654  alexsubALTlem4  22655  alexsubALT  22656  istmd  22679  istgp  22682  tsmssubm  22748  tsmssplit  22757  istrg  22769  istdrg  22771  istlm  22790  ustfilxp  22818  utoptop  22840  utop3cls  22857  bldisj  23005  blin  23028  blres  23038  lpbl  23110  metrest  23131  restmetu  23177  isngp  23202  isnlm  23281  isnmhm  23352  xrtgioo  23411  xrsmopn  23417  icccmplem2  23428  reconnlem2  23432  icoopnst  23544  iocopnst  23545  bndth  23563  zclmncvs  23753  isncvsngp  23754  ncvsprp  23757  ncvsm1  23759  ncvsdif  23760  ncvspi  23761  ncvs1  23762  ncvspds  23766  iscph  23775  tcphcph  23841  cfilfcls  23878  cmetcaulem  23892  isbn  23942  cldcss2  24046  hlhil  24047  ovolfcl  24070  ovolicc2lem2  24122  ovolicc2  24126  shftmbl  24142  volfiniun  24151  mbfmax  24253  mbfimaopnlem  24259  mbfaddlem  24264  i1faddlem  24297  i1fmullem  24298  i1fres  24309  itg1climres  24318  mbfi1fseqlem4  24322  itg2splitlem  24352  itg2split  24353  itgresr  24382  ellimc2  24480  ellimc3  24482  limcun  24498  dvreslem  24512  dvne0  24614  itgsubstlem  24651  ig1pval3  24775  aaliou2  24936  aaliou2b  24937  pilem1  25046  rlimcnp2  25552  fsumharmonic  25597  ppisval2  25690  prmorcht  25763  fsumvma2  25798  pclogsum  25799  vmasum  25800  chpchtsum  25803  chpub  25804  rpvmasum2  26096  tglineineq  26437  trlsegvdeg  28012  frgrncvvdeqlem7  28090  frgrncvvdeqlem9  28092  minvecolem1  28657  minvecolem4a  28660  minvecolem4b  28661  minvecolem4  28663  h2hcau  28762  axhcompl-zf  28781  hhcmpl  28983  hhcms  28986  ocin  29079  ocnel  29081  shmodsi  29172  pjhthlem2  29175  omlsilem  29185  pjoc1i  29214  spansnm0i  29433  nonbooli  29434  5oalem7  29443  3oalem3  29447  pjssmii  29464  mayete3i  29511  nmcopex  29812  nmcoplb  29813  lncnopbd  29820  nmcfnex  29836  nmcfnlb  29837  riesz4  29847  riesz1  29848  riesz2  29849  cnlnadjlem3  29852  cnlnadjlem5  29854  cnlnadjlem9  29858  cnlnadjeu  29861  rnbra  29890  pjimai  29959  pjclem4a  29981  pj3lem1  29989  jpi  30053  sumdmdii  30198  sumdmdlem  30201  sumdmdlem2  30202  cdjreui  30215  cdj3lem1  30217  iunin1f  30321  disjorf  30342  ofpreima  30428  1stpreima  30466  2ndpreima  30467  iocinioc2  30528  ssnnssfz  30536  cntzun  30745  isorng  30923  kerunit  30947  prmidl0  31034  ccfldextdgrr  31145  crefdf  31201  cmpcref  31203  cmppcmp  31211  cnre2csqima  31264  ordtconnlem1  31277  lmxrge0  31305  isrrext  31351  esum0  31418  esumcst  31432  esumpcvgval  31447  esumcvg  31455  measvuni  31583  eulerpartlemt0  31737  eulerpartlemr  31742  eulerpartlemgf  31747  eulerpartlemgs2  31748  eulerpartlemn  31749  fiblem  31766  oddprm2  32036  bnj521  32117  bnj1173  32384  bnj1174  32385  bnj1279  32400  elima4  33132  dfon2lem4  33144  frrlem13  33248  fprlem1  33250  madeval2  33403  ellimits  33484  dfom5b  33486  brapply  33512  brcap  33514  dfrecs2  33524  dfrdg4  33525  finminlem  33779  neibastop2lem  33821  neibastop2  33822  neifg  33832  tailfb  33838  onsucconni  33898  onintopssconn  33901  onsucsuccmpi  33904  limsucncmpi  33906  onint1  33910  bj-inrab  34369  bj-rcleqf  34461  bj-restuni  34512  bj-opelresdm  34560  bj-idres  34575  bj-opelidres  34576  bj-eldiag  34591  bj-eldiag2  34592  bj-ccinftydisj  34628  taupilem3  34733  isbasisrelowllem1  34772  isbasisrelowllem2  34773  nlpineqsn  34825  fvineqsneu  34828  ptrest  35056  poimirlem29  35086  poimirlem30  35087  mblfinlem2  35095  mbfposadd  35104  itg2gt0cn  35112  dvasin  35141  inixp  35166  0totbnd  35211  sstotbnd3  35214  heibor1lem  35247  heibor1  35248  heiborlem6  35254  isexid2  35293  smgrpismgmOLD  35300  issmgrpOLD  35301  mndoissmgrpOLD  35306  ismndo  35310  exidresid  35317  rngo1cl  35377  isfld2  35443  ineleq  35768  eleccossin  35883  elrefsymrelsrel  35967  dfeldisj3  36112  prtlem14  36170  lshpdisj  36283  lkrin  36460  ishlat1  36648  pmodlem2  37143  pclfinN  37196  pclcmpatN  37197  osumcllem4N  37255  pexmidlem1N  37266  dihmeetlem1N  38586  dihglblem5apreN  38587  dihmeetlem4preN  38602  dihmeetlem13N  38615  dochnel2  38688  lcdlss  38915  mapd1o  38944  baerlem3lem2  39006  baerlem5alem2  39007  baerlem5blem2  39008  cmpfiiin  39638  mrefg2  39648  fz1eqin  39710  fnwe2lem2  39995  islmodfg  40013  islssfg2  40015  lnr2i  40060  rp-fakeinunass  40223  fiinfi  40272  elinintab  40275  elinintrab  40277  elinlem  40298  cnvcnvintabd  40300  ntrneikb  40797  ntrneik3  40799  ntrneik13  40801  radcnvrat  41018  nzin  41022  onfrALTlem2  41252  onfrALTlem2VD  41595  inn0f  41707  iooabslt  42136  iccintsng  42160  lptioo2cn  42287  lptioo1cn  42288  cncfuni  42528  icccncfext  42529  stoweidlem44  42686  fourierdlem42  42791  fourierdlem80  42828  sge00  43015  eldmressn  43629  afvres  43728  afv2res  43795  prproropf1olem0  44019  31prm  44114  rnghmval2  44519  rnghmsubcsetclem1  44599  rngccatidALTV  44613  funcrngcsetcALT  44623  zrinitorngc  44624  zrtermorngc  44625  rhmsubcsetclem1  44645  rhmsubcrngclem1  44651  ringcbasbas  44658  funcringcsetcALTV2lem7  44666  ringccatidALTV  44676  ringcbasbasALTV  44682  funcringcsetclem7ALTV  44689  irinitoringc  44693  zrtermoringc  44694  srhmsubclem1  44697  fldhmsubc  44708  fldhmsubcALTV  44726  rhmsubcALTVlem3  44730  ssnn0ssfz  44751  elbigo2  44966  itsclinecirc0in  45189