Theorem elin 3921

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

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143  Vcvv 3455   ∩ cin 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3912

This theorem is referenced by:  elini  4152  elind  4153  elinel1  4154  elinel2  4155  elin2  4156  elin3  4159  ineqri  4165  nfin  4177  inass  4180  ssin  4191  ssrin  4194  ralin  4202  rexin  4203  dfss4  4222  difin  4225  indi  4237  undi  4238  unineq  4241  indifdi  4247  difin2  4254  inrab2  4270  ndisj  4325  inn0f  4326  difin0ss  4328  inssdif0OLD  4330  inelcm  4425  inundif  4440  elinsn  4676  uniinOLD  4897  intun  4945  intprg  4946  elrint  4954  iunin2  5035  iinin2  5044  elriin  5047  disjor  5091  disjiun  5097  brin  5163  trin  5230  inex1  5286  inuni  5320  wefrc  5655  inopab  5816  inxp  5818  dmin  5901  dfres3  5983  intasym  6115  asymref  6116  dminss  6150  imainss  6151  inimasn  6153  cnvresima  6231  dfco2a  6247  ordtri3or  6393  2elresin  6656  respreima  7061  fvcofneq  7088  tpres  7199  isomin  7335  isoini  7336  offval  7683  ordpwsuc  7807  frpoins3xpg  8132  frpoins3xp3g  8133  xpord3pred  8144  ressuppss  8175  frrlem13  8291  fprlem1  8293  uniinqs  8791  mapval2  8866  ixpin  8917  boxriin  8934  disjen  9118  ssenen  9135  onfin2  9197  elfpw  9307  fiin  9378  inf3lem2  9594  epfrs  9696  cp  9873  dfac5lem1  10103  dfac5lem5  10107  dfac5  10108  kmlem3  10132  kmlem14  10143  kmlem15  10144  fin23lem26  10304  pwxpndom2  10645  ingru  10795  gruina  10798  grur1  10800  axgroth4  10812  grothprim  10814  ixxdisj  13382  icodisj  13498  fzdisj  13575  nn0disj  13668  fzouzdisj  13720  cotr2g  15009  limsupgle  15524  ello12  15563  elo12  15574  lo1resb  15611  rlimresb  15612  o1resb  15613  lo1eq  15615  rlimeq  15616  fsumsplit  15788  sumsplit  15815  fsum2dlem  15817  fprod2dlem  16030  bitsmod  16489  saddisjlem  16517  sadadd  16520  sadass  16524  smuval2  16535  smupval  16541  smueqlem  16543  smumul  16546  isprm7  16762  prmreclem5  16975  prmrec  16977  4sqlem12  17011  vdwmc  17033  setsstruct2  17229  acsfn  17710  iszeroo  18050  iszeroi  18061  fpwipodrs  18591  psss  18631  insubm  18872  subgacs  19222  nsgacs  19223  resscntz  19398  gsmsymgreq  19497  sylow2a  19684  lsmmod  19740  lsmdisj2  19747  gsumzsplit  19992  subgdmdprd  20101  dprdcntz2  20105  dprddisj2  20106  pgpfac1lem3  20144  rnghmval2  20522  isrhm  20557  subsubrng2  20663  subsubrg2  20698  rnghmsubcsetclem1  20730  funcrngcsetcALT  20740  zrinitorngc  20741  zrtermorngc  20742  rhmsubcsetclem1  20759  rhmsubcrngclem1  20765  ringcbasbas  20772  zrtermoringc  20774  srhmsubclem1  20776  fldhmsubc  20888  acsfn1p  20902  subrgacs  20903  sdrgacs  20904  isorng  20964  lssacs  21088  lspdisj  21249  lspdisjb  21250  prmidl0  21478  dfprm2  21623  irinitoringc  21629  ocvin  21824  unocv  21830  iunocv  21831  obselocv  21878  isassa  22006  aspid  22024  aspval2  22048  pmatcoe1fsupp  22858  isbasis2g  23105  tgval2  23113  tgcl  23126  ppttop  23164  epttop  23166  ssntr  23215  ntreq0  23234  isclo  23244  restntr  23339  restlp  23340  cnpresti  23445  cnprest  23446  cnprest2  23447  lmss  23455  haust1  23509  nrmsep3  23512  isnrm2  23515  lmmo  23537  fincmp  23550  cmpsublem  23556  cmpsub  23557  uncmp  23560  hauscmplem  23563  dfconn2  23576  iunconnlem  23584  unconn  23586  is1stc2  23599  1stcrest  23610  1stcelcls  23618  llyi  23631  nllyi  23632  subislly  23638  lly1stc  23653  txcnp  23777  txcnmpt  23781  hausdiag  23802  kqcldsat  23890  isfbas2  23992  isfil2  24013  fbasfip  24025  elfg  24028  filconn  24040  rnelfmlem  24109  rnelfm  24110  fmfnfmlem2  24112  fmfnfmlem4  24114  fmfnfm  24115  flimrest  24140  hauspwpwf1  24144  fclsrest  24181  alexsubALTlem2  24205  alexsubALTlem3  24206  alexsubALTlem4  24207  alexsubALT  24208  istmd  24231  istgp  24234  tsmssubm  24300  tsmssplit  24309  istrg  24321  istdrg  24323  istlm  24342  ustfilxp  24370  utoptop  24391  utop3cls  24408  bldisj  24555  blin  24578  blres  24588  lpbl  24660  metrest  24681  restmetu  24727  isngp  24753  isnlm  24832  isnmhm  24903  xrtgioo  24964  xrsmopn  24970  icccmplem2  24981  reconnlem2  24985  icoopnst  25098  iocopnst  25099  bndth  25117  zclmncvs  25307  isncvsngp  25308  ncvsprp  25311  ncvsm1  25313  ncvsdif  25314  ncvspi  25315  ncvs1  25316  ncvspds  25320  iscph  25329  tcphcph  25396  cfilfcls  25433  cmetcaulem  25447  isbn  25497  cldcss2  25601  hlhil  25602  ovolfcl  25625  ovolicc2lem2  25677  ovolicc2  25681  shftmbl  25697  volfiniun  25706  mbfmax  25808  mbfimaopnlem  25814  mbfaddlem  25819  i1faddlem  25852  i1fmullem  25853  i1fres  25864  itg1climres  25873  mbfi1fseqlem4  25877  itg2splitlem  25907  itg2split  25908  itgresr  25938  ellimc2  26036  ellimc3  26038  limcun  26054  dvreslem  26068  dvne0  26170  itgsubstlem  26207  ig1pval3  26335  aaliou2  26503  aaliou2b  26504  pilem1  26614  rlimcnp2  27131  fsumharmonic  27176  ppisval2  27269  prmorcht  27342  fsumvma2  27378  pclogsum  27379  vmasum  27380  chpchtsum  27383  chpub  27384  rpvmasum2  27676  madeval2  28026  tglineineq  28916  trlsegvdeg  30578  frgrncvvdeqlem7  30656  frgrncvvdeqlem9  30658  minvecolem1  31226  minvecolem4a  31229  minvecolem4b  31230  minvecolem4  31232  h2hcau  31331  axhcompl-zf  31350  hhcmpl  31552  hhcms  31555  ocin  31648  ocnel  31650  shmodsi  31741  pjhthlem2  31744  omlsilem  31754  pjoc1i  31783  spansnm0i  32002  nonbooli  32003  5oalem7  32012  3oalem3  32016  pjssmii  32033  mayete3i  32080  nmcopex  32381  nmcoplb  32382  lncnopbd  32389  nmcfnex  32405  nmcfnlb  32406  riesz4  32416  riesz1  32417  riesz2  32418  cnlnadjlem3  32421  cnlnadjlem5  32423  cnlnadjlem9  32427  cnlnadjeu  32430  rnbra  32459  pjimai  32528  pjclem4a  32550  pj3lem1  32558  jpi  32622  sumdmdii  32767  sumdmdlem  32770  sumdmdlem2  32771  cdjreui  32784  cdj3lem1  32786  iunin1f  32902  disjorf  32924  ofpreima  33010  1stpreima  33052  2ndpreima  33053  iocinioc2  33124  ssnnssfz  33132  cntzun  33399  kerunit  33645  ressply1mon1p  33858  ccfldextdgrr  34062  crefdf  34238  cmpcref  34240  cmppcmp  34248  cnre2csqima  34301  ordtconnlem1  34314  lmxrge0  34342  isrrext  34390  esum0  34439  esumcst  34453  esumpcvgval  34468  esumcvg  34476  measvuni  34604  eulerpartlemt0  34759  eulerpartlemr  34764  eulerpartlemgf  34769  eulerpartlemgs2  34770  eulerpartlemn  34771  fiblem  34788  oddprm2  35042  bnj1173  35390  bnj1174  35391  bnj1279  35406  elima4  36268  dfon2lem4  36276  ellimits  36400  dfom5b  36402  brapply  36428  brcap  36430  dfrecs2  36442  dfrdg4  36443  finminlem  36849  neibastop2lem  36891  neibastop2  36892  neifg  36902  tailfb  36908  onsucconni  36968  onintopssconn  36971  onsucsuccmpi  36974  limsucncmpi  36976  onint1  36980  mh-infprim2bi  37078  bj-inex1gALT  37580  bj-inrab  37583  bj-rcleqf  37681  bj-restuni  37759  bj-opelresdm  37809  bj-idres  37824  bj-opelidres  37825  bj-eldiag  37840  bj-eldiag2  37841  bj-ccinftydisj  37877  taupilem3  37983  isbasisrelowllem1  38021  isbasisrelowllem2  38022  nlpineqsn  38074  fvineqsneu  38077  ptrest  38290  poimirlem29  38320  poimirlem30  38321  mblfinlem2  38329  mbfposadd  38338  itg2gt0cn  38346  dvasin  38375  inixp  38399  0totbnd  38444  sstotbnd3  38447  heibor1lem  38480  heibor1  38481  heiborlem6  38487  isexid2  38526  smgrpismgmOLD  38533  issmgrpOLD  38534  mndoissmgrpOLD  38539  ismndo  38543  exidresid  38550  rngo1cl  38610  isfld2  38676  ineleq  39023  refressn  39202  eleccossin  39242  elrefsymrelsrel  39324  dfeldisj3  39480  eldisjdmqsim  39486  disjlem14  39570  prtlem14  39668  lshpdisj  39781  lkrin  39958  ishlat1  40146  pmodlem2  40641  pclfinN  40694  pclcmpatN  40695  osumcllem4N  40753  pexmidlem1N  40764  dihmeetlem1N  42084  dihglblem5apreN  42085  dihmeetlem4preN  42100  dihmeetlem13N  42113  dochnel2  42186  lcdlss  42413  mapd1o  42442  baerlem3lem2  42504  baerlem5alem2  42505  baerlem5blem2  42506  redvmptabs  43141  cmpfiiin  43448  mrefg2  43458  fz1eqin  43520  fnwe2lem2  43798  islmodfg  43816  islssfg2  43818  lnr2i  43863  rp-fakeinunass  44261  fiinfi  44319  elinintab  44321  elinintrab  44323  elinlem  44344  cnvcnvintabd  44346  ntrneikb  44840  ntrneik3  44842  ntrneik13  44844  ismnushort  45031  radcnvrat  45044  nzin  45048  onfrALTlem2  45275  onfrALTlem2VD  45617  relpmin  45681  pwclaxpow  45713  dfac5prim  45719  modelac8prim  45721  permac8prim  45743  iooabslt  46235  iccintsng  46259  lptioo2cn  46379  lptioo1cn  46380  cncfuni  46620  icccncfext  46621  stoweidlem44  46778  fourierdlem42  46883  fourierdlem80  46920  sge00  47110  eldmressn  47794  afvres  47929  afv2res  47996  prproropf1olem0  48271  31prm  48369  indprmfz  48402  rngccatidALTV  49057  rhmsubcALTVlem3  49068  funcringcsetcALTV2lem7  49081  ringccatidALTV  49091  ringcbasbasALTV  49097  funcringcsetclem7ALTV  49104  fldhmsubcALTV  49118  dfidom2  49128  ssnn0ssfz  49149  elbigo2  49352  itsclinecirc0in  49575  resinsnALT  49671  opndisj  49701  clddisj  49702  i0oii  49718  io1ii  49719