Theorem elin 3963

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

Syntax hints:   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  Vcvv 3475   ∩ cin 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3954

This theorem is referenced by:  dfss2  3967  elini  4192  elind  4193  elinel1  4194  elinel2  4195  elin2  4196  elin3  4199  ineqri  4203  inass  4218  ssin  4229  ssrin  4232  rexin  4238  dfss4  4257  difin  4260  indi  4272  undi  4273  unineq  4276  indifdi  4282  indifdirOLD  4284  difin2  4290  inrab2  4306  ndisj  4366  difin0ss  4367  inssdif0  4368  inelcm  4463  inundif  4477  elinsn  4713  uniin  4934  intun  4983  intprg  4984  intprOLD  4986  elrint  4994  iunin2  5073  iinin2  5080  elriin  5083  disjor  5127  disjiun  5134  brin  5199  trin  5276  inex1  5316  inuni  5342  wefrc  5669  inopab  5827  inxp  5830  dmin  5909  dfres3  5984  intasym  6113  asymref  6114  dminss  6149  imainss  6150  inimasn  6152  cnvresima  6226  dfco2a  6242  ordtri3or  6393  2elresin  6668  respreima  7063  fvcofneq  7090  tpres  7197  isomin  7329  isoini  7330  offval  7674  ordpwsuc  7798  frpoins3xpg  8121  frpoins3xp3g  8122  xpord3pred  8133  ressuppss  8163  frrlem13  8278  fprlem1  8280  wfrlem5OLD  8308  uniinqs  8787  mapval2  8862  ixpin  8913  boxriin  8930  disjen  9130  ssenen  9147  onfin2  9227  elfpw  9350  fiin  9413  inf3lem2  9620  epfrs  9722  cp  9882  dfac5lem1  10114  dfac5lem5  10118  dfac5  10119  kmlem3  10143  kmlem14  10154  kmlem15  10155  fin23lem26  10316  pwxpndom2  10656  ingru  10806  gruina  10809  grur1  10811  axgroth4  10823  grothprim  10825  ixxdisj  13335  icodisj  13449  fzdisj  13524  nn0disj  13613  fzouzdisj  13664  cotr2g  14919  limsupgle  15417  ello12  15456  elo12  15467  lo1resb  15504  rlimresb  15505  o1resb  15506  lo1eq  15508  rlimeq  15509  fsumsplit  15683  sumsplit  15710  fsum2dlem  15712  fprod2dlem  15920  bitsmod  16373  saddisjlem  16401  sadadd  16404  sadass  16408  smuval2  16419  smupval  16425  smueqlem  16427  smumul  16430  isprm7  16641  prmreclem5  16849  prmrec  16851  4sqlem12  16885  vdwmc  16907  setsstruct2  17103  acsfn  17599  iszeroo  17944  iszeroi  17955  fpwipodrs  18489  psss  18529  insubm  18695  subgacs  19035  nsgacs  19036  resscntz  19190  gsmsymgreq  19293  sylow2a  19480  lsmmod  19536  lsmdisj2  19543  gsumzsplit  19787  subgdmdprd  19896  dprdcntz2  19900  dprddisj2  19901  pgpfac1lem3  19939  isrhm  20246  subsubrg2  20379  acsfn1p  20403  subrgacs  20404  sdrgacs  20405  lssacs  20566  lspdisj  20726  lspdisjb  20727  dfprm2  21027  ocvin  21211  unocv  21217  iunocv  21218  obselocv  21267  isassa  21395  aspid  21411  aspval2  21434  pmatcoe1fsupp  22185  isbasis2g  22433  tgval2  22441  tgcl  22454  ppttop  22492  epttop  22494  ssntr  22544  ntreq0  22563  isclo  22573  restntr  22668  restlp  22669  cnpresti  22774  cnprest  22775  cnprest2  22776  lmss  22784  haust1  22838  nrmsep3  22841  isnrm2  22844  lmmo  22866  fincmp  22879  cmpsublem  22885  cmpsub  22886  uncmp  22889  hauscmplem  22892  dfconn2  22905  iunconnlem  22913  unconn  22915  is1stc2  22928  1stcrest  22939  1stcelcls  22947  llyi  22960  nllyi  22961  subislly  22967  lly1stc  22982  txcnp  23106  txcnmpt  23110  hausdiag  23131  kqcldsat  23219  isfbas2  23321  isfil2  23342  fbasfip  23354  elfg  23357  filconn  23369  rnelfmlem  23438  rnelfm  23439  fmfnfmlem2  23441  fmfnfmlem4  23443  fmfnfm  23444  flimrest  23469  hauspwpwf1  23473  fclsrest  23510  alexsubALTlem2  23534  alexsubALTlem3  23535  alexsubALTlem4  23536  alexsubALT  23537  istmd  23560  istgp  23563  tsmssubm  23629  tsmssplit  23638  istrg  23650  istdrg  23652  istlm  23671  ustfilxp  23699  utoptop  23721  utop3cls  23738  bldisj  23886  blin  23909  blres  23919  lpbl  23994  metrest  24015  restmetu  24061  isngp  24087  isnlm  24174  isnmhm  24245  xrtgioo  24304  xrsmopn  24310  icccmplem2  24321  reconnlem2  24325  icoopnst  24437  iocopnst  24438  bndth  24456  zclmncvs  24647  isncvsngp  24648  ncvsprp  24651  ncvsm1  24653  ncvsdif  24654  ncvspi  24655  ncvs1  24656  ncvspds  24660  iscph  24669  tcphcph  24736  cfilfcls  24773  cmetcaulem  24787  isbn  24837  cldcss2  24941  hlhil  24942  ovolfcl  24965  ovolicc2lem2  25017  ovolicc2  25021  shftmbl  25037  volfiniun  25046  mbfmax  25148  mbfimaopnlem  25154  mbfaddlem  25159  i1faddlem  25192  i1fmullem  25193  i1fres  25205  itg1climres  25214  mbfi1fseqlem4  25218  itg2splitlem  25248  itg2split  25249  itgresr  25278  ellimc2  25376  ellimc3  25378  limcun  25394  dvreslem  25408  dvne0  25510  itgsubstlem  25547  ig1pval3  25674  aaliou2  25835  aaliou2b  25836  pilem1  25945  rlimcnp2  26451  fsumharmonic  26496  ppisval2  26589  prmorcht  26662  fsumvma2  26697  pclogsum  26698  vmasum  26699  chpchtsum  26702  chpub  26703  rpvmasum2  26995  madeval2  27328  tglineineq  27874  trlsegvdeg  29460  frgrncvvdeqlem7  29538  frgrncvvdeqlem9  29540  minvecolem1  30105  minvecolem4a  30108  minvecolem4b  30109  minvecolem4  30111  h2hcau  30210  axhcompl-zf  30229  hhcmpl  30431  hhcms  30434  ocin  30527  ocnel  30529  shmodsi  30620  pjhthlem2  30623  omlsilem  30633  pjoc1i  30662  spansnm0i  30881  nonbooli  30882  5oalem7  30891  3oalem3  30895  pjssmii  30912  mayete3i  30959  nmcopex  31260  nmcoplb  31261  lncnopbd  31268  nmcfnex  31284  nmcfnlb  31285  riesz4  31295  riesz1  31296  riesz2  31297  cnlnadjlem3  31300  cnlnadjlem5  31302  cnlnadjlem9  31306  cnlnadjeu  31309  rnbra  31338  pjimai  31407  pjclem4a  31429  pj3lem1  31437  jpi  31501  sumdmdii  31646  sumdmdlem  31649  sumdmdlem2  31650  cdjreui  31663  cdj3lem1  31665  iunin1f  31767  disjorf  31788  ofpreima  31868  1stpreima  31906  2ndpreima  31907  iocinioc2  31968  ssnnssfz  31976  cntzun  32190  isorng  32386  kerunit  32406  prmidl0  32527  ressply1mon1p  32604  ccfldextdgrr  32691  crefdf  32766  cmpcref  32768  cmppcmp  32776  cnre2csqima  32829  ordtconnlem1  32842  lmxrge0  32870  isrrext  32918  esum0  32985  esumcst  32999  esumpcvgval  33014  esumcvg  33022  measvuni  33150  eulerpartlemt0  33306  eulerpartlemr  33311  eulerpartlemgf  33316  eulerpartlemgs2  33317  eulerpartlemn  33318  fiblem  33335  oddprm2  33605  bnj1173  33951  bnj1174  33952  bnj1279  33967  elima4  34685  dfon2lem4  34696  ellimits  34820  dfom5b  34822  brapply  34848  brcap  34850  dfrecs2  34860  dfrdg4  34861  finminlem  35141  neibastop2lem  35183  neibastop2  35184  neifg  35194  tailfb  35200  onsucconni  35260  onintopssconn  35263  onsucsuccmpi  35266  limsucncmpi  35268  onint1  35272  bj-inrab  35745  bj-rcleqf  35844  bj-restuni  35916  bj-opelresdm  35964  bj-idres  35979  bj-opelidres  35980  bj-eldiag  35995  bj-eldiag2  35996  bj-ccinftydisj  36032  taupilem3  36138  isbasisrelowllem1  36174  isbasisrelowllem2  36175  nlpineqsn  36227  fvineqsneu  36230  ptrest  36425  poimirlem29  36455  poimirlem30  36456  mblfinlem2  36464  mbfposadd  36473  itg2gt0cn  36481  dvasin  36510  inixp  36534  0totbnd  36579  sstotbnd3  36582  heibor1lem  36615  heibor1  36616  heiborlem6  36622  isexid2  36661  smgrpismgmOLD  36668  issmgrpOLD  36669  mndoissmgrpOLD  36674  ismndo  36678  exidresid  36685  rngo1cl  36745  isfld2  36811  ralin  37053  ineleq  37161  refressn  37251  eleccossin  37291  elrefsymrelsrel  37379  dfeldisj3  37527  disjlem14  37606  prtlem14  37682  lshpdisj  37795  lkrin  37972  ishlat1  38160  pmodlem2  38656  pclfinN  38709  pclcmpatN  38710  osumcllem4N  38768  pexmidlem1N  38779  dihmeetlem1N  40099  dihglblem5apreN  40100  dihmeetlem4preN  40115  dihmeetlem13N  40128  dochnel2  40201  lcdlss  40428  mapd1o  40457  baerlem3lem2  40519  baerlem5alem2  40520  baerlem5blem2  40521  cmpfiiin  41368  mrefg2  41378  fz1eqin  41440  fnwe2lem2  41726  islmodfg  41744  islssfg2  41746  lnr2i  41791  rp-fakeinunass  42199  fiinfi  42257  elinintab  42259  elinintrab  42261  elinlem  42282  cnvcnvintabd  42284  ntrneikb  42778  ntrneik3  42780  ntrneik13  42782  ismnushort  42993  radcnvrat  43006  nzin  43010  onfrALTlem2  43240  onfrALTlem2VD  43583  inn0f  43693  iooabslt  44147  iccintsng  44171  lptioo2cn  44296  lptioo1cn  44297  cncfuni  44537  icccncfext  44538  stoweidlem44  44695  fourierdlem42  44800  fourierdlem80  44837  sge00  45027  eldmressn  45682  afvres  45815  afv2res  45882  prproropf1olem0  46105  31prm  46200  rnghmval2  46627  subsubrng2  46676  rnghmsubcsetclem1  46775  rngccatidALTV  46789  funcrngcsetcALT  46799  zrinitorngc  46800  zrtermorngc  46801  rhmsubcsetclem1  46821  rhmsubcrngclem1  46827  ringcbasbas  46834  funcringcsetcALTV2lem7  46842  ringccatidALTV  46852  ringcbasbasALTV  46858  funcringcsetclem7ALTV  46865  irinitoringc  46869  zrtermoringc  46870  srhmsubclem1  46873  fldhmsubc  46884  fldhmsubcALTV  46902  rhmsubcALTVlem3  46906  ssnn0ssfz  46927  elbigo2  47140  itsclinecirc0in  47363  opndisj  47437  clddisj  47438  i0oii  47454  io1ii  47455