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 3472	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 3472	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	adantl 487	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2849	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2849	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	4, 5	anbi12d 644	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
7		df-in 3906	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 3634	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 381	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  Vcvv 3451   ∩ cin 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906

This theorem is used by:  elini  4145  elind  4146  elinel1  4147  elinel2  4148  elin2  4149  elin3  4152  ineqri  4158  nfin  4170  inass  4173  ssin  4184  ssrin  4187  ralin  4195  rexin  4196  dfss4  4215  difin  4218  indi  4230  undi  4231  unineq  4234  indifdi  4240  difin2  4247  inrab2  4263  ndisj  4318  inn0f  4319  difin0ss  4321  inssdif0OLD  4323  inelcm  4418  inundif  4435  elinsn  4671  uniinOLD  4892  intun  4940  intprg  4941  elrint  4949  iunin2  5029  iinin2  5038  elriin  5041  disjor  5085  disjiun  5091  brin  5157  trin  5224  inex1  5277  inuni  5311  wefrc  5645  inopab  5807  inxp  5809  dmin  5893  dfres3  5975  intasym  6109  asymref  6110  dminss  6143  imainss  6144  inimasn  6146  cnvresima  6231  dfco2a  6247  ordtri3or  6395  2elresin  6660  respreima  7065  fvcofneq  7093  tpres  7207  isomin  7345  isoini  7346  offval  7702  ordpwsuc  7826  fnwe2lem3  8147  frpoins3xpg  8157  frpoins3xp3g  8158  xpord3pred  8169  ressuppss  8200  frrlem13  8316  fprlem1  8318  uniinqs  8818  mapval2  8900  ixpin  8951  boxriin  8968  disjen  9153  ssenen  9170  onfin2  9232  elfpw  9343  fiin  9414  inf3lem2  9630  epfrs  9732  cp  9954  dfac5lem1  10202  dfac5lem5  10206  dfac5  10207  kmlem3  10231  kmlem14  10242  kmlem15  10243  fin23lem26  10403  pwxpndom2  10750  ingru  10900  gruina  10903  grur1  10905  axgroth4  10917  grothprim  10919  ixxdisj  13491  icodisj  13607  fzdisj  13685  nn0disj  13778  fzouzdisj  13830  cotr2g  15129  limsupgle  15644  ello12  15683  elo12  15694  lo1resb  15731  rlimresb  15732  o1resb  15733  lo1eq  15735  rlimeq  15736  fsumsplit  15907  sumsplit  15934  fsum2dlem  15936  fprod2dlem  16147  bitsmod  16606  saddisjlem  16634  sadadd  16637  sadass  16641  smuval2  16652  smupval  16658  smueqlem  16660  smumul  16663  isprm7  16884  prmreclem5  17098  prmrec  17100  4sqlem12  17134  vdwmc  17156  setsstruct2  17352  acsfn  17833  iszeroo  18173  iszeroi  18184  fpwipodrs  18714  psss  18754  insubm  19014  subgacs  19371  nsgacs  19372  resscntz  19547  gsmsymgreq  19646  sylow2a  19833  lsmmod  19889  lsmdisj2  19896  gsumzsplit  20141  subgdmdprd  20250  dprdcntz2  20254  dprddisj2  20255  pgpfac1lem3  20293  rnghmval2  20674  isrhm  20709  subsubrng2  20816  subsubrg2  20851  rnghmsubcsetclem1  20883  funcrngcsetcALT  20893  zrinitorngc  20894  zrtermorngc  20895  rhmsubcsetclem1  20912  rhmsubcrngclem1  20918  ringcbasbas  20925  zrtermoringc  20927  srhmsubclem1  20929  fldhmsubc  21042  acsfn1p  21056  subrgacs  21057  sdrgacs  21058  isorng  21118  lssacs  21242  lspdisj  21403  lspdisjb  21404  prmidl0  21634  dfprm2  21779  irinitoringc  21785  ocvin  21980  unocv  21986  iunocv  21987  obselocv  22034  isassa  22164  aspid  22182  aspval2  22206  pmatcoe1fsupp  23019  isbasis2g  23266  tgval2  23274  tgcl  23287  ppttop  23325  epttop  23327  ssntr  23376  ntreq0  23395  isclo  23405  restntr  23500  restlp  23501  cnpresti  23606  cnprest  23607  cnprest2  23608  lmss  23616  haust1  23670  nrmsep3  23673  isnrm2  23676  lmmo  23698  fincmp  23711  cmpsublem  23717  cmpsub  23718  uncmp  23721  hauscmplem  23724  dfconn2  23737  iunconnlem  23745  unconn  23747  is1stc2  23760  1stcrest  23771  1stcelcls  23780  llyi  23793  nllyi  23794  subislly  23800  lly1stc  23815  txcnp  23939  txcnmpt  23943  hausdiag  23964  kqcldsat  24052  isfbas2  24154  isfil2  24175  fbasfip  24187  elfg  24190  filconn  24202  rnelfmlem  24271  rnelfm  24272  fmfnfmlem2  24274  fmfnfmlem4  24276  fmfnfm  24277  flimrest  24302  hauspwpwf1  24306  fclsrest  24343  alexsubALTlem2  24367  alexsubALTlem3  24368  alexsubALTlem4  24369  alexsubALT  24370  istmd  24393  istgp  24396  tsmssubm  24462  tsmssplit  24471  istrg  24483  istdrg  24485  istlm  24504  ustfilxp  24532  utoptop  24553  utop3cls  24570  bldisj  24717  blin  24740  blres  24750  lpbl  24822  metrest  24843  restmetu  24889  isngp  24915  isnlm  24994  isnmhm  25065  xrtgioo  25126  xrsmopn  25132  icccmplem2  25143  reconnlem2  25147  icoopnst  25260  iocopnst  25261  bndth  25279  zclmncvs  25469  isncvsngp  25470  ncvsprp  25473  ncvsm1  25475  ncvsdif  25476  ncvspi  25477  ncvs1  25478  ncvspds  25482  iscph  25491  tcphcph  25558  cfilfcls  25595  cmetcaulem  25609  isbn  25659  cldcss2  25763  hlhil  25764  ovolfcl  25787  ovolicc2lem2  25839  ovolicc2  25843  shftmbl  25859  volfiniun  25868  mbfmax  25970  mbfimaopnlem  25976  mbfaddlem  25981  i1faddlem  26014  i1fmullem  26015  i1fres  26026  itg1climres  26035  mbfi1fseqlem4  26039  itg2splitlem  26069  itg2split  26070  itgresr  26099  ellimc2  26197  ellimc3  26199  limcun  26215  dvreslem  26229  dvne0  26331  itgsubstlem  26368  ig1pval3  26496  aaliou2  26667  aaliou2b  26668  pilem1  26778  rlimcnp2  27294  fsumharmonic  27339  ppisval2  27432  prmorcht  27505  fsumvma2  27541  pclogsum  27542  vmasum  27543  chpchtsum  27546  chpub  27547  rpvmasum2  27839  madeval2  28219  tglineineq  29111  angmgmaddcpbl  29390  trlsegvdeg  30828  frgrncvvdeqlem7  30906  frgrncvvdeqlem9  30908  minvecolem1  31476  minvecolem4a  31479  minvecolem4b  31480  minvecolem4  31482  h2hcau  31581  axhcompl-zf  31600  hhcmpl  31802  hhcms  31805  ocin  31898  ocnel  31900  shmodsi  31991  pjhthlem2  31994  omlsilem  32004  pjoc1i  32033  spansnm0i  32252  nonbooli  32253  5oalem7  32262  3oalem3  32266  pjssmii  32283  mayete3i  32330  nmcopex  32631  nmcoplb  32632  lncnopbd  32639  nmcfnex  32655  nmcfnlb  32656  riesz4  32666  riesz1  32667  riesz2  32668  cnlnadjlem3  32671  cnlnadjlem5  32673  cnlnadjlem9  32677  cnlnadjeu  32680  rnbra  32709  pjimai  32778  pjclem4a  32800  pj3lem1  32808  jpi  32872  sumdmdii  33017  sumdmdlem  33020  sumdmdlem2  33021  cdjreui  33034  cdj3lem1  33036  iunin1f  33152  disjorf  33173  ofpreima  33259  1stpreima  33300  2ndpreima  33301  iocinioc2  33371  ssnnssfz  33379  cntzun  33640  kerunit  33886  ressply1mon1p  34100  ccfldextdgrr  34304  crefdf  34480  cmpcref  34482  cmppcmp  34490  cnre2csqima  34543  ordtconnlem1  34556  lmxrge0  34584  isrrext  34632  esum0  34681  esumcst  34695  esumpcvgval  34710  esumcvg  34718  measvuni  34847  eulerpartlemt0  35001  eulerpartlemr  35006  eulerpartlemgf  35011  eulerpartlemgs2  35012  eulerpartlemn  35013  fiblem  35030  oddprm2  35284  bnj1173  35632  bnj1174  35633  bnj1279  35648  elima4  36540  dfon2lem4  36548  ellimits  36672  dfom5b  36674  brapply  36700  brcap  36702  dfrecs2  36714  dfrdg4  36715  finminlem  37106  neibastop2lem  37148  neibastop2  37149  neifg  37159  tailfb  37165  onsucconni  37225  onintopssconn  37228  onsucsuccmpi  37231  limsucncmpi  37233  onint1  37237  mh-infprim2bi  37335  bj-inex1gALT  37837  bj-inrab  37840  bj-rcleqf  37938  coi1in  37961  bj-restuni  38018  bj-opelresdm  38066  bj-idres  38081  bj-opelidres  38082  bj-eldiag  38097  bj-eldiag2  38098  bj-ccinftydisj  38134  taupilem3  38240  isbasisrelowllem1  38278  isbasisrelowllem2  38279  nlpineqsn  38331  fvineqsneu  38334  ptrest  38537  poimirlem29  38567  poimirlem30  38568  mblfinlem2  38576  mbfposadd  38585  itg2gt0cn  38593  dvasin  38622  inixp  38662  0totbnd  38707  sstotbnd3  38710  heibor1lem  38743  heibor1  38744  heiborlem6  38750  isexid2  38789  smgrpismgmOLD  38796  issmgrpOLD  38797  mndoissmgrpOLD  38802  ismndo  38806  exidresid  38813  rngo1cl  38873  isfld2  38939  ineleq  39286  refressn  39465  eleccossin  39505  elrefsymrelsrel  39587  dfeldisj3  39743  eldisjdmqsim  39749  disjlem14  39833  prtlem14  39931  lshpdisj  40044  lkrin  40221  ishlat1  40409  pmodlem2  40904  pclfinN  40957  pclcmpatN  40958  osumcllem4N  41016  pexmidlem1N  41027  dihmeetlem1N  42347  dihglblem5apreN  42348  dihmeetlem4preN  42363  dihmeetlem13N  42376  dochnel2  42449  lcdlss  42676  mapd1o  42705  baerlem3lem2  42767  baerlem5alem2  42768  baerlem5blem2  42769  redvmptabs  43411  cmpfiiin  43707  mrefg2  43717  fz1eqin  43779  islmodfg  44070  islssfg2  44072  lnr2i  44117  rp-fakeinunass  44515  fiinfi  44573  elinintab  44575  elinintrab  44577  elinlem  44597  cnvcnvintabd  44599  ntrneikb  45093  ntrneik3  45095  ntrneik13  45097  ismnushort  45284  radcnvrat  45297  nzin  45301  onfrALTlem2  45528  onfrALTlem2VD  45870  relpmin  45941  pwclaxpow  45973  dfac5prim  45979  modelac8prim  45981  permac8prim  46003  iooabslt  46510  iccintsng  46534  lptioo2cn  46654  lptioo1cn  46655  cncfuni  46895  icccncfext  46896  stoweidlem44  47053  fourierdlem42  47158  fourierdlem80  47195  sge00  47385  wrddin2  47897  chndin2  47902  chnrin2  47907  eldmressn  48106  afvres  48241  afv2res  48308  prproropf1olem0  48583  31prm  48681  indprmfz  48714  rngccatidALTV  49368  rhmsubcALTVlem3  49379  funcringcsetcALTV2lem7  49392  ringccatidALTV  49402  ringcbasbasALTV  49408  funcringcsetclem7ALTV  49415  fldhmsubcALTV  49429  dfidom2  49439  ssnn0ssfz  49460  elbigo2  49663  itsclinecirc0in  49886  resinsnALT  49980  opndisj  50010  clddisj  50011  i0oii  50027  io1ii  50028