Theorem elin 3903

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 3450	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 3450	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	adantl 482	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2826	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2826	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	4, 5	anbi12d 631	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
7		df-in 3894	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 3611	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 380	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2106  Vcvv 3432   ∩ cin 3886

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894

This theorem is referenced by:  dfss2  3907  elini  4127  elind  4128  elinel1  4129  elinel2  4130  elin2  4131  elin3  4134  ineqri  4138  inass  4153  ssin  4164  ssrin  4167  rexin  4173  dfss4  4192  difin  4195  indi  4207  undi  4208  unineq  4211  indifdi  4217  indifdirOLD  4219  difin2  4225  inrab2  4241  ndisj  4301  difin0ss  4302  inssdif0  4303  inelcm  4398  inundif  4412  elinsn  4646  uniin  4865  intun  4911  intprg  4912  intprOLD  4914  elrint  4922  iunin2  5000  iinin2  5007  elriin  5010  disjor  5054  disjiun  5061  brin  5126  trin  5201  inex1  5241  inuni  5267  wefrc  5583  inopab  5739  inxp  5741  dmin  5820  dfres3  5896  intasym  6020  asymref  6021  dminss  6056  imainss  6057  inimasn  6059  cnvresima  6133  dfco2a  6150  ordtri3or  6298  2elresin  6553  respreima  6943  fvcofneq  6969  tpres  7076  isomin  7208  isoini  7209  offval  7542  ordpwsuc  7662  ressuppss  7999  frrlem13  8114  fprlem1  8116  wfrlem5OLD  8144  uniinqs  8586  mapval2  8660  ixpin  8711  boxriin  8728  disjen  8921  ssenen  8938  onfin2  9014  elfpw  9121  fiin  9181  inf3lem2  9387  epfrs  9489  cp  9649  dfac5lem1  9879  dfac5lem5  9883  dfac5  9884  kmlem3  9908  kmlem14  9919  kmlem15  9920  fin23lem26  10081  pwxpndom2  10421  ingru  10571  gruina  10574  grur1  10576  axgroth4  10588  grothprim  10590  ixxdisj  13094  icodisj  13208  fzdisj  13283  nn0disj  13372  fzouzdisj  13423  cotr2g  14687  limsupgle  15186  ello12  15225  elo12  15236  lo1resb  15273  rlimresb  15274  o1resb  15275  lo1eq  15277  rlimeq  15278  fsumsplit  15453  sumsplit  15480  fsum2dlem  15482  fprod2dlem  15690  bitsmod  16143  saddisjlem  16171  sadadd  16174  sadass  16178  smuval2  16189  smupval  16195  smueqlem  16197  smumul  16200  isprm7  16413  prmreclem5  16621  prmrec  16623  4sqlem12  16657  vdwmc  16679  setsstruct2  16875  acsfn  17368  iszeroo  17713  iszeroi  17724  fpwipodrs  18258  psss  18298  insubm  18457  subgacs  18789  nsgacs  18790  resscntz  18938  gsmsymgreq  19040  sylow2a  19224  lsmmod  19281  lsmdisj2  19288  gsumzsplit  19528  subgdmdprd  19637  dprdcntz2  19641  dprddisj2  19642  pgpfac1lem3  19680  isrhm  19965  subsubrg2  20051  acsfn1p  20067  subrgacs  20068  sdrgacs  20069  lssacs  20229  lspdisj  20387  lspdisjb  20388  dfprm2  20695  ocvin  20879  unocv  20885  iunocv  20886  obselocv  20935  isassa  21063  aspid  21079  aspval2  21102  pmatcoe1fsupp  21850  isbasis2g  22098  tgval2  22106  tgcl  22119  ppttop  22157  epttop  22159  ssntr  22209  ntreq0  22228  isclo  22238  restntr  22333  restlp  22334  cnpresti  22439  cnprest  22440  cnprest2  22441  lmss  22449  haust1  22503  nrmsep3  22506  isnrm2  22509  lmmo  22531  fincmp  22544  cmpsublem  22550  cmpsub  22551  uncmp  22554  hauscmplem  22557  dfconn2  22570  iunconnlem  22578  unconn  22580  is1stc2  22593  1stcrest  22604  1stcelcls  22612  llyi  22625  nllyi  22626  subislly  22632  lly1stc  22647  txcnp  22771  txcnmpt  22775  hausdiag  22796  kqcldsat  22884  isfbas2  22986  isfil2  23007  fbasfip  23019  elfg  23022  filconn  23034  rnelfmlem  23103  rnelfm  23104  fmfnfmlem2  23106  fmfnfmlem4  23108  fmfnfm  23109  flimrest  23134  hauspwpwf1  23138  fclsrest  23175  alexsubALTlem2  23199  alexsubALTlem3  23200  alexsubALTlem4  23201  alexsubALT  23202  istmd  23225  istgp  23228  tsmssubm  23294  tsmssplit  23303  istrg  23315  istdrg  23317  istlm  23336  ustfilxp  23364  utoptop  23386  utop3cls  23403  bldisj  23551  blin  23574  blres  23584  lpbl  23659  metrest  23680  restmetu  23726  isngp  23752  isnlm  23839  isnmhm  23910  xrtgioo  23969  xrsmopn  23975  icccmplem2  23986  reconnlem2  23990  icoopnst  24102  iocopnst  24103  bndth  24121  zclmncvs  24312  isncvsngp  24313  ncvsprp  24316  ncvsm1  24318  ncvsdif  24319  ncvspi  24320  ncvs1  24321  ncvspds  24325  iscph  24334  tcphcph  24401  cfilfcls  24438  cmetcaulem  24452  isbn  24502  cldcss2  24606  hlhil  24607  ovolfcl  24630  ovolicc2lem2  24682  ovolicc2  24686  shftmbl  24702  volfiniun  24711  mbfmax  24813  mbfimaopnlem  24819  mbfaddlem  24824  i1faddlem  24857  i1fmullem  24858  i1fres  24870  itg1climres  24879  mbfi1fseqlem4  24883  itg2splitlem  24913  itg2split  24914  itgresr  24943  ellimc2  25041  ellimc3  25043  limcun  25059  dvreslem  25073  dvne0  25175  itgsubstlem  25212  ig1pval3  25339  aaliou2  25500  aaliou2b  25501  pilem1  25610  rlimcnp2  26116  fsumharmonic  26161  ppisval2  26254  prmorcht  26327  fsumvma2  26362  pclogsum  26363  vmasum  26364  chpchtsum  26367  chpub  26368  rpvmasum2  26660  tglineineq  27004  trlsegvdeg  28591  frgrncvvdeqlem7  28669  frgrncvvdeqlem9  28671  minvecolem1  29236  minvecolem4a  29239  minvecolem4b  29240  minvecolem4  29242  h2hcau  29341  axhcompl-zf  29360  hhcmpl  29562  hhcms  29565  ocin  29658  ocnel  29660  shmodsi  29751  pjhthlem2  29754  omlsilem  29764  pjoc1i  29793  spansnm0i  30012  nonbooli  30013  5oalem7  30022  3oalem3  30026  pjssmii  30043  mayete3i  30090  nmcopex  30391  nmcoplb  30392  lncnopbd  30399  nmcfnex  30415  nmcfnlb  30416  riesz4  30426  riesz1  30427  riesz2  30428  cnlnadjlem3  30431  cnlnadjlem5  30433  cnlnadjlem9  30437  cnlnadjeu  30440  rnbra  30469  pjimai  30538  pjclem4a  30560  pj3lem1  30568  jpi  30632  sumdmdii  30777  sumdmdlem  30780  sumdmdlem2  30781  cdjreui  30794  cdj3lem1  30796  iunin1f  30897  disjorf  30918  ofpreima  31002  1stpreima  31039  2ndpreima  31040  iocinioc2  31100  ssnnssfz  31108  cntzun  31320  isorng  31498  kerunit  31522  prmidl0  31626  ccfldextdgrr  31742  crefdf  31798  cmpcref  31800  cmppcmp  31808  cnre2csqima  31861  ordtconnlem1  31874  lmxrge0  31902  isrrext  31950  esum0  32017  esumcst  32031  esumpcvgval  32046  esumcvg  32054  measvuni  32182  eulerpartlemt0  32336  eulerpartlemr  32341  eulerpartlemgf  32346  eulerpartlemgs2  32347  eulerpartlemn  32348  fiblem  32365  oddprm2  32635  bnj521  32716  bnj1173  32982  bnj1174  32983  bnj1279  32998  elima4  33750  dfon2lem4  33762  frpoins3xpg  33787  frpoins3xp3g  33788  xpord3pred  33798  madeval2  34037  ellimits  34212  dfom5b  34214  brapply  34240  brcap  34242  dfrecs2  34252  dfrdg4  34253  finminlem  34507  neibastop2lem  34549  neibastop2  34550  neifg  34560  tailfb  34566  onsucconni  34626  onintopssconn  34629  onsucsuccmpi  34632  limsucncmpi  34634  onint1  34638  bj-inrab  35115  bj-rcleqf  35215  bj-restuni  35268  bj-opelresdm  35316  bj-idres  35331  bj-opelidres  35332  bj-eldiag  35347  bj-eldiag2  35348  bj-ccinftydisj  35384  taupilem3  35490  isbasisrelowllem1  35526  isbasisrelowllem2  35527  nlpineqsn  35579  fvineqsneu  35582  ptrest  35776  poimirlem29  35806  poimirlem30  35807  mblfinlem2  35815  mbfposadd  35824  itg2gt0cn  35832  dvasin  35861  inixp  35886  0totbnd  35931  sstotbnd3  35934  heibor1lem  35967  heibor1  35968  heiborlem6  35974  isexid2  36013  smgrpismgmOLD  36020  issmgrpOLD  36021  mndoissmgrpOLD  36026  ismndo  36030  exidresid  36037  rngo1cl  36097  isfld2  36163  ineleq  36486  eleccossin  36601  elrefsymrelsrel  36685  dfeldisj3  36830  prtlem14  36888  lshpdisj  37001  lkrin  37178  ishlat1  37366  pmodlem2  37861  pclfinN  37914  pclcmpatN  37915  osumcllem4N  37973  pexmidlem1N  37984  dihmeetlem1N  39304  dihglblem5apreN  39305  dihmeetlem4preN  39320  dihmeetlem13N  39333  dochnel2  39406  lcdlss  39633  mapd1o  39662  baerlem3lem2  39724  baerlem5alem2  39725  baerlem5blem2  39726  mhphf  40285  cmpfiiin  40519  mrefg2  40529  fz1eqin  40591  fnwe2lem2  40876  islmodfg  40894  islssfg2  40896  lnr2i  40941  rp-fakeinunass  41122  fiinfi  41180  elinintab  41183  elinintrab  41185  elinlem  41206  cnvcnvintabd  41208  ntrneikb  41704  ntrneik3  41706  ntrneik13  41708  ismnushort  41919  radcnvrat  41932  nzin  41936  onfrALTlem2  42166  onfrALTlem2VD  42509  inn0f  42621  iooabslt  43037  iccintsng  43061  lptioo2cn  43186  lptioo1cn  43187  cncfuni  43427  icccncfext  43428  stoweidlem44  43585  fourierdlem42  43690  fourierdlem80  43727  sge00  43914  eldmressn  44531  afvres  44664  afv2res  44731  prproropf1olem0  44954  31prm  45049  rnghmval2  45453  rnghmsubcsetclem1  45533  rngccatidALTV  45547  funcrngcsetcALT  45557  zrinitorngc  45558  zrtermorngc  45559  rhmsubcsetclem1  45579  rhmsubcrngclem1  45585  ringcbasbas  45592  funcringcsetcALTV2lem7  45600  ringccatidALTV  45610  ringcbasbasALTV  45616  funcringcsetclem7ALTV  45623  irinitoringc  45627  zrtermoringc  45628  srhmsubclem1  45631  fldhmsubc  45642  fldhmsubcALTV  45660  rhmsubcALTVlem3  45664  ssnn0ssfz  45685  elbigo2  45898  itsclinecirc0in  46121  opndisj  46196  clddisj  46197  i0oii  46213  io1ii  46214