Theorem elin 3915

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 3459	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 3459	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	adantl 481	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2822	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2822	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	4, 5	anbi12d 632	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
7		df-in 3906	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 3633	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 378	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  Vcvv 3438   ∩ cin 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-in 3906

This theorem is referenced by:  elini  4149  elind  4150  elinel1  4151  elinel2  4152  elin2  4153  elin3  4156  ineqri  4162  nfin  4174  inass  4178  ssin  4189  ssrin  4192  ralin  4199  rexin  4200  dfss4  4219  difin  4222  indi  4234  undi  4235  unineq  4238  indifdi  4244  difin2  4251  inrab2  4267  ndisj  4320  inn0f  4321  difin0ss  4323  inssdif0  4324  inelcm  4415  inundif  4429  elinsn  4665  uniin  4885  intun  4933  intprg  4934  elrint  4942  iunin2  5024  iinin2  5031  elriin  5034  disjor  5078  disjiun  5084  brin  5148  trin  5214  inex1  5260  inuni  5293  wefrc  5616  inopab  5776  inxp  5778  inxpOLD  5779  dmin  5858  dfres3  5941  intasym  6070  asymref  6071  dminss  6109  imainss  6110  inimasn  6112  cnvresima  6186  dfco2a  6202  ordtri3or  6347  2elresin  6611  respreima  7009  fvcofneq  7036  tpres  7145  isomin  7281  isoini  7282  offval  7629  ordpwsuc  7755  frpoins3xpg  8080  frpoins3xp3g  8081  xpord3pred  8092  ressuppss  8123  frrlem13  8238  fprlem1  8240  uniinqs  8732  mapval2  8808  ixpin  8859  boxriin  8876  disjen  9060  ssenen  9077  onfin2  9139  elfpw  9252  fiin  9323  inf3lem2  9536  epfrs  9638  cp  9801  dfac5lem1  10031  dfac5lem5  10035  dfac5  10037  kmlem3  10061  kmlem14  10072  kmlem15  10073  fin23lem26  10233  pwxpndom2  10574  ingru  10724  gruina  10727  grur1  10729  axgroth4  10741  grothprim  10743  ixxdisj  13274  icodisj  13390  fzdisj  13465  nn0disj  13558  fzouzdisj  13609  cotr2g  14897  limsupgle  15398  ello12  15437  elo12  15448  lo1resb  15485  rlimresb  15486  o1resb  15487  lo1eq  15489  rlimeq  15490  fsumsplit  15662  sumsplit  15689  fsum2dlem  15691  fprod2dlem  15901  bitsmod  16361  saddisjlem  16389  sadadd  16392  sadass  16396  smuval2  16407  smupval  16413  smueqlem  16415  smumul  16418  isprm7  16633  prmreclem5  16846  prmrec  16848  4sqlem12  16882  vdwmc  16904  setsstruct2  17099  acsfn  17580  iszeroo  17920  iszeroi  17931  fpwipodrs  18461  psss  18501  insubm  18741  subgacs  19088  nsgacs  19089  resscntz  19260  gsmsymgreq  19359  sylow2a  19546  lsmmod  19602  lsmdisj2  19609  gsumzsplit  19854  subgdmdprd  19963  dprdcntz2  19967  dprddisj2  19968  pgpfac1lem3  20006  rnghmval2  20378  isrhm  20412  subsubrng2  20495  subsubrg2  20530  rnghmsubcsetclem1  20562  funcrngcsetcALT  20572  zrinitorngc  20573  zrtermorngc  20574  rhmsubcsetclem1  20591  rhmsubcrngclem1  20597  ringcbasbas  20604  zrtermoringc  20606  srhmsubclem1  20608  fldhmsubc  20716  acsfn1p  20730  subrgacs  20731  sdrgacs  20732  isorng  20792  lssacs  20916  lspdisj  21078  lspdisjb  21079  dfprm2  21426  irinitoringc  21432  ocvin  21627  unocv  21633  iunocv  21634  obselocv  21681  isassa  21809  aspid  21828  aspval2  21852  pmatcoe1fsupp  22643  isbasis2g  22890  tgval2  22898  tgcl  22911  ppttop  22949  epttop  22951  ssntr  23000  ntreq0  23019  isclo  23029  restntr  23124  restlp  23125  cnpresti  23230  cnprest  23231  cnprest2  23232  lmss  23240  haust1  23294  nrmsep3  23297  isnrm2  23300  lmmo  23322  fincmp  23335  cmpsublem  23341  cmpsub  23342  uncmp  23345  hauscmplem  23348  dfconn2  23361  iunconnlem  23369  unconn  23371  is1stc2  23384  1stcrest  23395  1stcelcls  23403  llyi  23416  nllyi  23417  subislly  23423  lly1stc  23438  txcnp  23562  txcnmpt  23566  hausdiag  23587  kqcldsat  23675  isfbas2  23777  isfil2  23798  fbasfip  23810  elfg  23813  filconn  23825  rnelfmlem  23894  rnelfm  23895  fmfnfmlem2  23897  fmfnfmlem4  23899  fmfnfm  23900  flimrest  23925  hauspwpwf1  23929  fclsrest  23966  alexsubALTlem2  23990  alexsubALTlem3  23991  alexsubALTlem4  23992  alexsubALT  23993  istmd  24016  istgp  24019  tsmssubm  24085  tsmssplit  24094  istrg  24106  istdrg  24108  istlm  24127  ustfilxp  24155  utoptop  24176  utop3cls  24193  bldisj  24340  blin  24363  blres  24373  lpbl  24445  metrest  24466  restmetu  24512  isngp  24538  isnlm  24617  isnmhm  24688  xrtgioo  24749  xrsmopn  24755  icccmplem2  24766  reconnlem2  24770  icoopnst  24890  iocopnst  24891  bndth  24911  zclmncvs  25102  isncvsngp  25103  ncvsprp  25106  ncvsm1  25108  ncvsdif  25109  ncvspi  25110  ncvs1  25111  ncvspds  25115  iscph  25124  tcphcph  25191  cfilfcls  25228  cmetcaulem  25242  isbn  25292  cldcss2  25396  hlhil  25397  ovolfcl  25421  ovolicc2lem2  25473  ovolicc2  25477  shftmbl  25493  volfiniun  25502  mbfmax  25604  mbfimaopnlem  25610  mbfaddlem  25615  i1faddlem  25648  i1fmullem  25649  i1fres  25660  itg1climres  25669  mbfi1fseqlem4  25673  itg2splitlem  25703  itg2split  25704  itgresr  25734  ellimc2  25832  ellimc3  25834  limcun  25850  dvreslem  25864  dvne0  25970  itgsubstlem  26009  ig1pval3  26137  aaliou2  26302  aaliou2b  26303  pilem1  26415  rlimcnp2  26930  fsumharmonic  26976  ppisval2  27069  prmorcht  27142  fsumvma2  27179  pclogsum  27180  vmasum  27181  chpchtsum  27184  chpub  27185  rpvmasum2  27477  madeval2  27821  tglineineq  28664  trlsegvdeg  30251  frgrncvvdeqlem7  30329  frgrncvvdeqlem9  30331  minvecolem1  30898  minvecolem4a  30901  minvecolem4b  30902  minvecolem4  30904  h2hcau  31003  axhcompl-zf  31022  hhcmpl  31224  hhcms  31227  ocin  31320  ocnel  31322  shmodsi  31413  pjhthlem2  31416  omlsilem  31426  pjoc1i  31455  spansnm0i  31674  nonbooli  31675  5oalem7  31684  3oalem3  31688  pjssmii  31705  mayete3i  31752  nmcopex  32053  nmcoplb  32054  lncnopbd  32061  nmcfnex  32077  nmcfnlb  32078  riesz4  32088  riesz1  32089  riesz2  32090  cnlnadjlem3  32093  cnlnadjlem5  32095  cnlnadjlem9  32099  cnlnadjeu  32102  rnbra  32131  pjimai  32200  pjclem4a  32222  pj3lem1  32230  jpi  32294  sumdmdii  32439  sumdmdlem  32442  sumdmdlem2  32443  cdjreui  32456  cdj3lem1  32458  iunin1f  32581  disjorf  32603  ofpreima  32692  1stpreima  32735  2ndpreima  32736  iocinioc2  32808  ssnnssfz  32816  cntzun  33110  kerunit  33355  prmidl0  33480  ressply1mon1p  33598  ccfldextdgrr  33778  crefdf  33954  cmpcref  33956  cmppcmp  33964  cnre2csqima  34017  ordtconnlem1  34030  lmxrge0  34058  isrrext  34106  esum0  34155  esumcst  34169  esumpcvgval  34184  esumcvg  34192  measvuni  34320  eulerpartlemt0  34475  eulerpartlemr  34480  eulerpartlemgf  34485  eulerpartlemgs2  34486  eulerpartlemn  34487  fiblem  34504  oddprm2  34761  bnj1173  35107  bnj1174  35108  bnj1279  35123  elima4  35919  dfon2lem4  35927  ellimits  36051  dfom5b  36053  brapply  36079  brcap  36081  dfrecs2  36093  dfrdg4  36094  finminlem  36461  neibastop2lem  36503  neibastop2  36504  neifg  36514  tailfb  36520  onsucconni  36580  onintopssconn  36583  onsucsuccmpi  36586  limsucncmpi  36588  onint1  36592  bj-inrab  37071  bj-rcleqf  37169  bj-restuni  37241  bj-opelresdm  37289  bj-idres  37304  bj-opelidres  37305  bj-eldiag  37320  bj-eldiag2  37321  bj-ccinftydisj  37357  taupilem3  37463  isbasisrelowllem1  37499  isbasisrelowllem2  37500  nlpineqsn  37552  fvineqsneu  37555  ptrest  37759  poimirlem29  37789  poimirlem30  37790  mblfinlem2  37798  mbfposadd  37807  itg2gt0cn  37815  dvasin  37844  inixp  37868  0totbnd  37913  sstotbnd3  37916  heibor1lem  37949  heibor1  37950  heiborlem6  37956  isexid2  37995  smgrpismgmOLD  38002  issmgrpOLD  38003  mndoissmgrpOLD  38008  ismndo  38012  exidresid  38019  rngo1cl  38079  isfld2  38145  ineleq  38486  refressn  38645  eleccossin  38685  elrefsymrelsrel  38767  dfeldisj3  38917  disjlem14  38996  prtlem14  39073  lshpdisj  39186  lkrin  39363  ishlat1  39551  pmodlem2  40046  pclfinN  40099  pclcmpatN  40100  osumcllem4N  40158  pexmidlem1N  40169  dihmeetlem1N  41489  dihglblem5apreN  41490  dihmeetlem4preN  41505  dihmeetlem13N  41518  dochnel2  41591  lcdlss  41818  mapd1o  41847  baerlem3lem2  41909  baerlem5alem2  41910  baerlem5blem2  41911  redvmptabs  42557  cmpfiiin  42881  mrefg2  42891  fz1eqin  42953  fnwe2lem2  43235  islmodfg  43253  islssfg2  43255  lnr2i  43300  rp-fakeinunass  43698  fiinfi  43756  elinintab  43758  elinintrab  43760  elinlem  43781  cnvcnvintabd  43783  ntrneikb  44277  ntrneik3  44279  ntrneik13  44281  ismnushort  44484  radcnvrat  44497  nzin  44501  onfrALTlem2  44729  onfrALTlem2VD  45071  relpmin  45135  pwclaxpow  45167  dfac5prim  45173  modelac8prim  45175  permac8prim  45197  iooabslt  45687  iccintsng  45711  lptioo2cn  45831  lptioo1cn  45832  cncfuni  46072  icccncfext  46073  stoweidlem44  46230  fourierdlem42  46335  fourierdlem80  46372  sge00  46562  eldmressn  47225  afvres  47360  afv2res  47427  prproropf1olem0  47690  31prm  47785  rngccatidALTV  48460  rhmsubcALTVlem3  48471  funcringcsetcALTV2lem7  48484  ringccatidALTV  48494  ringcbasbasALTV  48500  funcringcsetclem7ALTV  48507  fldhmsubcALTV  48521  ssnn0ssfz  48537  elbigo2  48740  itsclinecirc0in  48963  resinsnALT  49060  opndisj  49090  clddisj  49091  i0oii  49107  io1ii  49108