Theorem elin 3927

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3444   ∩ cin 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-in 3918

This theorem is referenced by:  elini  4158  elind  4159  elinel1  4160  elinel2  4161  elin2  4162  elin3  4165  ineqri  4171  nfin  4183  inass  4187  ssin  4198  ssrin  4201  ralin  4208  rexin  4209  dfss4  4228  difin  4231  indi  4243  undi  4244  unineq  4247  indifdi  4253  difin2  4260  inrab2  4276  ndisj  4329  inn0f  4330  difin0ss  4332  inssdif0  4333  inelcm  4424  inundif  4438  elinsn  4670  uniin  4891  intun  4940  intprg  4941  elrint  4949  iunin2  5030  iinin2  5037  elriin  5040  disjor  5084  disjiun  5090  brin  5154  trin  5221  inex1  5267  inuni  5300  wefrc  5625  inopab  5783  inxp  5785  inxpOLD  5786  dmin  5865  dfres3  5944  intasym  6076  asymref  6077  dminss  6114  imainss  6115  inimasn  6117  cnvresima  6191  dfco2a  6207  ordtri3or  6352  2elresin  6621  respreima  7020  fvcofneq  7047  tpres  7157  isomin  7294  isoini  7295  offval  7642  ordpwsuc  7770  frpoins3xpg  8096  frpoins3xp3g  8097  xpord3pred  8108  ressuppss  8139  frrlem13  8254  fprlem1  8256  uniinqs  8747  mapval2  8822  ixpin  8873  boxriin  8890  disjen  9075  ssenen  9092  onfin2  9157  elfpw  9281  fiin  9349  inf3lem2  9558  epfrs  9660  cp  9820  dfac5lem1  10052  dfac5lem5  10056  dfac5  10058  kmlem3  10082  kmlem14  10093  kmlem15  10094  fin23lem26  10254  pwxpndom2  10594  ingru  10744  gruina  10747  grur1  10749  axgroth4  10761  grothprim  10763  ixxdisj  13297  icodisj  13413  fzdisj  13488  nn0disj  13581  fzouzdisj  13632  cotr2g  14918  limsupgle  15419  ello12  15458  elo12  15469  lo1resb  15506  rlimresb  15507  o1resb  15508  lo1eq  15510  rlimeq  15511  fsumsplit  15683  sumsplit  15710  fsum2dlem  15712  fprod2dlem  15922  bitsmod  16382  saddisjlem  16410  sadadd  16413  sadass  16417  smuval2  16428  smupval  16434  smueqlem  16436  smumul  16439  isprm7  16654  prmreclem5  16867  prmrec  16869  4sqlem12  16903  vdwmc  16925  setsstruct2  17120  acsfn  17600  iszeroo  17940  iszeroi  17951  fpwipodrs  18481  psss  18521  insubm  18727  subgacs  19075  nsgacs  19076  resscntz  19247  gsmsymgreq  19346  sylow2a  19533  lsmmod  19589  lsmdisj2  19596  gsumzsplit  19841  subgdmdprd  19950  dprdcntz2  19954  dprddisj2  19955  pgpfac1lem3  19993  rnghmval2  20364  isrhm  20398  subsubrng2  20484  subsubrg2  20519  rnghmsubcsetclem1  20551  funcrngcsetcALT  20561  zrinitorngc  20562  zrtermorngc  20563  rhmsubcsetclem1  20580  rhmsubcrngclem1  20586  ringcbasbas  20593  zrtermoringc  20595  srhmsubclem1  20597  fldhmsubc  20705  acsfn1p  20719  subrgacs  20720  sdrgacs  20721  isorng  20781  lssacs  20905  lspdisj  21067  lspdisjb  21068  dfprm2  21415  irinitoringc  21421  ocvin  21616  unocv  21622  iunocv  21623  obselocv  21670  isassa  21798  aspid  21817  aspval2  21840  pmatcoe1fsupp  22621  isbasis2g  22868  tgval2  22876  tgcl  22889  ppttop  22927  epttop  22929  ssntr  22978  ntreq0  22997  isclo  23007  restntr  23102  restlp  23103  cnpresti  23208  cnprest  23209  cnprest2  23210  lmss  23218  haust1  23272  nrmsep3  23275  isnrm2  23278  lmmo  23300  fincmp  23313  cmpsublem  23319  cmpsub  23320  uncmp  23323  hauscmplem  23326  dfconn2  23339  iunconnlem  23347  unconn  23349  is1stc2  23362  1stcrest  23373  1stcelcls  23381  llyi  23394  nllyi  23395  subislly  23401  lly1stc  23416  txcnp  23540  txcnmpt  23544  hausdiag  23565  kqcldsat  23653  isfbas2  23755  isfil2  23776  fbasfip  23788  elfg  23791  filconn  23803  rnelfmlem  23872  rnelfm  23873  fmfnfmlem2  23875  fmfnfmlem4  23877  fmfnfm  23878  flimrest  23903  hauspwpwf1  23907  fclsrest  23944  alexsubALTlem2  23968  alexsubALTlem3  23969  alexsubALTlem4  23970  alexsubALT  23971  istmd  23994  istgp  23997  tsmssubm  24063  tsmssplit  24072  istrg  24084  istdrg  24086  istlm  24105  ustfilxp  24133  utoptop  24155  utop3cls  24172  bldisj  24319  blin  24342  blres  24352  lpbl  24424  metrest  24445  restmetu  24491  isngp  24517  isnlm  24596  isnmhm  24667  xrtgioo  24728  xrsmopn  24734  icccmplem2  24745  reconnlem2  24749  icoopnst  24869  iocopnst  24870  bndth  24890  zclmncvs  25081  isncvsngp  25082  ncvsprp  25085  ncvsm1  25087  ncvsdif  25088  ncvspi  25089  ncvs1  25090  ncvspds  25094  iscph  25103  tcphcph  25170  cfilfcls  25207  cmetcaulem  25221  isbn  25271  cldcss2  25375  hlhil  25376  ovolfcl  25400  ovolicc2lem2  25452  ovolicc2  25456  shftmbl  25472  volfiniun  25481  mbfmax  25583  mbfimaopnlem  25589  mbfaddlem  25594  i1faddlem  25627  i1fmullem  25628  i1fres  25639  itg1climres  25648  mbfi1fseqlem4  25652  itg2splitlem  25682  itg2split  25683  itgresr  25713  ellimc2  25811  ellimc3  25813  limcun  25829  dvreslem  25843  dvne0  25949  itgsubstlem  25988  ig1pval3  26116  aaliou2  26281  aaliou2b  26282  pilem1  26394  rlimcnp2  26909  fsumharmonic  26955  ppisval2  27048  prmorcht  27121  fsumvma2  27158  pclogsum  27159  vmasum  27160  chpchtsum  27163  chpub  27164  rpvmasum2  27456  madeval2  27798  tglineineq  28623  trlsegvdeg  30206  frgrncvvdeqlem7  30284  frgrncvvdeqlem9  30286  minvecolem1  30853  minvecolem4a  30856  minvecolem4b  30857  minvecolem4  30859  h2hcau  30958  axhcompl-zf  30977  hhcmpl  31179  hhcms  31182  ocin  31275  ocnel  31277  shmodsi  31368  pjhthlem2  31371  omlsilem  31381  pjoc1i  31410  spansnm0i  31629  nonbooli  31630  5oalem7  31639  3oalem3  31643  pjssmii  31660  mayete3i  31707  nmcopex  32008  nmcoplb  32009  lncnopbd  32016  nmcfnex  32032  nmcfnlb  32033  riesz4  32043  riesz1  32044  riesz2  32045  cnlnadjlem3  32048  cnlnadjlem5  32050  cnlnadjlem9  32054  cnlnadjeu  32057  rnbra  32086  pjimai  32155  pjclem4a  32177  pj3lem1  32185  jpi  32249  sumdmdii  32394  sumdmdlem  32397  sumdmdlem2  32398  cdjreui  32411  cdj3lem1  32413  iunin1f  32536  disjorf  32558  ofpreima  32639  1stpreima  32680  2ndpreima  32681  iocinioc2  32752  ssnnssfz  32760  cntzun  33051  kerunit  33290  prmidl0  33414  ressply1mon1p  33530  ccfldextdgrr  33660  crefdf  33831  cmpcref  33833  cmppcmp  33841  cnre2csqima  33894  ordtconnlem1  33907  lmxrge0  33935  isrrext  33983  esum0  34032  esumcst  34046  esumpcvgval  34061  esumcvg  34069  measvuni  34197  eulerpartlemt0  34353  eulerpartlemr  34358  eulerpartlemgf  34363  eulerpartlemgs2  34364  eulerpartlemn  34365  fiblem  34382  oddprm2  34639  bnj1173  34985  bnj1174  34986  bnj1279  35001  elima4  35756  dfon2lem4  35767  ellimits  35891  dfom5b  35893  brapply  35919  brcap  35921  dfrecs2  35931  dfrdg4  35932  finminlem  36299  neibastop2lem  36341  neibastop2  36342  neifg  36352  tailfb  36358  onsucconni  36418  onintopssconn  36421  onsucsuccmpi  36424  limsucncmpi  36426  onint1  36430  bj-inrab  36908  bj-rcleqf  37006  bj-restuni  37078  bj-opelresdm  37126  bj-idres  37141  bj-opelidres  37142  bj-eldiag  37157  bj-eldiag2  37158  bj-ccinftydisj  37194  taupilem3  37300  isbasisrelowllem1  37336  isbasisrelowllem2  37337  nlpineqsn  37389  fvineqsneu  37392  ptrest  37606  poimirlem29  37636  poimirlem30  37637  mblfinlem2  37645  mbfposadd  37654  itg2gt0cn  37662  dvasin  37691  inixp  37715  0totbnd  37760  sstotbnd3  37763  heibor1lem  37796  heibor1  37797  heiborlem6  37803  isexid2  37842  smgrpismgmOLD  37849  issmgrpOLD  37850  mndoissmgrpOLD  37855  ismndo  37859  exidresid  37866  rngo1cl  37926  isfld2  37992  ineleq  38329  refressn  38427  eleccossin  38467  elrefsymrelsrel  38555  dfeldisj3  38704  disjlem14  38783  prtlem14  38860  lshpdisj  38973  lkrin  39150  ishlat1  39338  pmodlem2  39834  pclfinN  39887  pclcmpatN  39888  osumcllem4N  39946  pexmidlem1N  39957  dihmeetlem1N  41277  dihglblem5apreN  41278  dihmeetlem4preN  41293  dihmeetlem13N  41306  dochnel2  41379  lcdlss  41606  mapd1o  41635  baerlem3lem2  41697  baerlem5alem2  41698  baerlem5blem2  41699  redvmptabs  42341  cmpfiiin  42678  mrefg2  42688  fz1eqin  42750  fnwe2lem2  43033  islmodfg  43051  islssfg2  43053  lnr2i  43098  rp-fakeinunass  43497  fiinfi  43555  elinintab  43557  elinintrab  43559  elinlem  43580  cnvcnvintabd  43582  ntrneikb  44076  ntrneik3  44078  ntrneik13  44080  ismnushort  44283  radcnvrat  44296  nzin  44300  onfrALTlem2  44529  onfrALTlem2VD  44871  relpmin  44935  pwclaxpow  44967  dfac5prim  44973  modelac8prim  44975  permac8prim  44997  iooabslt  45490  iccintsng  45514  lptioo2cn  45636  lptioo1cn  45637  cncfuni  45877  icccncfext  45878  stoweidlem44  46035  fourierdlem42  46140  fourierdlem80  46177  sge00  46367  eldmressn  47031  afvres  47166  afv2res  47233  prproropf1olem0  47496  31prm  47591  rngccatidALTV  48253  rhmsubcALTVlem3  48264  funcringcsetcALTV2lem7  48277  ringccatidALTV  48287  ringcbasbasALTV  48293  funcringcsetclem7ALTV  48300  fldhmsubcALTV  48314  ssnn0ssfz  48330  elbigo2  48534  itsclinecirc0in  48757  resinsnALT  48854  opndisj  48884  clddisj  48885  i0oii  48901  io1ii  48902