Theorem elin 3965

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

Syntax hints:   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  Vcvv 3475   ∩ cin 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956

This theorem is referenced by:  dfss2  3969  elini  4194  elind  4195  elinel1  4196  elinel2  4197  elin2  4198  elin3  4201  ineqri  4205  inass  4220  ssin  4231  ssrin  4234  rexin  4240  dfss4  4259  difin  4262  indi  4274  undi  4275  unineq  4278  indifdi  4284  indifdirOLD  4286  difin2  4292  inrab2  4308  ndisj  4368  difin0ss  4369  inssdif0  4370  inelcm  4465  inundif  4479  elinsn  4715  uniin  4936  intun  4985  intprg  4986  intprOLD  4988  elrint  4996  iunin2  5075  iinin2  5082  elriin  5085  disjor  5129  disjiun  5136  brin  5201  trin  5278  inex1  5318  inuni  5344  wefrc  5671  inopab  5830  inxp  5833  dmin  5912  dfres3  5987  intasym  6117  asymref  6118  dminss  6153  imainss  6154  inimasn  6156  cnvresima  6230  dfco2a  6246  ordtri3or  6397  2elresin  6672  respreima  7068  fvcofneq  7095  tpres  7202  isomin  7334  isoini  7335  offval  7679  ordpwsuc  7803  frpoins3xpg  8126  frpoins3xp3g  8127  xpord3pred  8138  ressuppss  8168  frrlem13  8283  fprlem1  8285  wfrlem5OLD  8313  uniinqs  8791  mapval2  8866  ixpin  8917  boxriin  8934  disjen  9134  ssenen  9151  onfin2  9231  elfpw  9354  fiin  9417  inf3lem2  9624  epfrs  9726  cp  9886  dfac5lem1  10118  dfac5lem5  10122  dfac5  10123  kmlem3  10147  kmlem14  10158  kmlem15  10159  fin23lem26  10320  pwxpndom2  10660  ingru  10810  gruina  10813  grur1  10815  axgroth4  10827  grothprim  10829  ixxdisj  13339  icodisj  13453  fzdisj  13528  nn0disj  13617  fzouzdisj  13668  cotr2g  14923  limsupgle  15421  ello12  15460  elo12  15471  lo1resb  15508  rlimresb  15509  o1resb  15510  lo1eq  15512  rlimeq  15513  fsumsplit  15687  sumsplit  15714  fsum2dlem  15716  fprod2dlem  15924  bitsmod  16377  saddisjlem  16405  sadadd  16408  sadass  16412  smuval2  16423  smupval  16429  smueqlem  16431  smumul  16434  isprm7  16645  prmreclem5  16853  prmrec  16855  4sqlem12  16889  vdwmc  16911  setsstruct2  17107  acsfn  17603  iszeroo  17948  iszeroi  17959  fpwipodrs  18493  psss  18533  insubm  18699  subgacs  19041  nsgacs  19042  resscntz  19197  gsmsymgreq  19300  sylow2a  19487  lsmmod  19543  lsmdisj2  19550  gsumzsplit  19795  subgdmdprd  19904  dprdcntz2  19908  dprddisj2  19909  pgpfac1lem3  19947  isrhm  20257  subsubrg2  20346  acsfn1p  20415  subrgacs  20416  sdrgacs  20417  lssacs  20578  lspdisj  20738  lspdisjb  20739  dfprm2  21043  ocvin  21227  unocv  21233  iunocv  21234  obselocv  21283  isassa  21411  aspid  21429  aspval2  21452  pmatcoe1fsupp  22203  isbasis2g  22451  tgval2  22459  tgcl  22472  ppttop  22510  epttop  22512  ssntr  22562  ntreq0  22581  isclo  22591  restntr  22686  restlp  22687  cnpresti  22792  cnprest  22793  cnprest2  22794  lmss  22802  haust1  22856  nrmsep3  22859  isnrm2  22862  lmmo  22884  fincmp  22897  cmpsublem  22903  cmpsub  22904  uncmp  22907  hauscmplem  22910  dfconn2  22923  iunconnlem  22931  unconn  22933  is1stc2  22946  1stcrest  22957  1stcelcls  22965  llyi  22978  nllyi  22979  subislly  22985  lly1stc  23000  txcnp  23124  txcnmpt  23128  hausdiag  23149  kqcldsat  23237  isfbas2  23339  isfil2  23360  fbasfip  23372  elfg  23375  filconn  23387  rnelfmlem  23456  rnelfm  23457  fmfnfmlem2  23459  fmfnfmlem4  23461  fmfnfm  23462  flimrest  23487  hauspwpwf1  23491  fclsrest  23528  alexsubALTlem2  23552  alexsubALTlem3  23553  alexsubALTlem4  23554  alexsubALT  23555  istmd  23578  istgp  23581  tsmssubm  23647  tsmssplit  23656  istrg  23668  istdrg  23670  istlm  23689  ustfilxp  23717  utoptop  23739  utop3cls  23756  bldisj  23904  blin  23927  blres  23937  lpbl  24012  metrest  24033  restmetu  24079  isngp  24105  isnlm  24192  isnmhm  24263  xrtgioo  24322  xrsmopn  24328  icccmplem2  24339  reconnlem2  24343  icoopnst  24455  iocopnst  24456  bndth  24474  zclmncvs  24665  isncvsngp  24666  ncvsprp  24669  ncvsm1  24671  ncvsdif  24672  ncvspi  24673  ncvs1  24674  ncvspds  24678  iscph  24687  tcphcph  24754  cfilfcls  24791  cmetcaulem  24805  isbn  24855  cldcss2  24959  hlhil  24960  ovolfcl  24983  ovolicc2lem2  25035  ovolicc2  25039  shftmbl  25055  volfiniun  25064  mbfmax  25166  mbfimaopnlem  25172  mbfaddlem  25177  i1faddlem  25210  i1fmullem  25211  i1fres  25223  itg1climres  25232  mbfi1fseqlem4  25236  itg2splitlem  25266  itg2split  25267  itgresr  25296  ellimc2  25394  ellimc3  25396  limcun  25412  dvreslem  25426  dvne0  25528  itgsubstlem  25565  ig1pval3  25692  aaliou2  25853  aaliou2b  25854  pilem1  25963  rlimcnp2  26471  fsumharmonic  26516  ppisval2  26609  prmorcht  26682  fsumvma2  26717  pclogsum  26718  vmasum  26719  chpchtsum  26722  chpub  26723  rpvmasum2  27015  madeval2  27348  tglineineq  27894  trlsegvdeg  29480  frgrncvvdeqlem7  29558  frgrncvvdeqlem9  29560  minvecolem1  30127  minvecolem4a  30130  minvecolem4b  30131  minvecolem4  30133  h2hcau  30232  axhcompl-zf  30251  hhcmpl  30453  hhcms  30456  ocin  30549  ocnel  30551  shmodsi  30642  pjhthlem2  30645  omlsilem  30655  pjoc1i  30684  spansnm0i  30903  nonbooli  30904  5oalem7  30913  3oalem3  30917  pjssmii  30934  mayete3i  30981  nmcopex  31282  nmcoplb  31283  lncnopbd  31290  nmcfnex  31306  nmcfnlb  31307  riesz4  31317  riesz1  31318  riesz2  31319  cnlnadjlem3  31322  cnlnadjlem5  31324  cnlnadjlem9  31328  cnlnadjeu  31331  rnbra  31360  pjimai  31429  pjclem4a  31451  pj3lem1  31459  jpi  31523  sumdmdii  31668  sumdmdlem  31671  sumdmdlem2  31672  cdjreui  31685  cdj3lem1  31687  iunin1f  31789  disjorf  31810  ofpreima  31890  1stpreima  31928  2ndpreima  31929  iocinioc2  31990  ssnnssfz  31998  cntzun  32212  isorng  32417  kerunit  32437  prmidl0  32569  ressply1mon1p  32657  ccfldextdgrr  32746  crefdf  32828  cmpcref  32830  cmppcmp  32838  cnre2csqima  32891  ordtconnlem1  32904  lmxrge0  32932  isrrext  32980  esum0  33047  esumcst  33061  esumpcvgval  33076  esumcvg  33084  measvuni  33212  eulerpartlemt0  33368  eulerpartlemr  33373  eulerpartlemgf  33378  eulerpartlemgs2  33379  eulerpartlemn  33380  fiblem  33397  oddprm2  33667  bnj1173  34013  bnj1174  34014  bnj1279  34029  elima4  34747  dfon2lem4  34758  ellimits  34882  dfom5b  34884  brapply  34910  brcap  34912  dfrecs2  34922  dfrdg4  34923  finminlem  35203  neibastop2lem  35245  neibastop2  35246  neifg  35256  tailfb  35262  onsucconni  35322  onintopssconn  35325  onsucsuccmpi  35328  limsucncmpi  35330  onint1  35334  bj-inrab  35807  bj-rcleqf  35906  bj-restuni  35978  bj-opelresdm  36026  bj-idres  36041  bj-opelidres  36042  bj-eldiag  36057  bj-eldiag2  36058  bj-ccinftydisj  36094  taupilem3  36200  isbasisrelowllem1  36236  isbasisrelowllem2  36237  nlpineqsn  36289  fvineqsneu  36292  ptrest  36487  poimirlem29  36517  poimirlem30  36518  mblfinlem2  36526  mbfposadd  36535  itg2gt0cn  36543  dvasin  36572  inixp  36596  0totbnd  36641  sstotbnd3  36644  heibor1lem  36677  heibor1  36678  heiborlem6  36684  isexid2  36723  smgrpismgmOLD  36730  issmgrpOLD  36731  mndoissmgrpOLD  36736  ismndo  36740  exidresid  36747  rngo1cl  36807  isfld2  36873  ralin  37115  ineleq  37223  refressn  37313  eleccossin  37353  elrefsymrelsrel  37441  dfeldisj3  37589  disjlem14  37668  prtlem14  37744  lshpdisj  37857  lkrin  38034  ishlat1  38222  pmodlem2  38718  pclfinN  38771  pclcmpatN  38772  osumcllem4N  38830  pexmidlem1N  38841  dihmeetlem1N  40161  dihglblem5apreN  40162  dihmeetlem4preN  40177  dihmeetlem13N  40190  dochnel2  40263  lcdlss  40490  mapd1o  40519  baerlem3lem2  40581  baerlem5alem2  40582  baerlem5blem2  40583  cmpfiiin  41435  mrefg2  41445  fz1eqin  41507  fnwe2lem2  41793  islmodfg  41811  islssfg2  41813  lnr2i  41858  rp-fakeinunass  42266  fiinfi  42324  elinintab  42326  elinintrab  42328  elinlem  42349  cnvcnvintabd  42351  ntrneikb  42845  ntrneik3  42847  ntrneik13  42849  ismnushort  43060  radcnvrat  43073  nzin  43077  onfrALTlem2  43307  onfrALTlem2VD  43650  inn0f  43760  iooabslt  44212  iccintsng  44236  lptioo2cn  44361  lptioo1cn  44362  cncfuni  44602  icccncfext  44603  stoweidlem44  44760  fourierdlem42  44865  fourierdlem80  44902  sge00  45092  eldmressn  45747  afvres  45880  afv2res  45947  prproropf1olem0  46170  31prm  46265  rnghmval2  46693  subsubrng2  46743  rnghmsubcsetclem1  46873  rngccatidALTV  46887  funcrngcsetcALT  46897  zrinitorngc  46898  zrtermorngc  46899  rhmsubcsetclem1  46919  rhmsubcrngclem1  46925  ringcbasbas  46932  funcringcsetcALTV2lem7  46940  ringccatidALTV  46950  ringcbasbasALTV  46956  funcringcsetclem7ALTV  46963  irinitoringc  46967  zrtermoringc  46968  srhmsubclem1  46971  fldhmsubc  46982  fldhmsubcALTV  47000  rhmsubcALTVlem3  47004  ssnn0ssfz  47025  elbigo2  47238  itsclinecirc0in  47461  opndisj  47535  clddisj  47536  i0oii  47552  io1ii  47553