Theorem elin 3796

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 3212	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 3212	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	adantl 482	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2689	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2689	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	4, 5	anbi12d 747	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
7		df-in 3581	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 3353	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 368	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 196   ∧ wa 384   = wceq 1483   ∈ wcel 1990  Vcvv 3200   ∩ cin 3573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581

This theorem is referenced by:  elini  3797  elind  3798  elinel1  3799  elinel2  3800  elin2  3801  elin3  3804  incom  3805  ineqri  3806  ineq1  3807  inass  3823  ssin  3835  ssrin  3838  dfss4  3858  difin  3861  indi  3873  undi  3874  unineq  3877  indifdir  3883  difin2  3890  inrab2  3900  difin0ss  3946  inssdif0  3947  inelcm  4032  inundif  4046  elinsn  4245  uniin  4457  intun  4509  intpr  4510  elrint  4518  iunin2  4584  iinin2  4590  elriin  4593  disjor  4634  disjiun  4640  brin  4704  trin  4763  inex1  4799  inuni  4826  wefrc  5108  inopab  5252  inxp  5254  dmin  5332  opelres  5401  dfres3  5403  intasym  5511  asymref  5512  dminss  5547  imainss  5548  inimasn  5550  ssrnres  5572  cnvresima  5623  dfco2a  5635  ordtri3or  5755  2elresin  6002  respreima  6344  fvcofneq  6367  tpres  6466  isomin  6587  isoini  6588  offval  6904  ordpwsuc  7015  ressuppss  7314  wfrlem5  7419  erdisj  7794  uniinqs  7827  mapval2  7887  ixpin  7933  boxriin  7950  disjen  8117  ssenen  8134  onfin2  8152  elfpw  8268  fiin  8328  inf3lem2  8526  epfrs  8607  cp  8754  bnd2  8756  dfac5lem1  8946  dfac5lem5  8950  dfac5  8951  kmlem3  8974  kmlem14  8985  kmlem15  8986  fin23lem26  9147  isfin1-3  9208  pwxpndom2  9487  ingru  9637  gruina  9640  grur1  9642  axgroth4  9654  grothprim  9656  ixxdisj  12190  icodisj  12297  fzdisj  12368  uzdisj  12413  nn0disj  12455  fzouzdisj  12504  xpcogend  13713  cotr2g  13715  limsupgle  14208  ello12  14247  elo12  14258  lo1resb  14295  rlimresb  14296  o1resb  14297  lo1eq  14299  rlimeq  14300  fsumsplit  14471  sumsplit  14499  fsum2dlem  14501  explecnv  14597  fprod2dlem  14710  bitsmod  15158  saddisjlem  15186  sadadd  15189  sadass  15193  smuval2  15204  smupval  15210  smueqlem  15212  smumul  15215  isprm7  15420  prmreclem5  15624  prmrec  15626  4sqlem12  15660  vdwmc  15682  setsstruct2  15896  acsfn  16320  iszeroo  16652  iszeroi  16659  isdrs2  16939  fpwipodrs  17164  psss  17214  subgacs  17629  nsgacs  17630  resscntz  17764  gsmsymgreq  17852  sylow2a  18034  lsmmod  18088  lsmdisj2  18095  gsumzsplit  18327  subgdmdprd  18433  dprdcntz2  18437  dprddisj2  18438  pgpfac1lem3  18476  isrhm  18721  subsubrg2  18807  lssacs  18967  lspdisj  19125  lspdisjb  19126  isassa  19315  aspid  19330  aspval2  19347  dfprm2  19842  ocvin  20018  unocv  20024  iunocv  20025  obselocv  20072  pmatcoe1fsupp  20506  isbasis2g  20752  tgval2  20760  tgcl  20773  ppttop  20811  epttop  20813  clsval2  20854  ssntr  20862  ntreq0  20881  isclo  20891  restntr  20986  restlp  20987  cnpresti  21092  cnprest  21093  cnprest2  21094  lmss  21102  haust1  21156  nrmsep3  21159  isnrm2  21162  lmmo  21184  fincmp  21196  0cmp  21197  discmp  21201  cmpsublem  21202  cmpsub  21203  uncmp  21206  hauscmplem  21209  dfconn2  21222  iunconnlem  21230  unconn  21232  is1stc2  21245  1stcrest  21256  1stcelcls  21264  llyi  21277  nllyi  21278  subislly  21284  lly1stc  21299  comppfsc  21335  txcnp  21423  txcnmpt  21427  hausdiag  21448  kqcldsat  21536  ptcmpfi  21616  isfbas2  21639  isfil2  21660  fbasfip  21672  elfg  21675  filconn  21687  rnelfmlem  21756  rnelfm  21757  fmfnfmlem2  21759  fmfnfmlem4  21761  fmfnfm  21762  flimrest  21787  hauspwpwf1  21791  fclsrest  21828  alexsubALTlem2  21852  alexsubALTlem3  21853  alexsubALTlem4  21854  alexsubALT  21855  ptcmp  21862  istmd  21878  istgp  21881  tsmssubm  21946  tsmssplit  21955  istrg  21967  istdrg  21969  istlm  21988  ustfilxp  22016  utoptop  22038  utop3cls  22055  bldisj  22203  blin  22226  blin2  22234  blres  22236  lpbl  22308  metrest  22329  restmetu  22375  isngp  22400  isnlm  22479  isnmhm  22550  xrtgioo  22609  xrsmopn  22615  icccmplem2  22626  reconnlem2  22630  icoopnst  22738  iocopnst  22739  bndth  22757  cvsi  22930  cnstrcvs  22941  cncvs  22945  zclmncvs  22948  isncvsngp  22949  ncvsprp  22952  ncvsm1  22954  ncvsdif  22955  ncvspi  22956  ncvs1  22957  ncvspds  22961  iscph  22970  tchcph  23036  cfilfcls  23072  cmetcaulem  23086  cmetss  23113  isbn  23135  cldcss2  23213  hlhil  23214  ovolfcl  23235  ovolicc1  23284  ovolicc2lem2  23286  ovolicc2lem4  23288  ovolicc2lem5  23289  ovolicc2  23290  shftmbl  23306  volfiniun  23315  ioorf  23341  mbfmax  23416  mbfimaopnlem  23422  mbfaddlem  23427  mbfadd  23428  mbfsub  23429  i1faddlem  23460  i1fmullem  23461  i1fres  23472  itg1climres  23481  mbfi1fseqlem4  23485  mbfmul  23493  itg2splitlem  23515  itg2split  23516  itgresr  23545  bddmulibl  23605  ellimc2  23641  ellimc3  23643  limcun  23659  dvreslem  23673  dvne0  23774  itgsubstlem  23811  ig1pval3  23934  aaliou2  24095  aaliou2b  24096  pilem1  24205  rlimcnp2  24693  fsumharmonic  24738  ppisval2  24831  prmorcht  24904  fsumvma2  24939  pclogsum  24940  vmasum  24941  chpchtsum  24944  chpub  24945  chebbnd1lem1  25158  rpvmasum2  25201  tglineineq  25538  trlsegvdeg  27087  frgrncvvdeqlem7  27169  frgrncvvdeqlem9  27171  minvecolem1  27730  minvecolem4a  27733  minvecolem4b  27734  minvecolem4  27736  h2hcau  27836  axhcompl-zf  27855  hhcmpl  28057  hhcms  28060  ocin  28155  ocnel  28157  shmodsi  28248  pjhthlem2  28251  omlsilem  28261  pjoc1i  28290  spansnm0i  28509  nonbooli  28510  5oalem7  28519  3oalem3  28523  pjssmii  28540  mayete3i  28587  nmcopex  28888  nmcoplb  28889  lncnopbd  28896  nmcfnex  28912  nmcfnlb  28913  riesz4  28923  riesz1  28924  riesz2  28925  cnlnadjlem3  28928  cnlnadjlem5  28930  cnlnadjlem9  28934  cnlnadjeu  28937  rnbra  28966  pjimai  29035  pjclem4a  29057  pj3lem1  29065  jpi  29129  sumdmdii  29274  sumdmdlem  29277  sumdmdlem2  29278  cdjreui  29291  cdj3lem1  29293  iunin1f  29374  disjorf  29392  ofpreima  29465  1stpreima  29484  2ndpreima  29485  iocinioc2  29541  ssnnssfz  29549  isorng  29799  kerunit  29823  crefdf  29915  cmpcref  29917  cmppcmp  29925  pcmplfin  29927  cnre2csqima  29957  ordtconnlem1  29970  lmxrge0  29998  isrrext  30044  esum0  30111  esumcst  30125  esumpcvgval  30140  esumcvg  30148  measvuni  30277  eulerpartlemt0  30431  eulerpartlemr  30436  eulerpartlemgf  30441  eulerpartlemgs2  30442  eulerpartlemn  30443  sseqf  30454  fiblem  30460  oddprm2  30733  bnj521  30805  bnj1173  31070  bnj1174  31071  bnj1279  31086  elima4  31679  imaindm  31682  dfon2lem4  31691  frrlem5  31784  madeval2  31936  ellimits  32017  dfom5b  32019  brapply  32045  brcap  32047  dfrecs2  32057  dfrdg4  32058  finminlem  32312  neibastop2lem  32355  neibastop2  32356  neifg  32366  tailfb  32372  onsucconni  32436  onintopssconn  32439  onsucsuccmpi  32442  limsucncmpi  32444  onint1  32448  bj-inrab  32923  bj-restuni  33050  bj-eldiag  33091  bj-eldiag2  33092  bj-ccinftydisj  33100  taupilem3  33165  isbasisrelowllem1  33203  isbasisrelowllem2  33204  ptrest  33408  poimirlem29  33438  poimirlem30  33439  mblfinlem2  33447  mbfposadd  33457  itg2gt0cn  33465  dvasin  33496  inixp  33523  0totbnd  33572  sstotbnd3  33575  heibor1lem  33608  heibor1  33609  heiborlem6  33615  isexid2  33654  smgrpismgmOLD  33661  issmgrpOLD  33662  mndoissmgrpOLD  33667  ismndo  33671  exidresid  33678  rngo1cl  33738  isfld2  33804  ineleq  34119  prtlem14  34159  lshpdisj  34274  lkrin  34451  ishlat1  34639  pmodlem2  35133  pclfinN  35186  pclcmpatN  35187  osumcllem4N  35245  pexmidlem1N  35256  dihmeetlem1N  36579  dihglblem5apreN  36580  dihmeetlem4preN  36595  dihmeetlem13N  36608  dochnel2  36681  lcdlss  36908  mapd1o  36937  baerlem3lem2  36999  baerlem5alem2  37000  baerlem5blem2  37001  cmpfiiin  37260  mrefg2  37270  fz1eqin  37332  fnwe2lem2  37621  islmodfg  37639  islssfg2  37641  lnr2i  37686  acsfn1p  37769  subrgacs  37770  sdrgacs  37771  rp-fakeinunass  37861  fiinfi  37878  elinintab  37881  elinintrab  37883  elinlem  37904  cnvcnvintabd  37906  ndisj  38063  ntrneikb  38392  ntrneik3  38394  ntrneik13  38396  radcnvrat  38513  nzin  38517  onfrALTlem2  38761  onfrALTlem2VD  39125  inn0f  39242  iooabslt  39721  iccintsng  39749  lptioo2cn  39877  lptioo1cn  39878  cncfuni  40099  icccncfext  40100  stoweidlem44  40261  fourierdlem42  40366  fourierdlem80  40403  sge00  40593  eldmressn  41203  afvres  41252  31prm  41512  rnghmval2  41895  rnghmsubcsetclem1  41975  rngccatidALTV  41989  funcrngcsetcALT  41999  zrinitorngc  42000  zrtermorngc  42001  rhmsubcsetclem1  42021  rhmsubcrngclem1  42027  ringcbasbas  42034  funcringcsetcALTV2lem7  42042  ringccatidALTV  42052  ringcbasbasALTV  42058  funcringcsetclem7ALTV  42065  irinitoringc  42069  zrtermoringc  42070  srhmsubclem1  42073  fldhmsubc  42084  fldhmsubcALTV  42102  rhmsubcALTVlem3  42106  ssnn0ssfz  42127  elbigo2  42346