Theorem elin 3942

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108  Vcvv 3459   ∩ cin 3925

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-in 3933

This theorem is referenced by:  elini  4174  elind  4175  elinel1  4176  elinel2  4177  elin2  4178  elin3  4181  ineqri  4187  nfin  4199  inass  4203  ssin  4214  ssrin  4217  ralin  4224  rexin  4225  dfss4  4244  difin  4247  indi  4259  undi  4260  unineq  4263  indifdi  4269  difin2  4276  inrab2  4292  ndisj  4345  inn0f  4346  difin0ss  4348  inssdif0  4349  inelcm  4440  inundif  4454  elinsn  4686  uniin  4907  intun  4956  intprg  4957  elrint  4965  iunin2  5047  iinin2  5054  elriin  5057  disjor  5101  disjiun  5107  brin  5171  trin  5241  inex1  5287  inuni  5320  wefrc  5648  inopab  5808  inxp  5811  inxpOLD  5812  dmin  5891  dfres3  5971  intasym  6104  asymref  6105  dminss  6142  imainss  6143  inimasn  6145  cnvresima  6219  dfco2a  6235  ordtri3or  6384  2elresin  6658  respreima  7055  fvcofneq  7082  tpres  7192  isomin  7329  isoini  7330  offval  7678  ordpwsuc  7807  frpoins3xpg  8137  frpoins3xp3g  8138  xpord3pred  8149  ressuppss  8180  frrlem13  8295  fprlem1  8297  wfrlem5OLD  8325  uniinqs  8809  mapval2  8884  ixpin  8935  boxriin  8952  disjen  9146  ssenen  9163  onfin2  9238  elfpw  9364  fiin  9432  inf3lem2  9641  epfrs  9743  cp  9903  dfac5lem1  10135  dfac5lem5  10139  dfac5  10141  kmlem3  10165  kmlem14  10176  kmlem15  10177  fin23lem26  10337  pwxpndom2  10677  ingru  10827  gruina  10830  grur1  10832  axgroth4  10844  grothprim  10846  ixxdisj  13375  icodisj  13491  fzdisj  13566  nn0disj  13659  fzouzdisj  13710  cotr2g  14993  limsupgle  15491  ello12  15530  elo12  15541  lo1resb  15578  rlimresb  15579  o1resb  15580  lo1eq  15582  rlimeq  15583  fsumsplit  15755  sumsplit  15782  fsum2dlem  15784  fprod2dlem  15994  bitsmod  16453  saddisjlem  16481  sadadd  16484  sadass  16488  smuval2  16499  smupval  16505  smueqlem  16507  smumul  16510  isprm7  16725  prmreclem5  16938  prmrec  16940  4sqlem12  16974  vdwmc  16996  setsstruct2  17191  acsfn  17669  iszeroo  18009  iszeroi  18020  fpwipodrs  18548  psss  18588  insubm  18794  subgacs  19142  nsgacs  19143  resscntz  19314  gsmsymgreq  19411  sylow2a  19598  lsmmod  19654  lsmdisj2  19661  gsumzsplit  19906  subgdmdprd  20015  dprdcntz2  20019  dprddisj2  20020  pgpfac1lem3  20058  rnghmval2  20402  isrhm  20436  subsubrng2  20522  subsubrg2  20557  rnghmsubcsetclem1  20589  funcrngcsetcALT  20599  zrinitorngc  20600  zrtermorngc  20601  rhmsubcsetclem1  20618  rhmsubcrngclem1  20624  ringcbasbas  20631  zrtermoringc  20633  srhmsubclem1  20635  fldhmsubc  20743  acsfn1p  20757  subrgacs  20758  sdrgacs  20759  lssacs  20922  lspdisj  21084  lspdisjb  21085  dfprm2  21432  irinitoringc  21438  ocvin  21632  unocv  21638  iunocv  21639  obselocv  21686  isassa  21814  aspid  21833  aspval2  21856  pmatcoe1fsupp  22637  isbasis2g  22884  tgval2  22892  tgcl  22905  ppttop  22943  epttop  22945  ssntr  22994  ntreq0  23013  isclo  23023  restntr  23118  restlp  23119  cnpresti  23224  cnprest  23225  cnprest2  23226  lmss  23234  haust1  23288  nrmsep3  23291  isnrm2  23294  lmmo  23316  fincmp  23329  cmpsublem  23335  cmpsub  23336  uncmp  23339  hauscmplem  23342  dfconn2  23355  iunconnlem  23363  unconn  23365  is1stc2  23378  1stcrest  23389  1stcelcls  23397  llyi  23410  nllyi  23411  subislly  23417  lly1stc  23432  txcnp  23556  txcnmpt  23560  hausdiag  23581  kqcldsat  23669  isfbas2  23771  isfil2  23792  fbasfip  23804  elfg  23807  filconn  23819  rnelfmlem  23888  rnelfm  23889  fmfnfmlem2  23891  fmfnfmlem4  23893  fmfnfm  23894  flimrest  23919  hauspwpwf1  23923  fclsrest  23960  alexsubALTlem2  23984  alexsubALTlem3  23985  alexsubALTlem4  23986  alexsubALT  23987  istmd  24010  istgp  24013  tsmssubm  24079  tsmssplit  24088  istrg  24100  istdrg  24102  istlm  24121  ustfilxp  24149  utoptop  24171  utop3cls  24188  bldisj  24335  blin  24358  blres  24368  lpbl  24440  metrest  24461  restmetu  24507  isngp  24533  isnlm  24612  isnmhm  24683  xrtgioo  24744  xrsmopn  24750  icccmplem2  24761  reconnlem2  24765  icoopnst  24885  iocopnst  24886  bndth  24906  zclmncvs  25098  isncvsngp  25099  ncvsprp  25102  ncvsm1  25104  ncvsdif  25105  ncvspi  25106  ncvs1  25107  ncvspds  25111  iscph  25120  tcphcph  25187  cfilfcls  25224  cmetcaulem  25238  isbn  25288  cldcss2  25392  hlhil  25393  ovolfcl  25417  ovolicc2lem2  25469  ovolicc2  25473  shftmbl  25489  volfiniun  25498  mbfmax  25600  mbfimaopnlem  25606  mbfaddlem  25611  i1faddlem  25644  i1fmullem  25645  i1fres  25656  itg1climres  25665  mbfi1fseqlem4  25669  itg2splitlem  25699  itg2split  25700  itgresr  25730  ellimc2  25828  ellimc3  25830  limcun  25846  dvreslem  25860  dvne0  25966  itgsubstlem  26005  ig1pval3  26133  aaliou2  26298  aaliou2b  26299  pilem1  26411  rlimcnp2  26926  fsumharmonic  26972  ppisval2  27065  prmorcht  27138  fsumvma2  27175  pclogsum  27176  vmasum  27177  chpchtsum  27180  chpub  27181  rpvmasum2  27473  madeval2  27809  tglineineq  28568  trlsegvdeg  30154  frgrncvvdeqlem7  30232  frgrncvvdeqlem9  30234  minvecolem1  30801  minvecolem4a  30804  minvecolem4b  30805  minvecolem4  30807  h2hcau  30906  axhcompl-zf  30925  hhcmpl  31127  hhcms  31130  ocin  31223  ocnel  31225  shmodsi  31316  pjhthlem2  31319  omlsilem  31329  pjoc1i  31358  spansnm0i  31577  nonbooli  31578  5oalem7  31587  3oalem3  31591  pjssmii  31608  mayete3i  31655  nmcopex  31956  nmcoplb  31957  lncnopbd  31964  nmcfnex  31980  nmcfnlb  31981  riesz4  31991  riesz1  31992  riesz2  31993  cnlnadjlem3  31996  cnlnadjlem5  31998  cnlnadjlem9  32002  cnlnadjeu  32005  rnbra  32034  pjimai  32103  pjclem4a  32125  pj3lem1  32133  jpi  32197  sumdmdii  32342  sumdmdlem  32345  sumdmdlem2  32346  cdjreui  32359  cdj3lem1  32361  iunin1f  32484  disjorf  32506  ofpreima  32589  1stpreima  32630  2ndpreima  32631  iocinioc2  32702  ssnnssfz  32710  cntzun  33008  isorng  33267  kerunit  33287  prmidl0  33411  ressply1mon1p  33527  ccfldextdgrr  33659  crefdf  33825  cmpcref  33827  cmppcmp  33835  cnre2csqima  33888  ordtconnlem1  33901  lmxrge0  33929  isrrext  33977  esum0  34026  esumcst  34040  esumpcvgval  34055  esumcvg  34063  measvuni  34191  eulerpartlemt0  34347  eulerpartlemr  34352  eulerpartlemgf  34357  eulerpartlemgs2  34358  eulerpartlemn  34359  fiblem  34376  oddprm2  34633  bnj1173  34979  bnj1174  34980  bnj1279  34995  elima4  35739  dfon2lem4  35750  ellimits  35874  dfom5b  35876  brapply  35902  brcap  35904  dfrecs2  35914  dfrdg4  35915  finminlem  36282  neibastop2lem  36324  neibastop2  36325  neifg  36335  tailfb  36341  onsucconni  36401  onintopssconn  36404  onsucsuccmpi  36407  limsucncmpi  36409  onint1  36413  bj-inrab  36891  bj-rcleqf  36989  bj-restuni  37061  bj-opelresdm  37109  bj-idres  37124  bj-opelidres  37125  bj-eldiag  37140  bj-eldiag2  37141  bj-ccinftydisj  37177  taupilem3  37283  isbasisrelowllem1  37319  isbasisrelowllem2  37320  nlpineqsn  37372  fvineqsneu  37375  ptrest  37589  poimirlem29  37619  poimirlem30  37620  mblfinlem2  37628  mbfposadd  37637  itg2gt0cn  37645  dvasin  37674  inixp  37698  0totbnd  37743  sstotbnd3  37746  heibor1lem  37779  heibor1  37780  heiborlem6  37786  isexid2  37825  smgrpismgmOLD  37832  issmgrpOLD  37833  mndoissmgrpOLD  37838  ismndo  37842  exidresid  37849  rngo1cl  37909  isfld2  37975  ineleq  38318  refressn  38407  eleccossin  38447  elrefsymrelsrel  38535  dfeldisj3  38683  disjlem14  38762  prtlem14  38838  lshpdisj  38951  lkrin  39128  ishlat1  39316  pmodlem2  39812  pclfinN  39865  pclcmpatN  39866  osumcllem4N  39924  pexmidlem1N  39935  dihmeetlem1N  41255  dihglblem5apreN  41256  dihmeetlem4preN  41271  dihmeetlem13N  41284  dochnel2  41357  lcdlss  41584  mapd1o  41613  baerlem3lem2  41675  baerlem5alem2  41676  baerlem5blem2  41677  redvmptabs  42350  cmpfiiin  42667  mrefg2  42677  fz1eqin  42739  fnwe2lem2  43022  islmodfg  43040  islssfg2  43042  lnr2i  43087  rp-fakeinunass  43486  fiinfi  43544  elinintab  43546  elinintrab  43548  elinlem  43569  cnvcnvintabd  43571  ntrneikb  44065  ntrneik3  44067  ntrneik13  44069  ismnushort  44273  radcnvrat  44286  nzin  44290  onfrALTlem2  44519  onfrALTlem2VD  44861  relpmin  44925  pwclaxpow  44957  dfac5prim  44963  modelac8prim  44965  iooabslt  45476  iccintsng  45500  lptioo2cn  45622  lptioo1cn  45623  cncfuni  45863  icccncfext  45864  stoweidlem44  46021  fourierdlem42  46126  fourierdlem80  46163  sge00  46353  eldmressn  47014  afvres  47149  afv2res  47216  prproropf1olem0  47464  31prm  47559  rngccatidALTV  48195  rhmsubcALTVlem3  48206  funcringcsetcALTV2lem7  48219  ringccatidALTV  48229  ringcbasbasALTV  48235  funcringcsetclem7ALTV  48242  fldhmsubcALTV  48256  ssnn0ssfz  48272  elbigo2  48480  itsclinecirc0in  48703  resinsnALT  48796  opndisj  48825  clddisj  48826  i0oii  48842  io1ii  48843