Theorem elin 3964

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 3492	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 3492	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	adantl 481	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2820	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2820	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	4, 5	anbi12d 630	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
7		df-in 3955	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 3670	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 378	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 205   ∧ wa 395   = wceq 1540   ∈ wcel 2105  Vcvv 3473   ∩ cin 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3955

This theorem is referenced by:  dfss2  3968  elini  4193  elind  4194  elinel1  4195  elinel2  4196  elin2  4197  elin3  4200  ineqri  4204  inass  4219  ssin  4230  ssrin  4233  rexin  4239  dfss4  4258  difin  4261  indi  4273  undi  4274  unineq  4277  indifdi  4283  indifdirOLD  4285  difin2  4291  inrab2  4307  ndisj  4367  difin0ss  4368  inssdif0  4369  inelcm  4464  inundif  4478  elinsn  4714  uniin  4935  intun  4984  intprg  4985  intprOLD  4987  elrint  4995  iunin2  5074  iinin2  5081  elriin  5084  disjor  5128  disjiun  5135  brin  5200  trin  5277  inex1  5317  inuni  5343  wefrc  5670  inopab  5829  inxp  5832  dmin  5911  dfres3  5986  intasym  6116  asymref  6117  dminss  6152  imainss  6153  inimasn  6155  cnvresima  6229  dfco2a  6245  ordtri3or  6396  2elresin  6671  respreima  7067  fvcofneq  7094  tpres  7204  isomin  7337  isoini  7338  offval  7683  ordpwsuc  7807  frpoins3xpg  8131  frpoins3xp3g  8132  xpord3pred  8143  ressuppss  8173  frrlem13  8289  fprlem1  8291  wfrlem5OLD  8319  uniinqs  8797  mapval2  8872  ixpin  8923  boxriin  8940  disjen  9140  ssenen  9157  onfin2  9237  elfpw  9360  fiin  9423  inf3lem2  9630  epfrs  9732  cp  9892  dfac5lem1  10124  dfac5lem5  10128  dfac5  10129  kmlem3  10153  kmlem14  10164  kmlem15  10165  fin23lem26  10326  pwxpndom2  10666  ingru  10816  gruina  10819  grur1  10821  axgroth4  10833  grothprim  10835  ixxdisj  13346  icodisj  13460  fzdisj  13535  nn0disj  13624  fzouzdisj  13675  cotr2g  14930  limsupgle  15428  ello12  15467  elo12  15478  lo1resb  15515  rlimresb  15516  o1resb  15517  lo1eq  15519  rlimeq  15520  fsumsplit  15694  sumsplit  15721  fsum2dlem  15723  fprod2dlem  15931  bitsmod  16384  saddisjlem  16412  sadadd  16415  sadass  16419  smuval2  16430  smupval  16436  smueqlem  16438  smumul  16441  isprm7  16652  prmreclem5  16860  prmrec  16862  4sqlem12  16896  vdwmc  16918  setsstruct2  17114  acsfn  17610  iszeroo  17955  iszeroi  17966  fpwipodrs  18500  psss  18540  insubm  18738  subgacs  19081  nsgacs  19082  resscntz  19242  gsmsymgreq  19345  sylow2a  19532  lsmmod  19588  lsmdisj2  19595  gsumzsplit  19840  subgdmdprd  19949  dprdcntz2  19953  dprddisj2  19954  pgpfac1lem3  19992  rnghmval2  20339  isrhm  20373  subsubrng2  20456  subsubrg2  20493  acsfn1p  20562  subrgacs  20563  sdrgacs  20564  lssacs  20726  lspdisj  20887  lspdisjb  20888  dfprm2  21248  ocvin  21450  unocv  21456  iunocv  21457  obselocv  21506  isassa  21634  aspid  21652  aspval2  21675  pmatcoe1fsupp  22436  isbasis2g  22684  tgval2  22692  tgcl  22705  ppttop  22743  epttop  22745  ssntr  22795  ntreq0  22814  isclo  22824  restntr  22919  restlp  22920  cnpresti  23025  cnprest  23026  cnprest2  23027  lmss  23035  haust1  23089  nrmsep3  23092  isnrm2  23095  lmmo  23117  fincmp  23130  cmpsublem  23136  cmpsub  23137  uncmp  23140  hauscmplem  23143  dfconn2  23156  iunconnlem  23164  unconn  23166  is1stc2  23179  1stcrest  23190  1stcelcls  23198  llyi  23211  nllyi  23212  subislly  23218  lly1stc  23233  txcnp  23357  txcnmpt  23361  hausdiag  23382  kqcldsat  23470  isfbas2  23572  isfil2  23593  fbasfip  23605  elfg  23608  filconn  23620  rnelfmlem  23689  rnelfm  23690  fmfnfmlem2  23692  fmfnfmlem4  23694  fmfnfm  23695  flimrest  23720  hauspwpwf1  23724  fclsrest  23761  alexsubALTlem2  23785  alexsubALTlem3  23786  alexsubALTlem4  23787  alexsubALT  23788  istmd  23811  istgp  23814  tsmssubm  23880  tsmssplit  23889  istrg  23901  istdrg  23903  istlm  23922  ustfilxp  23950  utoptop  23972  utop3cls  23989  bldisj  24137  blin  24160  blres  24170  lpbl  24245  metrest  24266  restmetu  24312  isngp  24338  isnlm  24425  isnmhm  24496  xrtgioo  24555  xrsmopn  24561  icccmplem2  24572  reconnlem2  24576  icoopnst  24696  iocopnst  24697  bndth  24717  zclmncvs  24909  isncvsngp  24910  ncvsprp  24913  ncvsm1  24915  ncvsdif  24916  ncvspi  24917  ncvs1  24918  ncvspds  24922  iscph  24931  tcphcph  24998  cfilfcls  25035  cmetcaulem  25049  isbn  25099  cldcss2  25203  hlhil  25204  ovolfcl  25228  ovolicc2lem2  25280  ovolicc2  25284  shftmbl  25300  volfiniun  25309  mbfmax  25411  mbfimaopnlem  25417  mbfaddlem  25422  i1faddlem  25455  i1fmullem  25456  i1fres  25468  itg1climres  25477  mbfi1fseqlem4  25481  itg2splitlem  25511  itg2split  25512  itgresr  25541  ellimc2  25639  ellimc3  25641  limcun  25657  dvreslem  25671  dvne0  25777  itgsubstlem  25814  ig1pval3  25941  aaliou2  26103  aaliou2b  26104  pilem1  26214  rlimcnp2  26722  fsumharmonic  26767  ppisval2  26860  prmorcht  26933  fsumvma2  26968  pclogsum  26969  vmasum  26970  chpchtsum  26973  chpub  26974  rpvmasum2  27266  madeval2  27600  tglineineq  28176  trlsegvdeg  29762  frgrncvvdeqlem7  29840  frgrncvvdeqlem9  29842  minvecolem1  30409  minvecolem4a  30412  minvecolem4b  30413  minvecolem4  30415  h2hcau  30514  axhcompl-zf  30533  hhcmpl  30735  hhcms  30738  ocin  30831  ocnel  30833  shmodsi  30924  pjhthlem2  30927  omlsilem  30937  pjoc1i  30966  spansnm0i  31185  nonbooli  31186  5oalem7  31195  3oalem3  31199  pjssmii  31216  mayete3i  31263  nmcopex  31564  nmcoplb  31565  lncnopbd  31572  nmcfnex  31588  nmcfnlb  31589  riesz4  31599  riesz1  31600  riesz2  31601  cnlnadjlem3  31604  cnlnadjlem5  31606  cnlnadjlem9  31610  cnlnadjeu  31613  rnbra  31642  pjimai  31711  pjclem4a  31733  pj3lem1  31741  jpi  31805  sumdmdii  31950  sumdmdlem  31953  sumdmdlem2  31954  cdjreui  31967  cdj3lem1  31969  iunin1f  32071  disjorf  32092  ofpreima  32172  1stpreima  32210  2ndpreima  32211  iocinioc2  32272  ssnnssfz  32280  cntzun  32497  isorng  32702  kerunit  32722  prmidl0  32858  ressply1mon1p  32946  ccfldextdgrr  33050  crefdf  33141  cmpcref  33143  cmppcmp  33151  cnre2csqima  33204  ordtconnlem1  33217  lmxrge0  33245  isrrext  33293  esum0  33360  esumcst  33374  esumpcvgval  33389  esumcvg  33397  measvuni  33525  eulerpartlemt0  33681  eulerpartlemr  33686  eulerpartlemgf  33691  eulerpartlemgs2  33692  eulerpartlemn  33693  fiblem  33710  oddprm2  33980  bnj1173  34326  bnj1174  34327  bnj1279  34342  elima4  35066  dfon2lem4  35077  ellimits  35201  dfom5b  35203  brapply  35229  brcap  35231  dfrecs2  35241  dfrdg4  35242  finminlem  35519  neibastop2lem  35561  neibastop2  35562  neifg  35572  tailfb  35578  onsucconni  35638  onintopssconn  35641  onsucsuccmpi  35644  limsucncmpi  35646  onint1  35650  bj-inrab  36123  bj-rcleqf  36222  bj-restuni  36294  bj-opelresdm  36342  bj-idres  36357  bj-opelidres  36358  bj-eldiag  36373  bj-eldiag2  36374  bj-ccinftydisj  36410  taupilem3  36516  isbasisrelowllem1  36552  isbasisrelowllem2  36553  nlpineqsn  36605  fvineqsneu  36608  ptrest  36803  poimirlem29  36833  poimirlem30  36834  mblfinlem2  36842  mbfposadd  36851  itg2gt0cn  36859  dvasin  36888  inixp  36912  0totbnd  36957  sstotbnd3  36960  heibor1lem  36993  heibor1  36994  heiborlem6  37000  isexid2  37039  smgrpismgmOLD  37046  issmgrpOLD  37047  mndoissmgrpOLD  37052  ismndo  37056  exidresid  37063  rngo1cl  37123  isfld2  37189  ralin  37431  ineleq  37539  refressn  37629  eleccossin  37669  elrefsymrelsrel  37757  dfeldisj3  37905  disjlem14  37984  prtlem14  38060  lshpdisj  38173  lkrin  38350  ishlat1  38538  pmodlem2  39034  pclfinN  39087  pclcmpatN  39088  osumcllem4N  39146  pexmidlem1N  39157  dihmeetlem1N  40477  dihglblem5apreN  40478  dihmeetlem4preN  40493  dihmeetlem13N  40506  dochnel2  40579  lcdlss  40806  mapd1o  40835  baerlem3lem2  40897  baerlem5alem2  40898  baerlem5blem2  40899  cmpfiiin  41750  mrefg2  41760  fz1eqin  41822  fnwe2lem2  42108  islmodfg  42126  islssfg2  42128  lnr2i  42173  rp-fakeinunass  42581  fiinfi  42639  elinintab  42641  elinintrab  42643  elinlem  42664  cnvcnvintabd  42666  ntrneikb  43160  ntrneik3  43162  ntrneik13  43164  ismnushort  43375  radcnvrat  43388  nzin  43392  onfrALTlem2  43622  onfrALTlem2VD  43965  inn0f  44074  iooabslt  44523  iccintsng  44547  lptioo2cn  44672  lptioo1cn  44673  cncfuni  44913  icccncfext  44914  stoweidlem44  45071  fourierdlem42  45176  fourierdlem80  45213  sge00  45403  eldmressn  46058  afvres  46191  afv2res  46258  prproropf1olem0  46481  31prm  46576  rnghmsubcsetclem1  46974  rngccatidALTV  46988  funcrngcsetcALT  46998  zrinitorngc  46999  zrtermorngc  47000  rhmsubcsetclem1  47020  rhmsubcrngclem1  47026  ringcbasbas  47033  funcringcsetcALTV2lem7  47041  ringccatidALTV  47051  ringcbasbasALTV  47057  funcringcsetclem7ALTV  47064  irinitoringc  47068  zrtermoringc  47069  srhmsubclem1  47072  fldhmsubc  47083  fldhmsubcALTV  47101  rhmsubcALTVlem3  47105  ssnn0ssfz  47126  elbigo2  47338  itsclinecirc0in  47561  opndisj  47635  clddisj  47636  i0oii  47652  io1ii  47653