Theorem elin 3978

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1536   ∈ wcel 2105  Vcvv 3477   ∩ cin 3961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-in 3969

This theorem is referenced by:  elini  4208  elind  4209  elinel1  4210  elinel2  4211  elin2  4212  elin3  4215  ineqri  4219  nfin  4231  inass  4235  ssin  4246  ssrin  4249  rexin  4255  dfss4  4274  difin  4277  indi  4289  undi  4290  unineq  4293  indifdi  4299  difin2  4306  inrab2  4322  ndisj  4375  inn0f  4376  difin0ss  4378  inssdif0  4379  inelcm  4470  inundif  4484  elinsn  4714  uniin  4935  intun  4984  intprg  4985  elrint  4993  iunin2  5075  iinin2  5082  elriin  5085  disjor  5129  disjiun  5135  brin  5199  trin  5276  inex1  5322  inuni  5355  wefrc  5682  inopab  5841  inxp  5844  inxpOLD  5845  dmin  5924  dfres3  6004  intasym  6137  asymref  6138  dminss  6174  imainss  6175  inimasn  6177  cnvresima  6251  dfco2a  6267  ordtri3or  6417  2elresin  6689  respreima  7085  fvcofneq  7112  tpres  7220  isomin  7356  isoini  7357  offval  7705  ordpwsuc  7834  frpoins3xpg  8163  frpoins3xp3g  8164  xpord3pred  8175  ressuppss  8206  frrlem13  8321  fprlem1  8323  wfrlem5OLD  8351  uniinqs  8835  mapval2  8910  ixpin  8961  boxriin  8978  disjen  9172  ssenen  9189  onfin2  9265  elfpw  9391  fiin  9459  inf3lem2  9666  epfrs  9768  cp  9928  dfac5lem1  10160  dfac5lem5  10164  dfac5  10166  kmlem3  10190  kmlem14  10201  kmlem15  10202  fin23lem26  10362  pwxpndom2  10702  ingru  10852  gruina  10855  grur1  10857  axgroth4  10869  grothprim  10871  ixxdisj  13398  icodisj  13512  fzdisj  13587  nn0disj  13680  fzouzdisj  13731  cotr2g  15011  limsupgle  15509  ello12  15548  elo12  15559  lo1resb  15596  rlimresb  15597  o1resb  15598  lo1eq  15600  rlimeq  15601  fsumsplit  15773  sumsplit  15800  fsum2dlem  15802  fprod2dlem  16012  bitsmod  16469  saddisjlem  16497  sadadd  16500  sadass  16504  smuval2  16515  smupval  16521  smueqlem  16523  smumul  16526  isprm7  16741  prmreclem5  16953  prmrec  16955  4sqlem12  16989  vdwmc  17011  setsstruct2  17207  acsfn  17703  iszeroo  18051  iszeroi  18062  fpwipodrs  18597  psss  18637  insubm  18843  subgacs  19191  nsgacs  19192  resscntz  19363  gsmsymgreq  19464  sylow2a  19651  lsmmod  19707  lsmdisj2  19714  gsumzsplit  19959  subgdmdprd  20068  dprdcntz2  20072  dprddisj2  20073  pgpfac1lem3  20111  rnghmval2  20460  isrhm  20494  subsubrng2  20580  subsubrg2  20615  rnghmsubcsetclem1  20647  funcrngcsetcALT  20657  zrinitorngc  20658  zrtermorngc  20659  rhmsubcsetclem1  20676  rhmsubcrngclem1  20682  ringcbasbas  20689  zrtermoringc  20691  srhmsubclem1  20693  fldhmsubc  20802  acsfn1p  20816  subrgacs  20817  sdrgacs  20818  lssacs  20982  lspdisj  21144  lspdisjb  21145  dfprm2  21501  irinitoringc  21507  ocvin  21709  unocv  21715  iunocv  21716  obselocv  21765  isassa  21893  aspid  21912  aspval2  21935  pmatcoe1fsupp  22722  isbasis2g  22970  tgval2  22978  tgcl  22991  ppttop  23029  epttop  23031  ssntr  23081  ntreq0  23100  isclo  23110  restntr  23205  restlp  23206  cnpresti  23311  cnprest  23312  cnprest2  23313  lmss  23321  haust1  23375  nrmsep3  23378  isnrm2  23381  lmmo  23403  fincmp  23416  cmpsublem  23422  cmpsub  23423  uncmp  23426  hauscmplem  23429  dfconn2  23442  iunconnlem  23450  unconn  23452  is1stc2  23465  1stcrest  23476  1stcelcls  23484  llyi  23497  nllyi  23498  subislly  23504  lly1stc  23519  txcnp  23643  txcnmpt  23647  hausdiag  23668  kqcldsat  23756  isfbas2  23858  isfil2  23879  fbasfip  23891  elfg  23894  filconn  23906  rnelfmlem  23975  rnelfm  23976  fmfnfmlem2  23978  fmfnfmlem4  23980  fmfnfm  23981  flimrest  24006  hauspwpwf1  24010  fclsrest  24047  alexsubALTlem2  24071  alexsubALTlem3  24072  alexsubALTlem4  24073  alexsubALT  24074  istmd  24097  istgp  24100  tsmssubm  24166  tsmssplit  24175  istrg  24187  istdrg  24189  istlm  24208  ustfilxp  24236  utoptop  24258  utop3cls  24275  bldisj  24423  blin  24446  blres  24456  lpbl  24531  metrest  24552  restmetu  24598  isngp  24624  isnlm  24711  isnmhm  24782  xrtgioo  24841  xrsmopn  24847  icccmplem2  24858  reconnlem2  24862  icoopnst  24982  iocopnst  24983  bndth  25003  zclmncvs  25195  isncvsngp  25196  ncvsprp  25199  ncvsm1  25201  ncvsdif  25202  ncvspi  25203  ncvs1  25204  ncvspds  25208  iscph  25217  tcphcph  25284  cfilfcls  25321  cmetcaulem  25335  isbn  25385  cldcss2  25489  hlhil  25490  ovolfcl  25514  ovolicc2lem2  25566  ovolicc2  25570  shftmbl  25586  volfiniun  25595  mbfmax  25697  mbfimaopnlem  25703  mbfaddlem  25708  i1faddlem  25741  i1fmullem  25742  i1fres  25754  itg1climres  25763  mbfi1fseqlem4  25767  itg2splitlem  25797  itg2split  25798  itgresr  25828  ellimc2  25926  ellimc3  25928  limcun  25944  dvreslem  25958  dvne0  26064  itgsubstlem  26103  ig1pval3  26231  aaliou2  26396  aaliou2b  26397  pilem1  26509  rlimcnp2  27023  fsumharmonic  27069  ppisval2  27162  prmorcht  27235  fsumvma2  27272  pclogsum  27273  vmasum  27274  chpchtsum  27277  chpub  27278  rpvmasum2  27570  madeval2  27906  tglineineq  28665  trlsegvdeg  30255  frgrncvvdeqlem7  30333  frgrncvvdeqlem9  30335  minvecolem1  30902  minvecolem4a  30905  minvecolem4b  30906  minvecolem4  30908  h2hcau  31007  axhcompl-zf  31026  hhcmpl  31228  hhcms  31231  ocin  31324  ocnel  31326  shmodsi  31417  pjhthlem2  31420  omlsilem  31430  pjoc1i  31459  spansnm0i  31678  nonbooli  31679  5oalem7  31688  3oalem3  31692  pjssmii  31709  mayete3i  31756  nmcopex  32057  nmcoplb  32058  lncnopbd  32065  nmcfnex  32081  nmcfnlb  32082  riesz4  32092  riesz1  32093  riesz2  32094  cnlnadjlem3  32097  cnlnadjlem5  32099  cnlnadjlem9  32103  cnlnadjeu  32106  rnbra  32135  pjimai  32204  pjclem4a  32226  pj3lem1  32234  jpi  32298  sumdmdii  32443  sumdmdlem  32446  sumdmdlem2  32447  cdjreui  32460  cdj3lem1  32462  iunin1f  32577  disjorf  32598  ofpreima  32681  1stpreima  32721  2ndpreima  32722  iocinioc2  32787  ssnnssfz  32795  cntzun  33053  isorng  33308  kerunit  33328  prmidl0  33457  ressply1mon1p  33572  ccfldextdgrr  33696  crefdf  33808  cmpcref  33810  cmppcmp  33818  cnre2csqima  33871  ordtconnlem1  33884  lmxrge0  33912  isrrext  33962  esum0  34029  esumcst  34043  esumpcvgval  34058  esumcvg  34066  measvuni  34194  eulerpartlemt0  34350  eulerpartlemr  34355  eulerpartlemgf  34360  eulerpartlemgs2  34361  eulerpartlemn  34362  fiblem  34379  oddprm2  34648  bnj1173  34994  bnj1174  34995  bnj1279  35010  elima4  35756  dfon2lem4  35767  ellimits  35891  dfom5b  35893  brapply  35919  brcap  35921  dfrecs2  35931  dfrdg4  35932  finminlem  36300  neibastop2lem  36342  neibastop2  36343  neifg  36353  tailfb  36359  onsucconni  36419  onintopssconn  36422  onsucsuccmpi  36425  limsucncmpi  36427  onint1  36431  bj-inrab  36909  bj-rcleqf  37007  bj-restuni  37079  bj-opelresdm  37127  bj-idres  37142  bj-opelidres  37143  bj-eldiag  37158  bj-eldiag2  37159  bj-ccinftydisj  37195  taupilem3  37301  isbasisrelowllem1  37337  isbasisrelowllem2  37338  nlpineqsn  37390  fvineqsneu  37393  ptrest  37605  poimirlem29  37635  poimirlem30  37636  mblfinlem2  37644  mbfposadd  37653  itg2gt0cn  37661  dvasin  37690  inixp  37714  0totbnd  37759  sstotbnd3  37762  heibor1lem  37795  heibor1  37796  heiborlem6  37802  isexid2  37841  smgrpismgmOLD  37848  issmgrpOLD  37849  mndoissmgrpOLD  37854  ismndo  37858  exidresid  37865  rngo1cl  37925  isfld2  37991  ralin  38229  ineleq  38335  refressn  38424  eleccossin  38464  elrefsymrelsrel  38552  dfeldisj3  38700  disjlem14  38779  prtlem14  38855  lshpdisj  38968  lkrin  39145  ishlat1  39333  pmodlem2  39829  pclfinN  39882  pclcmpatN  39883  osumcllem4N  39941  pexmidlem1N  39952  dihmeetlem1N  41272  dihglblem5apreN  41273  dihmeetlem4preN  41288  dihmeetlem13N  41301  dochnel2  41374  lcdlss  41601  mapd1o  41630  baerlem3lem2  41692  baerlem5alem2  41693  baerlem5blem2  41694  redvmptabs  42368  cmpfiiin  42684  mrefg2  42694  fz1eqin  42756  fnwe2lem2  43039  islmodfg  43057  islssfg2  43059  lnr2i  43104  rp-fakeinunass  43504  fiinfi  43562  elinintab  43564  elinintrab  43566  elinlem  43587  cnvcnvintabd  43589  ntrneikb  44083  ntrneik3  44085  ntrneik13  44087  ismnushort  44296  radcnvrat  44309  nzin  44313  onfrALTlem2  44543  onfrALTlem2VD  44886  iooabslt  45451  iccintsng  45475  lptioo2cn  45600  lptioo1cn  45601  cncfuni  45841  icccncfext  45842  stoweidlem44  45999  fourierdlem42  46104  fourierdlem80  46141  sge00  46331  eldmressn  46986  afvres  47121  afv2res  47188  prproropf1olem0  47426  31prm  47521  rngccatidALTV  48115  rhmsubcALTVlem3  48126  funcringcsetcALTV2lem7  48139  ringccatidALTV  48149  ringcbasbasALTV  48155  funcringcsetclem7ALTV  48162  fldhmsubcALTV  48176  ssnn0ssfz  48193  elbigo2  48401  itsclinecirc0in  48624  opndisj  48698  clddisj  48699  i0oii  48715  io1ii  48716