Theorem elin 3758

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 3185	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 3185	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	adantl 481	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2676	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2676	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	4, 5	anbi12d 743	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
7		df-in 3547	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 3322	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 367	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  Vcvv 3173   ∩ cin 3539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547

This theorem is referenced by:  elini  3759  elind  3760  elinel1  3761  elinel2  3762  elin2  3763  elin3  3766  incom  3767  ineqri  3768  ineq1  3769  inass  3785  ssin  3797  ssrin  3800  dfss4  3820  difin  3823  indi  3832  undi  3833  unineq  3836  indifdir  3842  difin2  3849  inrab2  3859  difin0ss  3900  inssdif0  3901  inelcm  3984  inundif  3998  uniin  4393  intun  4444  intpr  4445  elrint  4453  iunin2  4520  iinin2  4526  elriin  4529  disjor  4567  disjiun  4573  brin  4634  trin  4691  inex1  4727  inuni  4753  wefrc  5032  inopab  5174  inxp  5176  dmin  5254  opelres  5322  intasym  5430  asymref  5431  dminss  5466  imainss  5467  inimasn  5469  ssrnres  5491  cnvresima  5541  dfco2a  5552  ordtri3or  5672  2elresin  5916  respreima  6252  fvcofneq  6275  tpres  6371  isomin  6487  isoini  6488  offval  6802  ordpwsuc  6907  ressuppss  7201  wfrlem5  7306  erdisj  7681  uniinqs  7714  mapval2  7773  ixpin  7819  boxriin  7836  disjen  8002  ssenen  8019  onfin2  8037  elfpw  8151  fiin  8211  inf3lem2  8409  epfrs  8490  cp  8637  bnd2  8639  dfac5lem1  8829  dfac5lem5  8833  dfac5  8834  kmlem3  8857  kmlem14  8868  kmlem15  8869  fin23lem26  9030  isfin1-3  9091  pwxpndom2  9366  ingru  9516  gruina  9519  grur1  9521  axgroth4  9533  grothprim  9535  ixxdisj  12061  icodisj  12168  fzdisj  12239  uzdisj  12282  nn0disj  12324  fzouzdisj  12373  xpcogend  13561  cotr2g  13563  limsupgle  14056  ello12  14095  elo12  14106  lo1resb  14143  rlimresb  14144  o1resb  14145  lo1eq  14147  rlimeq  14148  fsumsplit  14318  sumsplit  14341  fsum2dlem  14343  explecnv  14436  fprod2dlem  14549  bitsmod  14996  saddisjlem  15024  sadadd  15027  sadass  15031  smuval2  15042  smupval  15048  smueqlem  15050  smumul  15053  isprm7  15258  prmreclem5  15462  prmrec  15464  4sqlem12  15498  vdwmc  15520  acsfn  16143  iszeroo  16475  iszeroi  16482  isdrs2  16762  fpwipodrs  16987  psss  17037  subgacs  17452  nsgacs  17453  resscntz  17587  gsmsymgreq  17675  sylow2a  17857  lsmmod  17911  lsmdisj2  17918  gsumzsplit  18150  subgdmdprd  18256  dprdcntz2  18260  dprddisj2  18261  pgpfac1lem3  18299  isrhm  18544  subsubrg2  18630  lssacs  18788  lspdisj  18946  lspdisjb  18947  isassa  19136  aspid  19151  aspval2  19168  dfprm2  19661  ocvin  19837  unocv  19843  iunocv  19844  obselocv  19891  pmatcoe1fsupp  20325  isbasis2g  20563  tgval2  20571  tgcl  20584  ppttop  20621  epttop  20623  clsval2  20664  ssntr  20672  ntreq0  20691  isclo  20701  restntr  20796  restlp  20797  cnpresti  20902  cnprest  20903  cnprest2  20904  lmss  20912  haust1  20966  nrmsep3  20969  isnrm2  20972  lmmo  20994  fincmp  21006  0cmp  21007  discmp  21011  cmpsublem  21012  cmpsub  21013  uncmp  21016  hauscmplem  21019  dfcon2  21032  iunconlem  21040  uncon  21042  is1stc2  21055  1stcrest  21066  1stcelcls  21074  llyi  21087  nllyi  21088  subislly  21094  lly1stc  21109  comppfsc  21145  txcnp  21233  txcnmpt  21237  hausdiag  21258  kqcldsat  21346  ptcmpfi  21426  isfbas2  21449  isfil2  21470  fbasfip  21482  elfg  21485  filcon  21497  rnelfmlem  21566  rnelfm  21567  fmfnfmlem2  21569  fmfnfmlem4  21571  fmfnfm  21572  flimrest  21597  hauspwpwf1  21601  fclsrest  21638  alexsubALTlem2  21662  alexsubALTlem3  21663  alexsubALTlem4  21664  alexsubALT  21665  ptcmp  21672  istmd  21688  istgp  21691  tsmssubm  21756  tsmssplit  21765  istrg  21777  istdrg  21779  istlm  21798  ustfilxp  21826  utoptop  21848  utop3cls  21865  bldisj  22013  blin  22036  blin2  22044  blres  22046  lpbl  22118  metrest  22139  restmetu  22185  isngp  22210  isnlm  22289  isnmhm  22360  xrtgioo  22417  xrsmopn  22423  icccmplem2  22434  reconnlem2  22438  icoopnst  22546  iocopnst  22547  bndth  22565  cvsi  22738  cnstrcvs  22749  cncvs  22753  zclmncvs  22756  isncvsngp  22757  ncvsprp  22760  ncvsm1  22762  ncvsdif  22763  ncvspi  22764  ncvs1  22765  ncvspds  22769  iscph  22778  tchcph  22844  cfilfcls  22880  cmetcaulem  22894  cmetss  22921  isbn  22943  cldcss2  23021  hlhil  23022  ovolfcl  23042  ovolicc1  23091  ovolicc2lem2  23093  ovolicc2lem4  23095  ovolicc2lem5  23096  ovolicc2  23097  shftmbl  23113  volfiniun  23122  ioorf  23147  mbfmax  23222  mbfimaopnlem  23228  mbfaddlem  23233  mbfadd  23234  mbfsub  23235  i1faddlem  23266  i1fmullem  23267  i1fres  23278  itg1climres  23287  mbfi1fseqlem4  23291  mbfmul  23299  itg2splitlem  23321  itg2split  23322  itgresr  23351  bddmulibl  23411  ellimc2  23447  ellimc3  23449  limcun  23465  dvreslem  23479  dvne0  23578  itgsubstlem  23615  ig1pval3  23738  aaliou2  23899  aaliou2b  23900  pilem1  24009  rlimcnp2  24493  fsumharmonic  24538  ppisval2  24631  prmorcht  24704  fsumvma2  24739  pclogsum  24740  vmasum  24741  chpchtsum  24744  chpub  24745  chebbnd1lem1  24958  rpvmasum2  25001  tglineineq  25338  frgrancvvdeqlem4  26560  frgrancvvdeqlem7  26563  frgrancvvdeqlemA  26564  frgrancvvdeqlemC  26566  minvecolem1  27114  minvecolem4a  27117  minvecolem4b  27118  minvecolem4  27120  h2hcau  27220  axhcompl-zf  27239  hhcmpl  27441  hhcms  27444  ocin  27539  ocnel  27541  shmodsi  27632  pjhthlem2  27635  omlsilem  27645  pjoc1i  27674  spansnm0i  27893  nonbooli  27894  5oalem7  27903  3oalem3  27907  pjssmii  27924  mayete3i  27971  nmcopex  28272  nmcoplb  28273  lncnopbd  28280  nmcfnex  28296  nmcfnlb  28297  riesz4  28307  riesz1  28308  riesz2  28309  cnlnadjlem3  28312  cnlnadjlem5  28314  cnlnadjlem9  28318  cnlnadjeu  28321  rnbra  28350  pjimai  28419  pjclem4a  28441  pj3lem1  28449  jpi  28513  sumdmdii  28658  sumdmdlem  28661  sumdmdlem2  28662  cdjreui  28675  cdj3lem1  28677  iunin1f  28757  disjorf  28774  ofpreima  28848  1stpreima  28867  2ndpreima  28868  iocinioc2  28931  ssnnssfz  28937  isorng  29130  kerunit  29154  crefdf  29243  cmpcref  29245  cmppcmp  29253  pcmplfin  29255  cnre2csqima  29285  ordtconlem1  29298  lmxrge0  29326  isrrext  29372  esum0  29438  esumcst  29452  esumpcvgval  29467  esumcvg  29475  measvuni  29604  eulerpartlemt0  29758  eulerpartlemr  29763  eulerpartlemgf  29768  eulerpartlemgs2  29769  eulerpartlemn  29770  sseqf  29781  fiblem  29787  bnj521  30059  bnj1172  30323  bnj1173  30324  bnj1174  30325  bnj1279  30340  dfres3  30902  elima4  30924  dfon2lem4  30935  frrlem5  31028  ellimits  31187  dfom5b  31189  brapply  31215  brcap  31217  dfrecs2  31227  dfrdg4  31228  finminlem  31482  neibastop2lem  31525  neibastop2  31526  neifg  31536  tailfb  31542  onsucconi  31606  onintopsscon  31609  onsucsuccmpi  31612  limsucncmpi  31614  onint1  31618  bj-inrab  32115  bj-restuni  32231  bj-eldiag  32268  bj-eldiag2  32269  bj-ccinftydisj  32277  taupilem3  32342  isbasisrelowllem1  32379  isbasisrelowllem2  32380  ptrest  32578  poimirlem29  32608  poimirlem30  32609  mblfinlem2  32617  mbfposadd  32627  itg2gt0cn  32635  dvasin  32666  inixp  32693  0totbnd  32742  sstotbnd3  32745  heibor1lem  32778  heibor1  32779  heiborlem6  32785  isexid2  32824  smgrpismgmOLD  32831  issmgrpOLD  32832  mndoissmgrpOLD  32837  mndoisexid  32838  ismndo  32841  exidresid  32848  rngo1cl  32908  isfld2  32974  prtlem14  33177  lshpdisj  33292  lkrin  33469  ishlat1  33657  pmodlem2  34151  pclfinN  34204  pclcmpatN  34205  osumcllem4N  34263  pexmidlem1N  34274  dihmeetlem1N  35597  dihglblem5apreN  35598  dihmeetlem4preN  35613  dihmeetlem13N  35626  dochnel2  35699  lcdlss  35926  mapd1o  35955  baerlem3lem2  36017  baerlem5alem2  36018  baerlem5blem2  36019  cmpfiiin  36278  mrefg2  36288  fz1eqin  36350  fnwe2lem2  36639  islmodfg  36657  islssfg2  36659  lnr2i  36705  acsfn1p  36788  subrgacs  36789  sdrgacs  36790  rp-fakeinunass  36880  fiinfi  36897  elinintab  36900  elinintrab  36902  elinlem  36923  cnvcnvintabd  36925  ndisj  37083  ntrneikb  37412  ntrneik3  37414  ntrneik13  37416  radcnvrat  37535  nzin  37539  onfrALTlem2  37782  onfrALTlem2VD  38147  inn0f  38268  iooabslt  38568  iccintsng  38596  lptioo2cn  38712  lptioo1cn  38713  cncfuni  38772  icccncfext  38773  stoweidlem44  38937  fourierdlem42  39042  fourierdlem80  39079  sge00  39269  eldmressn  39852  afvres  39901  31prm  40050  trlsegvdeg  41395  frgrncvvdeqlem4  41472  frgrncvvdeqlem7  41475  frgrncvvdeqlemA  41476  frgrncvvdeqlemC  41478  rnghmval2  41685  rnghmsubcsetclem1  41767  rngccatidALTV  41781  funcrngcsetcALT  41791  zrinitorngc  41792  zrtermorngc  41793  rhmsubcsetclem1  41813  rhmsubcrngclem1  41819  ringcbasbas  41826  funcringcsetcALTV2lem7  41834  ringccatidALTV  41844  ringcbasbasALTV  41850  funcringcsetclem7ALTV  41857  irinitoringc  41861  zrtermoringc  41862  srhmsubclem1  41865  fldhmsubc  41876  srhmsubcALTVlem1  41884  fldhmsubcALTV  41895  rhmsubcALTVlem3  41899  ssnn0ssfz  41920  elbigo2  42144