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 3471	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 3471	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	adantl 487	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2848	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2848	. . . 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 3450   ∩ 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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  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  5280  inuni  5314  wefrc  5649  inopab  5810  inxp  5812  dmin  5895  dfres3  5977  intasym  6109  asymref  6110  dminss  6144  imainss  6145  inimasn  6147  cnvresima  6226  dfco2a  6242  ordtri3or  6390  2elresin  6654  respreima  7059  fvcofneq  7087  tpres  7201  isomin  7339  isoini  7340  offval  7688  ordpwsuc  7812  frpoins3xpg  8139  frpoins3xp3g  8140  xpord3pred  8151  ressuppss  8182  frrlem13  8298  fprlem1  8300  uniinqs  8798  mapval2  8880  ixpin  8931  boxriin  8948  disjen  9133  ssenen  9150  onfin2  9212  elfpw  9322  fiin  9393  inf3lem2  9609  epfrs  9711  cp  9894  dfac5lem1  10127  dfac5lem5  10131  dfac5  10132  kmlem3  10156  kmlem14  10167  kmlem15  10168  fin23lem26  10328  pwxpndom2  10675  ingru  10825  gruina  10828  grur1  10830  axgroth4  10842  grothprim  10844  ixxdisj  13414  icodisj  13530  fzdisj  13607  nn0disj  13700  fzouzdisj  13752  cotr2g  15050  limsupgle  15565  ello12  15604  elo12  15615  lo1resb  15652  rlimresb  15653  o1resb  15654  lo1eq  15656  rlimeq  15657  fsumsplit  15828  sumsplit  15855  fsum2dlem  15857  fprod2dlem  16068  bitsmod  16527  saddisjlem  16555  sadadd  16558  sadass  16562  smuval2  16573  smupval  16579  smueqlem  16581  smumul  16584  isprm7  16800  prmreclem5  17013  prmrec  17015  4sqlem12  17049  vdwmc  17071  setsstruct2  17267  acsfn  17748  iszeroo  18088  iszeroi  18099  fpwipodrs  18629  psss  18669  insubm  18928  subgacs  19285  nsgacs  19286  resscntz  19461  gsmsymgreq  19560  sylow2a  19747  lsmmod  19803  lsmdisj2  19810  gsumzsplit  20055  subgdmdprd  20164  dprdcntz2  20168  dprddisj2  20169  pgpfac1lem3  20207  rnghmval2  20586  isrhm  20621  subsubrng2  20727  subsubrg2  20762  rnghmsubcsetclem1  20794  funcrngcsetcALT  20804  zrinitorngc  20805  zrtermorngc  20806  rhmsubcsetclem1  20823  rhmsubcrngclem1  20829  ringcbasbas  20836  zrtermoringc  20838  srhmsubclem1  20840  fldhmsubc  20952  acsfn1p  20966  subrgacs  20967  sdrgacs  20968  isorng  21028  lssacs  21152  lspdisj  21313  lspdisjb  21314  prmidl0  21542  dfprm2  21687  irinitoringc  21693  ocvin  21888  unocv  21894  iunocv  21895  obselocv  21942  isassa  22072  aspid  22090  aspval2  22114  pmatcoe1fsupp  22927  isbasis2g  23174  tgval2  23182  tgcl  23195  ppttop  23233  epttop  23235  ssntr  23284  ntreq0  23303  isclo  23313  restntr  23408  restlp  23409  cnpresti  23514  cnprest  23515  cnprest2  23516  lmss  23524  haust1  23578  nrmsep3  23581  isnrm2  23584  lmmo  23606  fincmp  23619  cmpsublem  23625  cmpsub  23626  uncmp  23629  hauscmplem  23632  dfconn2  23645  iunconnlem  23653  unconn  23655  is1stc2  23668  1stcrest  23679  1stcelcls  23688  llyi  23701  nllyi  23702  subislly  23708  lly1stc  23723  txcnp  23847  txcnmpt  23851  hausdiag  23872  kqcldsat  23960  isfbas2  24062  isfil2  24083  fbasfip  24095  elfg  24098  filconn  24110  rnelfmlem  24179  rnelfm  24180  fmfnfmlem2  24182  fmfnfmlem4  24184  fmfnfm  24185  flimrest  24210  hauspwpwf1  24214  fclsrest  24251  alexsubALTlem2  24275  alexsubALTlem3  24276  alexsubALTlem4  24277  alexsubALT  24278  istmd  24301  istgp  24304  tsmssubm  24370  tsmssplit  24379  istrg  24391  istdrg  24393  istlm  24412  ustfilxp  24440  utoptop  24461  utop3cls  24478  bldisj  24625  blin  24648  blres  24658  lpbl  24730  metrest  24751  restmetu  24797  isngp  24823  isnlm  24902  isnmhm  24973  xrtgioo  25034  xrsmopn  25040  icccmplem2  25051  reconnlem2  25055  icoopnst  25168  iocopnst  25169  bndth  25187  zclmncvs  25377  isncvsngp  25378  ncvsprp  25381  ncvsm1  25383  ncvsdif  25384  ncvspi  25385  ncvs1  25386  ncvspds  25390  iscph  25399  tcphcph  25466  cfilfcls  25503  cmetcaulem  25517  isbn  25567  cldcss2  25671  hlhil  25672  ovolfcl  25695  ovolicc2lem2  25747  ovolicc2  25751  shftmbl  25767  volfiniun  25776  mbfmax  25878  mbfimaopnlem  25884  mbfaddlem  25889  i1faddlem  25922  i1fmullem  25923  i1fres  25934  itg1climres  25943  mbfi1fseqlem4  25947  itg2splitlem  25977  itg2split  25978  itgresr  26007  ellimc2  26105  ellimc3  26107  limcun  26123  dvreslem  26137  dvne0  26239  itgsubstlem  26276  ig1pval3  26404  aaliou2  26577  aaliou2b  26578  pilem1  26688  rlimcnp2  27204  fsumharmonic  27249  ppisval2  27342  prmorcht  27415  fsumvma2  27451  pclogsum  27452  vmasum  27453  chpchtsum  27456  chpub  27457  rpvmasum2  27749  madeval2  28099  tglineineq  28991  angmgmaddcpbl  29270  trlsegvdeg  30708  frgrncvvdeqlem7  30786  frgrncvvdeqlem9  30788  minvecolem1  31356  minvecolem4a  31359  minvecolem4b  31360  minvecolem4  31362  h2hcau  31461  axhcompl-zf  31480  hhcmpl  31682  hhcms  31685  ocin  31778  ocnel  31780  shmodsi  31871  pjhthlem2  31874  omlsilem  31884  pjoc1i  31913  spansnm0i  32132  nonbooli  32133  5oalem7  32142  3oalem3  32146  pjssmii  32163  mayete3i  32210  nmcopex  32511  nmcoplb  32512  lncnopbd  32519  nmcfnex  32535  nmcfnlb  32536  riesz4  32546  riesz1  32547  riesz2  32548  cnlnadjlem3  32551  cnlnadjlem5  32553  cnlnadjlem9  32557  cnlnadjeu  32560  rnbra  32589  pjimai  32658  pjclem4a  32680  pj3lem1  32688  jpi  32752  sumdmdii  32897  sumdmdlem  32900  sumdmdlem2  32901  cdjreui  32914  cdj3lem1  32916  iunin1f  33032  disjorf  33053  ofpreima  33139  1stpreima  33180  2ndpreima  33181  iocinioc2  33251  ssnnssfz  33259  cntzun  33520  kerunit  33766  ressply1mon1p  33979  ccfldextdgrr  34183  crefdf  34359  cmpcref  34361  cmppcmp  34369  cnre2csqima  34422  ordtconnlem1  34435  lmxrge0  34463  isrrext  34511  esum0  34560  esumcst  34574  esumpcvgval  34589  esumcvg  34597  measvuni  34726  eulerpartlemt0  34881  eulerpartlemr  34886  eulerpartlemgf  34891  eulerpartlemgs2  34892  eulerpartlemn  34893  fiblem  34910  oddprm2  35164  bnj1173  35512  bnj1174  35513  bnj1279  35528  elima4  36356  dfon2lem4  36364  ellimits  36488  dfom5b  36490  brapply  36516  brcap  36518  dfrecs2  36530  dfrdg4  36531  finminlem  36938  neibastop2lem  36980  neibastop2  36981  neifg  36991  tailfb  36997  onsucconni  37057  onintopssconn  37060  onsucsuccmpi  37063  limsucncmpi  37065  onint1  37069  mh-infprim2bi  37167  bj-inex1gALT  37669  bj-inrab  37672  bj-rcleqf  37770  bj-restuni  37848  bj-opelresdm  37898  bj-idres  37913  bj-opelidres  37914  bj-eldiag  37929  bj-eldiag2  37930  bj-ccinftydisj  37966  taupilem3  38072  isbasisrelowllem1  38110  isbasisrelowllem2  38111  nlpineqsn  38163  fvineqsneu  38166  ptrest  38369  poimirlem29  38399  poimirlem30  38400  mblfinlem2  38408  mbfposadd  38417  itg2gt0cn  38425  dvasin  38454  inixp  38479  0totbnd  38524  sstotbnd3  38527  heibor1lem  38560  heibor1  38561  heiborlem6  38567  isexid2  38606  smgrpismgmOLD  38613  issmgrpOLD  38614  mndoissmgrpOLD  38619  ismndo  38623  exidresid  38630  rngo1cl  38690  isfld2  38756  ineleq  39103  refressn  39282  eleccossin  39322  elrefsymrelsrel  39404  dfeldisj3  39560  eldisjdmqsim  39566  disjlem14  39650  prtlem14  39748  lshpdisj  39861  lkrin  40038  ishlat1  40226  pmodlem2  40721  pclfinN  40774  pclcmpatN  40775  osumcllem4N  40833  pexmidlem1N  40844  dihmeetlem1N  42164  dihglblem5apreN  42165  dihmeetlem4preN  42180  dihmeetlem13N  42193  dochnel2  42266  lcdlss  42493  mapd1o  42522  baerlem3lem2  42584  baerlem5alem2  42585  baerlem5blem2  42586  redvmptabs  43236  cmpfiiin  43543  mrefg2  43553  fz1eqin  43615  fnwe2lem2  43893  islmodfg  43911  islssfg2  43913  lnr2i  43958  rp-fakeinunass  44356  fiinfi  44414  elinintab  44416  elinintrab  44418  elinlem  44439  cnvcnvintabd  44441  ntrneikb  44935  ntrneik3  44937  ntrneik13  44939  ismnushort  45126  radcnvrat  45139  nzin  45143  onfrALTlem2  45370  onfrALTlem2VD  45712  relpmin  45776  pwclaxpow  45808  dfac5prim  45814  modelac8prim  45816  permac8prim  45838  iooabslt  46330  iccintsng  46354  lptioo2cn  46474  lptioo1cn  46475  cncfuni  46715  icccncfext  46716  stoweidlem44  46873  fourierdlem42  46978  fourierdlem80  47015  sge00  47205  wrddin2  47717  chndin2  47722  chnrin2  47727  eldmressn  47926  afvres  48061  afv2res  48128  prproropf1olem0  48403  31prm  48501  indprmfz  48534  rngccatidALTV  49188  rhmsubcALTVlem3  49199  funcringcsetcALTV2lem7  49212  ringccatidALTV  49222  ringcbasbasALTV  49228  funcringcsetclem7ALTV  49235  fldhmsubcALTV  49249  dfidom2  49259  ssnn0ssfz  49280  elbigo2  49483  itsclinecirc0in  49706  resinsnALT  49800  opndisj  49830  clddisj  49831  i0oii  49847  io1ii  49848