Theorem elin 3929

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 3484	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 3484	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	adantl 486	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2857	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2857	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	4, 5	anbi12d 643	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
7		df-in 3920	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 3648	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 381	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  Vcvv 3463   ∩ cin 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-in 3920

This theorem is referenced by:  elini  4160  elind  4161  elinel1  4162  elinel2  4163  elin2  4164  elin3  4167  ineqri  4173  nfin  4185  inass  4188  ssin  4199  ssrin  4202  ralin  4210  rexin  4211  dfss4  4230  difin  4233  indi  4245  undi  4246  unineq  4249  indifdi  4255  difin2  4262  inrab2  4278  ndisj  4333  inn0f  4334  difin0ss  4336  inssdif0  4337  inelcm  4431  inundif  4445  elinsn  4681  uniinOLD  4901  intun  4949  intprg  4950  elrint  4958  iunin2  5039  iinin2  5048  elriin  5051  disjor  5095  disjiun  5101  brin  5167  trin  5234  inex1  5288  inuni  5321  wefrc  5656  inopab  5817  inxp  5819  dmin  5902  dfres3  5984  intasym  6116  asymref  6117  dminss  6151  imainss  6152  inimasn  6154  cnvresima  6232  dfco2a  6248  ordtri3or  6394  2elresin  6657  respreima  7062  fvcofneq  7089  tpres  7200  isomin  7336  isoini  7337  offval  7684  ordpwsuc  7811  frpoins3xpg  8136  frpoins3xp3g  8137  xpord3pred  8148  ressuppss  8179  frrlem13  8295  fprlem1  8297  uniinqs  8795  mapval2  8870  ixpin  8921  boxriin  8938  disjen  9122  ssenen  9139  onfin2  9201  elfpw  9311  fiin  9382  inf3lem2  9598  epfrs  9700  cp  9877  dfac5lem1  10107  dfac5lem5  10111  dfac5  10112  kmlem3  10136  kmlem14  10147  kmlem15  10148  fin23lem26  10309  pwxpndom2  10650  ingru  10800  gruina  10803  grur1  10805  axgroth4  10817  grothprim  10819  ixxdisj  13387  icodisj  13503  fzdisj  13579  nn0disj  13672  fzouzdisj  13724  cotr2g  15013  limsupgle  15528  ello12  15567  elo12  15578  lo1resb  15615  rlimresb  15616  o1resb  15617  lo1eq  15619  rlimeq  15620  fsumsplit  15792  sumsplit  15819  fsum2dlem  15821  fprod2dlem  16034  bitsmod  16494  saddisjlem  16522  sadadd  16525  sadass  16529  smuval2  16540  smupval  16546  smueqlem  16548  smumul  16551  isprm7  16767  prmreclem5  16980  prmrec  16982  4sqlem12  17016  vdwmc  17038  setsstruct2  17234  acsfn  17715  iszeroo  18055  iszeroi  18066  fpwipodrs  18596  psss  18636  insubm  18877  subgacs  19227  nsgacs  19228  resscntz  19403  gsmsymgreq  19502  sylow2a  19689  lsmmod  19745  lsmdisj2  19752  gsumzsplit  19997  subgdmdprd  20106  dprdcntz2  20110  dprddisj2  20111  pgpfac1lem3  20149  rnghmval2  20526  isrhm  20560  subsubrng2  20649  subsubrg2  20684  rnghmsubcsetclem1  20716  funcrngcsetcALT  20726  zrinitorngc  20727  zrtermorngc  20728  rhmsubcsetclem1  20745  rhmsubcrngclem1  20751  ringcbasbas  20758  zrtermoringc  20760  srhmsubclem1  20762  fldhmsubc  20866  acsfn1p  20880  subrgacs  20881  sdrgacs  20882  isorng  20942  lssacs  21066  lspdisj  21227  lspdisjb  21228  prmidl0  21447  dfprm2  21592  irinitoringc  21598  ocvin  21793  unocv  21799  iunocv  21800  obselocv  21847  isassa  21975  aspid  21993  aspval2  22017  pmatcoe1fsupp  22827  isbasis2g  23074  tgval2  23082  tgcl  23095  ppttop  23133  epttop  23135  ssntr  23184  ntreq0  23203  isclo  23213  restntr  23308  restlp  23309  cnpresti  23414  cnprest  23415  cnprest2  23416  lmss  23424  haust1  23478  nrmsep3  23481  isnrm2  23484  lmmo  23506  fincmp  23519  cmpsublem  23525  cmpsub  23526  uncmp  23529  hauscmplem  23532  dfconn2  23545  iunconnlem  23553  unconn  23555  is1stc2  23568  1stcrest  23579  1stcelcls  23587  llyi  23600  nllyi  23601  subislly  23607  lly1stc  23622  txcnp  23746  txcnmpt  23750  hausdiag  23771  kqcldsat  23859  isfbas2  23961  isfil2  23982  fbasfip  23994  elfg  23997  filconn  24009  rnelfmlem  24078  rnelfm  24079  fmfnfmlem2  24081  fmfnfmlem4  24083  fmfnfm  24084  flimrest  24109  hauspwpwf1  24113  fclsrest  24150  alexsubALTlem2  24174  alexsubALTlem3  24175  alexsubALTlem4  24176  alexsubALT  24177  istmd  24200  istgp  24203  tsmssubm  24269  tsmssplit  24278  istrg  24290  istdrg  24292  istlm  24311  ustfilxp  24339  utoptop  24360  utop3cls  24377  bldisj  24524  blin  24547  blres  24557  lpbl  24629  metrest  24650  restmetu  24696  isngp  24722  isnlm  24801  isnmhm  24872  xrtgioo  24933  xrsmopn  24939  icccmplem2  24950  reconnlem2  24954  icoopnst  25067  iocopnst  25068  bndth  25086  zclmncvs  25276  isncvsngp  25277  ncvsprp  25280  ncvsm1  25282  ncvsdif  25283  ncvspi  25284  ncvs1  25285  ncvspds  25289  iscph  25298  tcphcph  25365  cfilfcls  25402  cmetcaulem  25416  isbn  25466  cldcss2  25570  hlhil  25571  ovolfcl  25594  ovolicc2lem2  25646  ovolicc2  25650  shftmbl  25666  volfiniun  25675  mbfmax  25777  mbfimaopnlem  25783  mbfaddlem  25788  i1faddlem  25821  i1fmullem  25822  i1fres  25833  itg1climres  25842  mbfi1fseqlem4  25846  itg2splitlem  25876  itg2split  25877  itgresr  25907  ellimc2  26005  ellimc3  26007  limcun  26023  dvreslem  26037  dvne0  26139  itgsubstlem  26176  ig1pval3  26304  aaliou2  26470  aaliou2b  26471  pilem1  26580  rlimcnp2  27097  fsumharmonic  27142  ppisval2  27235  prmorcht  27308  fsumvma2  27344  pclogsum  27345  vmasum  27346  chpchtsum  27349  chpub  27350  rpvmasum2  27642  madeval2  27992  tglineineq  28878  trlsegvdeg  30519  frgrncvvdeqlem7  30597  frgrncvvdeqlem9  30599  minvecolem1  31167  minvecolem4a  31170  minvecolem4b  31171  minvecolem4  31173  h2hcau  31272  axhcompl-zf  31291  hhcmpl  31493  hhcms  31496  ocin  31589  ocnel  31591  shmodsi  31682  pjhthlem2  31685  omlsilem  31695  pjoc1i  31724  spansnm0i  31943  nonbooli  31944  5oalem7  31953  3oalem3  31957  pjssmii  31974  mayete3i  32021  nmcopex  32322  nmcoplb  32323  lncnopbd  32330  nmcfnex  32346  nmcfnlb  32347  riesz4  32357  riesz1  32358  riesz2  32359  cnlnadjlem3  32362  cnlnadjlem5  32364  cnlnadjlem9  32368  cnlnadjeu  32371  rnbra  32400  pjimai  32469  pjclem4a  32491  pj3lem1  32499  jpi  32563  sumdmdii  32708  sumdmdlem  32711  sumdmdlem2  32712  cdjreui  32725  cdj3lem1  32727  iunin1f  32843  disjorf  32865  ofpreima  32951  1stpreima  32993  2ndpreima  32994  iocinioc2  33065  ssnnssfz  33073  cntzun  33340  kerunit  33588  ressply1mon1p  33803  ccfldextdgrr  34007  crefdf  34183  cmpcref  34185  cmppcmp  34193  cnre2csqima  34246  ordtconnlem1  34259  lmxrge0  34287  isrrext  34335  esum0  34384  esumcst  34398  esumpcvgval  34413  esumcvg  34421  measvuni  34549  eulerpartlemt0  34704  eulerpartlemr  34709  eulerpartlemgf  34714  eulerpartlemgs2  34715  eulerpartlemn  34716  fiblem  34733  oddprm2  34987  bnj1173  35335  bnj1174  35336  bnj1279  35351  elima4  36167  dfon2lem4  36175  ellimits  36299  dfom5b  36301  brapply  36327  brcap  36329  dfrecs2  36341  dfrdg4  36342  finminlem  36718  neibastop2lem  36760  neibastop2  36761  neifg  36771  tailfb  36777  onsucconni  36837  onintopssconn  36840  onsucsuccmpi  36843  limsucncmpi  36845  onint1  36849  mh-infprim2bi  36947  bj-inrab  37451  bj-rcleqf  37549  bj-restuni  37627  bj-opelresdm  37677  bj-idres  37692  bj-opelidres  37693  bj-eldiag  37708  bj-eldiag2  37709  bj-ccinftydisj  37745  taupilem3  37851  isbasisrelowllem1  37889  isbasisrelowllem2  37890  nlpineqsn  37942  fvineqsneu  37945  ptrest  38158  poimirlem29  38188  poimirlem30  38189  mblfinlem2  38197  mbfposadd  38206  itg2gt0cn  38214  dvasin  38243  inixp  38267  0totbnd  38312  sstotbnd3  38315  heibor1lem  38348  heibor1  38349  heiborlem6  38355  isexid2  38394  smgrpismgmOLD  38401  issmgrpOLD  38402  mndoissmgrpOLD  38407  ismndo  38411  exidresid  38418  rngo1cl  38478  isfld2  38544  ineleq  38893  refressn  39072  eleccossin  39112  elrefsymrelsrel  39194  dfeldisj3  39350  eldisjdmqsim  39356  disjlem14  39440  prtlem14  39538  lshpdisj  39651  lkrin  39828  ishlat1  40016  pmodlem2  40511  pclfinN  40564  pclcmpatN  40565  osumcllem4N  40623  pexmidlem1N  40634  dihmeetlem1N  41954  dihglblem5apreN  41955  dihmeetlem4preN  41970  dihmeetlem13N  41983  dochnel2  42056  lcdlss  42283  mapd1o  42312  baerlem3lem2  42374  baerlem5alem2  42375  baerlem5blem2  42376  redvmptabs  43011  cmpfiiin  43320  mrefg2  43330  fz1eqin  43392  fnwe2lem2  43670  islmodfg  43688  islssfg2  43690  lnr2i  43735  rp-fakeinunass  44133  fiinfi  44191  elinintab  44193  elinintrab  44195  elinlem  44216  cnvcnvintabd  44218  ntrneikb  44712  ntrneik3  44714  ntrneik13  44716  ismnushort  44903  radcnvrat  44916  nzin  44920  onfrALTlem2  45147  onfrALTlem2VD  45489  relpmin  45553  pwclaxpow  45585  dfac5prim  45591  modelac8prim  45593  permac8prim  45615  iooabslt  46107  iccintsng  46131  lptioo2cn  46251  lptioo1cn  46252  cncfuni  46492  icccncfext  46493  stoweidlem44  46650  fourierdlem42  46755  fourierdlem80  46792  sge00  46982  eldmressn  47663  afvres  47798  afv2res  47865  prproropf1olem0  48140  31prm  48238  indprmfz  48271  rngccatidALTV  48926  rhmsubcALTVlem3  48937  funcringcsetcALTV2lem7  48950  ringccatidALTV  48960  ringcbasbasALTV  48966  funcringcsetclem7ALTV  48973  fldhmsubcALTV  48987  dfidom2  48997  ssnn0ssfz  49014  elbigo2  49217  itsclinecirc0in  49440  resinsnALT  49536  opndisj  49566  clddisj  49567  i0oii  49583  io1ii  49584