Theorem elin 3967

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 variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3501	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 3501	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	adantl 481	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2829	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2829	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	4, 5	anbi12d 632	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
7		df-in 3958	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 3680	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 378	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108  Vcvv 3480   ∩ cin 3950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958

This theorem is referenced by:  elini  4199  elind  4200  elinel1  4201  elinel2  4202  elin2  4203  elin3  4206  ineqri  4212  nfin  4224  inass  4228  ssin  4239  ssrin  4242  ralin  4249  rexin  4250  dfss4  4269  difin  4272  indi  4284  undi  4285  unineq  4288  indifdi  4294  difin2  4301  inrab2  4317  ndisj  4370  inn0f  4371  difin0ss  4373  inssdif0  4374  inelcm  4465  inundif  4479  elinsn  4710  uniin  4931  intun  4980  intprg  4981  elrint  4989  iunin2  5071  iinin2  5078  elriin  5081  disjor  5125  disjiun  5131  brin  5195  trin  5271  inex1  5317  inuni  5350  wefrc  5679  inopab  5839  inxp  5842  inxpOLD  5843  dmin  5922  dfres3  6002  intasym  6135  asymref  6136  dminss  6173  imainss  6174  inimasn  6176  cnvresima  6250  dfco2a  6266  ordtri3or  6416  2elresin  6689  respreima  7086  fvcofneq  7113  tpres  7221  isomin  7357  isoini  7358  offval  7706  ordpwsuc  7835  frpoins3xpg  8165  frpoins3xp3g  8166  xpord3pred  8177  ressuppss  8208  frrlem13  8323  fprlem1  8325  wfrlem5OLD  8353  uniinqs  8837  mapval2  8912  ixpin  8963  boxriin  8980  disjen  9174  ssenen  9191  onfin2  9268  elfpw  9394  fiin  9462  inf3lem2  9669  epfrs  9771  cp  9931  dfac5lem1  10163  dfac5lem5  10167  dfac5  10169  kmlem3  10193  kmlem14  10204  kmlem15  10205  fin23lem26  10365  pwxpndom2  10705  ingru  10855  gruina  10858  grur1  10860  axgroth4  10872  grothprim  10874  ixxdisj  13402  icodisj  13516  fzdisj  13591  nn0disj  13684  fzouzdisj  13735  cotr2g  15015  limsupgle  15513  ello12  15552  elo12  15563  lo1resb  15600  rlimresb  15601  o1resb  15602  lo1eq  15604  rlimeq  15605  fsumsplit  15777  sumsplit  15804  fsum2dlem  15806  fprod2dlem  16016  bitsmod  16473  saddisjlem  16501  sadadd  16504  sadass  16508  smuval2  16519  smupval  16525  smueqlem  16527  smumul  16530  isprm7  16745  prmreclem5  16958  prmrec  16960  4sqlem12  16994  vdwmc  17016  setsstruct2  17211  acsfn  17702  iszeroo  18043  iszeroi  18054  fpwipodrs  18585  psss  18625  insubm  18831  subgacs  19179  nsgacs  19180  resscntz  19351  gsmsymgreq  19450  sylow2a  19637  lsmmod  19693  lsmdisj2  19700  gsumzsplit  19945  subgdmdprd  20054  dprdcntz2  20058  dprddisj2  20059  pgpfac1lem3  20097  rnghmval2  20444  isrhm  20478  subsubrng2  20564  subsubrg2  20599  rnghmsubcsetclem1  20631  funcrngcsetcALT  20641  zrinitorngc  20642  zrtermorngc  20643  rhmsubcsetclem1  20660  rhmsubcrngclem1  20666  ringcbasbas  20673  zrtermoringc  20675  srhmsubclem1  20677  fldhmsubc  20786  acsfn1p  20800  subrgacs  20801  sdrgacs  20802  lssacs  20965  lspdisj  21127  lspdisjb  21128  dfprm2  21484  irinitoringc  21490  ocvin  21692  unocv  21698  iunocv  21699  obselocv  21748  isassa  21876  aspid  21895  aspval2  21918  pmatcoe1fsupp  22707  isbasis2g  22955  tgval2  22963  tgcl  22976  ppttop  23014  epttop  23016  ssntr  23066  ntreq0  23085  isclo  23095  restntr  23190  restlp  23191  cnpresti  23296  cnprest  23297  cnprest2  23298  lmss  23306  haust1  23360  nrmsep3  23363  isnrm2  23366  lmmo  23388  fincmp  23401  cmpsublem  23407  cmpsub  23408  uncmp  23411  hauscmplem  23414  dfconn2  23427  iunconnlem  23435  unconn  23437  is1stc2  23450  1stcrest  23461  1stcelcls  23469  llyi  23482  nllyi  23483  subislly  23489  lly1stc  23504  txcnp  23628  txcnmpt  23632  hausdiag  23653  kqcldsat  23741  isfbas2  23843  isfil2  23864  fbasfip  23876  elfg  23879  filconn  23891  rnelfmlem  23960  rnelfm  23961  fmfnfmlem2  23963  fmfnfmlem4  23965  fmfnfm  23966  flimrest  23991  hauspwpwf1  23995  fclsrest  24032  alexsubALTlem2  24056  alexsubALTlem3  24057  alexsubALTlem4  24058  alexsubALT  24059  istmd  24082  istgp  24085  tsmssubm  24151  tsmssplit  24160  istrg  24172  istdrg  24174  istlm  24193  ustfilxp  24221  utoptop  24243  utop3cls  24260  bldisj  24408  blin  24431  blres  24441  lpbl  24516  metrest  24537  restmetu  24583  isngp  24609  isnlm  24696  isnmhm  24767  xrtgioo  24828  xrsmopn  24834  icccmplem2  24845  reconnlem2  24849  icoopnst  24969  iocopnst  24970  bndth  24990  zclmncvs  25182  isncvsngp  25183  ncvsprp  25186  ncvsm1  25188  ncvsdif  25189  ncvspi  25190  ncvs1  25191  ncvspds  25195  iscph  25204  tcphcph  25271  cfilfcls  25308  cmetcaulem  25322  isbn  25372  cldcss2  25476  hlhil  25477  ovolfcl  25501  ovolicc2lem2  25553  ovolicc2  25557  shftmbl  25573  volfiniun  25582  mbfmax  25684  mbfimaopnlem  25690  mbfaddlem  25695  i1faddlem  25728  i1fmullem  25729  i1fres  25740  itg1climres  25749  mbfi1fseqlem4  25753  itg2splitlem  25783  itg2split  25784  itgresr  25814  ellimc2  25912  ellimc3  25914  limcun  25930  dvreslem  25944  dvne0  26050  itgsubstlem  26089  ig1pval3  26217  aaliou2  26382  aaliou2b  26383  pilem1  26495  rlimcnp2  27009  fsumharmonic  27055  ppisval2  27148  prmorcht  27221  fsumvma2  27258  pclogsum  27259  vmasum  27260  chpchtsum  27263  chpub  27264  rpvmasum2  27556  madeval2  27892  tglineineq  28651  trlsegvdeg  30246  frgrncvvdeqlem7  30324  frgrncvvdeqlem9  30326  minvecolem1  30893  minvecolem4a  30896  minvecolem4b  30897  minvecolem4  30899  h2hcau  30998  axhcompl-zf  31017  hhcmpl  31219  hhcms  31222  ocin  31315  ocnel  31317  shmodsi  31408  pjhthlem2  31411  omlsilem  31421  pjoc1i  31450  spansnm0i  31669  nonbooli  31670  5oalem7  31679  3oalem3  31683  pjssmii  31700  mayete3i  31747  nmcopex  32048  nmcoplb  32049  lncnopbd  32056  nmcfnex  32072  nmcfnlb  32073  riesz4  32083  riesz1  32084  riesz2  32085  cnlnadjlem3  32088  cnlnadjlem5  32090  cnlnadjlem9  32094  cnlnadjeu  32097  rnbra  32126  pjimai  32195  pjclem4a  32217  pj3lem1  32225  jpi  32289  sumdmdii  32434  sumdmdlem  32437  sumdmdlem2  32438  cdjreui  32451  cdj3lem1  32453  iunin1f  32570  disjorf  32592  ofpreima  32675  1stpreima  32716  2ndpreima  32717  iocinioc2  32781  ssnnssfz  32789  cntzun  33071  isorng  33329  kerunit  33349  prmidl0  33478  ressply1mon1p  33593  ccfldextdgrr  33722  crefdf  33847  cmpcref  33849  cmppcmp  33857  cnre2csqima  33910  ordtconnlem1  33923  lmxrge0  33951  isrrext  34001  esum0  34050  esumcst  34064  esumpcvgval  34079  esumcvg  34087  measvuni  34215  eulerpartlemt0  34371  eulerpartlemr  34376  eulerpartlemgf  34381  eulerpartlemgs2  34382  eulerpartlemn  34383  fiblem  34400  oddprm2  34670  bnj1173  35016  bnj1174  35017  bnj1279  35032  elima4  35776  dfon2lem4  35787  ellimits  35911  dfom5b  35913  brapply  35939  brcap  35941  dfrecs2  35951  dfrdg4  35952  finminlem  36319  neibastop2lem  36361  neibastop2  36362  neifg  36372  tailfb  36378  onsucconni  36438  onintopssconn  36441  onsucsuccmpi  36444  limsucncmpi  36446  onint1  36450  bj-inrab  36928  bj-rcleqf  37026  bj-restuni  37098  bj-opelresdm  37146  bj-idres  37161  bj-opelidres  37162  bj-eldiag  37177  bj-eldiag2  37178  bj-ccinftydisj  37214  taupilem3  37320  isbasisrelowllem1  37356  isbasisrelowllem2  37357  nlpineqsn  37409  fvineqsneu  37412  ptrest  37626  poimirlem29  37656  poimirlem30  37657  mblfinlem2  37665  mbfposadd  37674  itg2gt0cn  37682  dvasin  37711  inixp  37735  0totbnd  37780  sstotbnd3  37783  heibor1lem  37816  heibor1  37817  heiborlem6  37823  isexid2  37862  smgrpismgmOLD  37869  issmgrpOLD  37870  mndoissmgrpOLD  37875  ismndo  37879  exidresid  37886  rngo1cl  37946  isfld2  38012  ineleq  38355  refressn  38444  eleccossin  38484  elrefsymrelsrel  38572  dfeldisj3  38720  disjlem14  38799  prtlem14  38875  lshpdisj  38988  lkrin  39165  ishlat1  39353  pmodlem2  39849  pclfinN  39902  pclcmpatN  39903  osumcllem4N  39961  pexmidlem1N  39972  dihmeetlem1N  41292  dihglblem5apreN  41293  dihmeetlem4preN  41308  dihmeetlem13N  41321  dochnel2  41394  lcdlss  41621  mapd1o  41650  baerlem3lem2  41712  baerlem5alem2  41713  baerlem5blem2  41714  redvmptabs  42390  cmpfiiin  42708  mrefg2  42718  fz1eqin  42780  fnwe2lem2  43063  islmodfg  43081  islssfg2  43083  lnr2i  43128  rp-fakeinunass  43528  fiinfi  43586  elinintab  43588  elinintrab  43590  elinlem  43611  cnvcnvintabd  43613  ntrneikb  44107  ntrneik3  44109  ntrneik13  44111  ismnushort  44320  radcnvrat  44333  nzin  44337  onfrALTlem2  44566  onfrALTlem2VD  44909  relpmin  44973  pwclaxpow  45001  dfac5prim  45007  modelac8prim  45009  iooabslt  45512  iccintsng  45536  lptioo2cn  45660  lptioo1cn  45661  cncfuni  45901  icccncfext  45902  stoweidlem44  46059  fourierdlem42  46164  fourierdlem80  46201  sge00  46391  eldmressn  47049  afvres  47184  afv2res  47251  prproropf1olem0  47489  31prm  47584  rngccatidALTV  48188  rhmsubcALTVlem3  48199  funcringcsetcALTV2lem7  48212  ringccatidALTV  48222  ringcbasbasALTV  48228  funcringcsetclem7ALTV  48235  fldhmsubcALTV  48249  ssnn0ssfz  48265  elbigo2  48473  itsclinecirc0in  48696  resinsnALT  48773  opndisj  48800  clddisj  48801  i0oii  48817  io1ii  48818