Theorem elin 3917

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  Vcvv 3440   ∩ cin 3900

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908

This theorem is referenced by:  elini  4151  elind  4152  elinel1  4153  elinel2  4154  elin2  4155  elin3  4158  ineqri  4164  nfin  4176  inass  4180  ssin  4191  ssrin  4194  ralin  4201  rexin  4202  dfss4  4221  difin  4224  indi  4236  undi  4237  unineq  4240  indifdi  4246  difin2  4253  inrab2  4269  ndisj  4322  inn0f  4323  difin0ss  4325  inssdif0  4326  inelcm  4417  inundif  4431  elinsn  4667  uniin  4887  intun  4935  intprg  4936  elrint  4944  iunin2  5026  iinin2  5033  elriin  5036  disjor  5080  disjiun  5086  brin  5150  trin  5216  inex1  5262  inuni  5295  wefrc  5618  inopab  5778  inxp  5780  inxpOLD  5781  dmin  5860  dfres3  5943  intasym  6072  asymref  6073  dminss  6111  imainss  6112  inimasn  6114  cnvresima  6188  dfco2a  6204  ordtri3or  6349  2elresin  6613  respreima  7011  fvcofneq  7038  tpres  7147  isomin  7283  isoini  7284  offval  7631  ordpwsuc  7757  frpoins3xpg  8082  frpoins3xp3g  8083  xpord3pred  8094  ressuppss  8125  frrlem13  8240  fprlem1  8242  uniinqs  8734  mapval2  8810  ixpin  8861  boxriin  8878  disjen  9062  ssenen  9079  onfin2  9141  elfpw  9254  fiin  9325  inf3lem2  9538  epfrs  9640  cp  9803  dfac5lem1  10033  dfac5lem5  10037  dfac5  10039  kmlem3  10063  kmlem14  10074  kmlem15  10075  fin23lem26  10235  pwxpndom2  10576  ingru  10726  gruina  10729  grur1  10731  axgroth4  10743  grothprim  10745  ixxdisj  13276  icodisj  13392  fzdisj  13467  nn0disj  13560  fzouzdisj  13611  cotr2g  14899  limsupgle  15400  ello12  15439  elo12  15450  lo1resb  15487  rlimresb  15488  o1resb  15489  lo1eq  15491  rlimeq  15492  fsumsplit  15664  sumsplit  15691  fsum2dlem  15693  fprod2dlem  15903  bitsmod  16363  saddisjlem  16391  sadadd  16394  sadass  16398  smuval2  16409  smupval  16415  smueqlem  16417  smumul  16420  isprm7  16635  prmreclem5  16848  prmrec  16850  4sqlem12  16884  vdwmc  16906  setsstruct2  17101  acsfn  17582  iszeroo  17922  iszeroi  17933  fpwipodrs  18463  psss  18503  insubm  18743  subgacs  19090  nsgacs  19091  resscntz  19262  gsmsymgreq  19361  sylow2a  19548  lsmmod  19604  lsmdisj2  19611  gsumzsplit  19856  subgdmdprd  19965  dprdcntz2  19969  dprddisj2  19970  pgpfac1lem3  20008  rnghmval2  20380  isrhm  20414  subsubrng2  20497  subsubrg2  20532  rnghmsubcsetclem1  20564  funcrngcsetcALT  20574  zrinitorngc  20575  zrtermorngc  20576  rhmsubcsetclem1  20593  rhmsubcrngclem1  20599  ringcbasbas  20606  zrtermoringc  20608  srhmsubclem1  20610  fldhmsubc  20718  acsfn1p  20732  subrgacs  20733  sdrgacs  20734  isorng  20794  lssacs  20918  lspdisj  21080  lspdisjb  21081  dfprm2  21428  irinitoringc  21434  ocvin  21629  unocv  21635  iunocv  21636  obselocv  21683  isassa  21811  aspid  21830  aspval2  21854  pmatcoe1fsupp  22645  isbasis2g  22892  tgval2  22900  tgcl  22913  ppttop  22951  epttop  22953  ssntr  23002  ntreq0  23021  isclo  23031  restntr  23126  restlp  23127  cnpresti  23232  cnprest  23233  cnprest2  23234  lmss  23242  haust1  23296  nrmsep3  23299  isnrm2  23302  lmmo  23324  fincmp  23337  cmpsublem  23343  cmpsub  23344  uncmp  23347  hauscmplem  23350  dfconn2  23363  iunconnlem  23371  unconn  23373  is1stc2  23386  1stcrest  23397  1stcelcls  23405  llyi  23418  nllyi  23419  subislly  23425  lly1stc  23440  txcnp  23564  txcnmpt  23568  hausdiag  23589  kqcldsat  23677  isfbas2  23779  isfil2  23800  fbasfip  23812  elfg  23815  filconn  23827  rnelfmlem  23896  rnelfm  23897  fmfnfmlem2  23899  fmfnfmlem4  23901  fmfnfm  23902  flimrest  23927  hauspwpwf1  23931  fclsrest  23968  alexsubALTlem2  23992  alexsubALTlem3  23993  alexsubALTlem4  23994  alexsubALT  23995  istmd  24018  istgp  24021  tsmssubm  24087  tsmssplit  24096  istrg  24108  istdrg  24110  istlm  24129  ustfilxp  24157  utoptop  24178  utop3cls  24195  bldisj  24342  blin  24365  blres  24375  lpbl  24447  metrest  24468  restmetu  24514  isngp  24540  isnlm  24619  isnmhm  24690  xrtgioo  24751  xrsmopn  24757  icccmplem2  24768  reconnlem2  24772  icoopnst  24892  iocopnst  24893  bndth  24913  zclmncvs  25104  isncvsngp  25105  ncvsprp  25108  ncvsm1  25110  ncvsdif  25111  ncvspi  25112  ncvs1  25113  ncvspds  25117  iscph  25126  tcphcph  25193  cfilfcls  25230  cmetcaulem  25244  isbn  25294  cldcss2  25398  hlhil  25399  ovolfcl  25423  ovolicc2lem2  25475  ovolicc2  25479  shftmbl  25495  volfiniun  25504  mbfmax  25606  mbfimaopnlem  25612  mbfaddlem  25617  i1faddlem  25650  i1fmullem  25651  i1fres  25662  itg1climres  25671  mbfi1fseqlem4  25675  itg2splitlem  25705  itg2split  25706  itgresr  25736  ellimc2  25834  ellimc3  25836  limcun  25852  dvreslem  25866  dvne0  25972  itgsubstlem  26011  ig1pval3  26139  aaliou2  26304  aaliou2b  26305  pilem1  26417  rlimcnp2  26932  fsumharmonic  26978  ppisval2  27071  prmorcht  27144  fsumvma2  27181  pclogsum  27182  vmasum  27183  chpchtsum  27186  chpub  27187  rpvmasum2  27479  madeval2  27829  tglineineq  28715  trlsegvdeg  30302  frgrncvvdeqlem7  30380  frgrncvvdeqlem9  30382  minvecolem1  30949  minvecolem4a  30952  minvecolem4b  30953  minvecolem4  30955  h2hcau  31054  axhcompl-zf  31073  hhcmpl  31275  hhcms  31278  ocin  31371  ocnel  31373  shmodsi  31464  pjhthlem2  31467  omlsilem  31477  pjoc1i  31506  spansnm0i  31725  nonbooli  31726  5oalem7  31735  3oalem3  31739  pjssmii  31756  mayete3i  31803  nmcopex  32104  nmcoplb  32105  lncnopbd  32112  nmcfnex  32128  nmcfnlb  32129  riesz4  32139  riesz1  32140  riesz2  32141  cnlnadjlem3  32144  cnlnadjlem5  32146  cnlnadjlem9  32150  cnlnadjeu  32153  rnbra  32182  pjimai  32251  pjclem4a  32273  pj3lem1  32281  jpi  32345  sumdmdii  32490  sumdmdlem  32493  sumdmdlem2  32494  cdjreui  32507  cdj3lem1  32509  iunin1f  32632  disjorf  32654  ofpreima  32743  1stpreima  32786  2ndpreima  32787  iocinioc2  32859  ssnnssfz  32867  cntzun  33161  kerunit  33406  prmidl0  33531  ressply1mon1p  33649  ccfldextdgrr  33829  crefdf  34005  cmpcref  34007  cmppcmp  34015  cnre2csqima  34068  ordtconnlem1  34081  lmxrge0  34109  isrrext  34157  esum0  34206  esumcst  34220  esumpcvgval  34235  esumcvg  34243  measvuni  34371  eulerpartlemt0  34526  eulerpartlemr  34531  eulerpartlemgf  34536  eulerpartlemgs2  34537  eulerpartlemn  34538  fiblem  34555  oddprm2  34812  bnj1173  35158  bnj1174  35159  bnj1279  35174  elima4  35970  dfon2lem4  35978  ellimits  36102  dfom5b  36104  brapply  36130  brcap  36132  dfrecs2  36144  dfrdg4  36145  finminlem  36512  neibastop2lem  36554  neibastop2  36555  neifg  36565  tailfb  36571  onsucconni  36631  onintopssconn  36634  onsucsuccmpi  36637  limsucncmpi  36639  onint1  36643  bj-inrab  37128  bj-rcleqf  37226  bj-restuni  37302  bj-opelresdm  37350  bj-idres  37365  bj-opelidres  37366  bj-eldiag  37381  bj-eldiag2  37382  bj-ccinftydisj  37418  taupilem3  37524  isbasisrelowllem1  37560  isbasisrelowllem2  37561  nlpineqsn  37613  fvineqsneu  37616  ptrest  37820  poimirlem29  37850  poimirlem30  37851  mblfinlem2  37859  mbfposadd  37868  itg2gt0cn  37876  dvasin  37905  inixp  37929  0totbnd  37974  sstotbnd3  37977  heibor1lem  38010  heibor1  38011  heiborlem6  38017  isexid2  38056  smgrpismgmOLD  38063  issmgrpOLD  38064  mndoissmgrpOLD  38069  ismndo  38073  exidresid  38080  rngo1cl  38140  isfld2  38206  ineleq  38549  refressn  38716  eleccossin  38756  elrefsymrelsrel  38838  dfeldisj3  38988  disjlem14  39067  prtlem14  39144  lshpdisj  39257  lkrin  39434  ishlat1  39622  pmodlem2  40117  pclfinN  40170  pclcmpatN  40171  osumcllem4N  40229  pexmidlem1N  40240  dihmeetlem1N  41560  dihglblem5apreN  41561  dihmeetlem4preN  41576  dihmeetlem13N  41589  dochnel2  41662  lcdlss  41889  mapd1o  41918  baerlem3lem2  41980  baerlem5alem2  41981  baerlem5blem2  41982  redvmptabs  42625  cmpfiiin  42949  mrefg2  42959  fz1eqin  43021  fnwe2lem2  43303  islmodfg  43321  islssfg2  43323  lnr2i  43368  rp-fakeinunass  43766  fiinfi  43824  elinintab  43826  elinintrab  43828  elinlem  43849  cnvcnvintabd  43851  ntrneikb  44345  ntrneik3  44347  ntrneik13  44349  ismnushort  44552  radcnvrat  44565  nzin  44569  onfrALTlem2  44797  onfrALTlem2VD  45139  relpmin  45203  pwclaxpow  45235  dfac5prim  45241  modelac8prim  45243  permac8prim  45265  iooabslt  45755  iccintsng  45779  lptioo2cn  45899  lptioo1cn  45900  cncfuni  46140  icccncfext  46141  stoweidlem44  46298  fourierdlem42  46403  fourierdlem80  46440  sge00  46630  eldmressn  47293  afvres  47428  afv2res  47495  prproropf1olem0  47758  31prm  47853  rngccatidALTV  48528  rhmsubcALTVlem3  48539  funcringcsetcALTV2lem7  48552  ringccatidALTV  48562  ringcbasbasALTV  48568  funcringcsetclem7ALTV  48575  fldhmsubcALTV  48589  ssnn0ssfz  48605  elbigo2  48808  itsclinecirc0in  49031  resinsnALT  49128  opndisj  49158  clddisj  49159  i0oii  49175  io1ii  49176