Theorem elin 3919

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3436   ∩ cin 3902

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-in 3910

This theorem is referenced by:  elini  4150  elind  4151  elinel1  4152  elinel2  4153  elin2  4154  elin3  4157  ineqri  4163  nfin  4175  inass  4179  ssin  4190  ssrin  4193  ralin  4200  rexin  4201  dfss4  4220  difin  4223  indi  4235  undi  4236  unineq  4239  indifdi  4245  difin2  4252  inrab2  4268  ndisj  4321  inn0f  4322  difin0ss  4324  inssdif0  4325  inelcm  4416  inundif  4430  elinsn  4662  uniin  4882  intun  4930  intprg  4931  elrint  4939  iunin2  5020  iinin2  5027  elriin  5030  disjor  5074  disjiun  5080  brin  5144  trin  5210  inex1  5256  inuni  5289  wefrc  5613  inopab  5772  inxp  5774  inxpOLD  5775  dmin  5854  dfres3  5935  intasym  6064  asymref  6065  dminss  6102  imainss  6103  inimasn  6105  cnvresima  6179  dfco2a  6195  ordtri3or  6339  2elresin  6603  respreima  7000  fvcofneq  7027  tpres  7137  isomin  7274  isoini  7275  offval  7622  ordpwsuc  7748  frpoins3xpg  8073  frpoins3xp3g  8074  xpord3pred  8085  ressuppss  8116  frrlem13  8231  fprlem1  8233  uniinqs  8724  mapval2  8799  ixpin  8850  boxriin  8867  disjen  9051  ssenen  9068  onfin2  9130  elfpw  9244  fiin  9312  inf3lem2  9525  epfrs  9627  cp  9787  dfac5lem1  10017  dfac5lem5  10021  dfac5  10023  kmlem3  10047  kmlem14  10058  kmlem15  10059  fin23lem26  10219  pwxpndom2  10559  ingru  10709  gruina  10712  grur1  10714  axgroth4  10726  grothprim  10728  ixxdisj  13263  icodisj  13379  fzdisj  13454  nn0disj  13547  fzouzdisj  13598  cotr2g  14883  limsupgle  15384  ello12  15423  elo12  15434  lo1resb  15471  rlimresb  15472  o1resb  15473  lo1eq  15475  rlimeq  15476  fsumsplit  15648  sumsplit  15675  fsum2dlem  15677  fprod2dlem  15887  bitsmod  16347  saddisjlem  16375  sadadd  16378  sadass  16382  smuval2  16393  smupval  16399  smueqlem  16401  smumul  16404  isprm7  16619  prmreclem5  16832  prmrec  16834  4sqlem12  16868  vdwmc  16890  setsstruct2  17085  acsfn  17565  iszeroo  17905  iszeroi  17916  fpwipodrs  18446  psss  18486  insubm  18692  subgacs  19040  nsgacs  19041  resscntz  19212  gsmsymgreq  19311  sylow2a  19498  lsmmod  19554  lsmdisj2  19561  gsumzsplit  19806  subgdmdprd  19915  dprdcntz2  19919  dprddisj2  19920  pgpfac1lem3  19958  rnghmval2  20329  isrhm  20363  subsubrng2  20449  subsubrg2  20484  rnghmsubcsetclem1  20516  funcrngcsetcALT  20526  zrinitorngc  20527  zrtermorngc  20528  rhmsubcsetclem1  20545  rhmsubcrngclem1  20551  ringcbasbas  20558  zrtermoringc  20560  srhmsubclem1  20562  fldhmsubc  20670  acsfn1p  20684  subrgacs  20685  sdrgacs  20686  isorng  20746  lssacs  20870  lspdisj  21032  lspdisjb  21033  dfprm2  21380  irinitoringc  21386  ocvin  21581  unocv  21587  iunocv  21588  obselocv  21635  isassa  21763  aspid  21782  aspval2  21805  pmatcoe1fsupp  22586  isbasis2g  22833  tgval2  22841  tgcl  22854  ppttop  22892  epttop  22894  ssntr  22943  ntreq0  22962  isclo  22972  restntr  23067  restlp  23068  cnpresti  23173  cnprest  23174  cnprest2  23175  lmss  23183  haust1  23237  nrmsep3  23240  isnrm2  23243  lmmo  23265  fincmp  23278  cmpsublem  23284  cmpsub  23285  uncmp  23288  hauscmplem  23291  dfconn2  23304  iunconnlem  23312  unconn  23314  is1stc2  23327  1stcrest  23338  1stcelcls  23346  llyi  23359  nllyi  23360  subislly  23366  lly1stc  23381  txcnp  23505  txcnmpt  23509  hausdiag  23530  kqcldsat  23618  isfbas2  23720  isfil2  23741  fbasfip  23753  elfg  23756  filconn  23768  rnelfmlem  23837  rnelfm  23838  fmfnfmlem2  23840  fmfnfmlem4  23842  fmfnfm  23843  flimrest  23868  hauspwpwf1  23872  fclsrest  23909  alexsubALTlem2  23933  alexsubALTlem3  23934  alexsubALTlem4  23935  alexsubALT  23936  istmd  23959  istgp  23962  tsmssubm  24028  tsmssplit  24037  istrg  24049  istdrg  24051  istlm  24070  ustfilxp  24098  utoptop  24120  utop3cls  24137  bldisj  24284  blin  24307  blres  24317  lpbl  24389  metrest  24410  restmetu  24456  isngp  24482  isnlm  24561  isnmhm  24632  xrtgioo  24693  xrsmopn  24699  icccmplem2  24710  reconnlem2  24714  icoopnst  24834  iocopnst  24835  bndth  24855  zclmncvs  25046  isncvsngp  25047  ncvsprp  25050  ncvsm1  25052  ncvsdif  25053  ncvspi  25054  ncvs1  25055  ncvspds  25059  iscph  25068  tcphcph  25135  cfilfcls  25172  cmetcaulem  25186  isbn  25236  cldcss2  25340  hlhil  25341  ovolfcl  25365  ovolicc2lem2  25417  ovolicc2  25421  shftmbl  25437  volfiniun  25446  mbfmax  25548  mbfimaopnlem  25554  mbfaddlem  25559  i1faddlem  25592  i1fmullem  25593  i1fres  25604  itg1climres  25613  mbfi1fseqlem4  25617  itg2splitlem  25647  itg2split  25648  itgresr  25678  ellimc2  25776  ellimc3  25778  limcun  25794  dvreslem  25808  dvne0  25914  itgsubstlem  25953  ig1pval3  26081  aaliou2  26246  aaliou2b  26247  pilem1  26359  rlimcnp2  26874  fsumharmonic  26920  ppisval2  27013  prmorcht  27086  fsumvma2  27123  pclogsum  27124  vmasum  27125  chpchtsum  27128  chpub  27129  rpvmasum2  27421  madeval2  27763  tglineineq  28588  trlsegvdeg  30171  frgrncvvdeqlem7  30249  frgrncvvdeqlem9  30251  minvecolem1  30818  minvecolem4a  30821  minvecolem4b  30822  minvecolem4  30824  h2hcau  30923  axhcompl-zf  30942  hhcmpl  31144  hhcms  31147  ocin  31240  ocnel  31242  shmodsi  31333  pjhthlem2  31336  omlsilem  31346  pjoc1i  31375  spansnm0i  31594  nonbooli  31595  5oalem7  31604  3oalem3  31608  pjssmii  31625  mayete3i  31672  nmcopex  31973  nmcoplb  31974  lncnopbd  31981  nmcfnex  31997  nmcfnlb  31998  riesz4  32008  riesz1  32009  riesz2  32010  cnlnadjlem3  32013  cnlnadjlem5  32015  cnlnadjlem9  32019  cnlnadjeu  32022  rnbra  32051  pjimai  32120  pjclem4a  32142  pj3lem1  32150  jpi  32214  sumdmdii  32359  sumdmdlem  32362  sumdmdlem2  32363  cdjreui  32376  cdj3lem1  32378  iunin1f  32501  disjorf  32523  ofpreima  32608  1stpreima  32649  2ndpreima  32650  iocinioc2  32722  ssnnssfz  32730  cntzun  33021  kerunit  33263  prmidl0  33387  ressply1mon1p  33503  ccfldextdgrr  33639  crefdf  33815  cmpcref  33817  cmppcmp  33825  cnre2csqima  33878  ordtconnlem1  33891  lmxrge0  33919  isrrext  33967  esum0  34016  esumcst  34030  esumpcvgval  34045  esumcvg  34053  measvuni  34181  eulerpartlemt0  34337  eulerpartlemr  34342  eulerpartlemgf  34347  eulerpartlemgs2  34348  eulerpartlemn  34349  fiblem  34366  oddprm2  34623  bnj1173  34969  bnj1174  34970  bnj1279  34985  elima4  35753  dfon2lem4  35764  ellimits  35888  dfom5b  35890  brapply  35916  brcap  35918  dfrecs2  35928  dfrdg4  35929  finminlem  36296  neibastop2lem  36338  neibastop2  36339  neifg  36349  tailfb  36355  onsucconni  36415  onintopssconn  36418  onsucsuccmpi  36421  limsucncmpi  36423  onint1  36427  bj-inrab  36905  bj-rcleqf  37003  bj-restuni  37075  bj-opelresdm  37123  bj-idres  37138  bj-opelidres  37139  bj-eldiag  37154  bj-eldiag2  37155  bj-ccinftydisj  37191  taupilem3  37297  isbasisrelowllem1  37333  isbasisrelowllem2  37334  nlpineqsn  37386  fvineqsneu  37389  ptrest  37603  poimirlem29  37633  poimirlem30  37634  mblfinlem2  37642  mbfposadd  37651  itg2gt0cn  37659  dvasin  37688  inixp  37712  0totbnd  37757  sstotbnd3  37760  heibor1lem  37793  heibor1  37794  heiborlem6  37800  isexid2  37839  smgrpismgmOLD  37846  issmgrpOLD  37847  mndoissmgrpOLD  37852  ismndo  37856  exidresid  37863  rngo1cl  37923  isfld2  37989  ineleq  38326  refressn  38424  eleccossin  38464  elrefsymrelsrel  38552  dfeldisj3  38701  disjlem14  38780  prtlem14  38857  lshpdisj  38970  lkrin  39147  ishlat1  39335  pmodlem2  39830  pclfinN  39883  pclcmpatN  39884  osumcllem4N  39942  pexmidlem1N  39953  dihmeetlem1N  41273  dihglblem5apreN  41274  dihmeetlem4preN  41289  dihmeetlem13N  41302  dochnel2  41375  lcdlss  41602  mapd1o  41631  baerlem3lem2  41693  baerlem5alem2  41694  baerlem5blem2  41695  redvmptabs  42337  cmpfiiin  42674  mrefg2  42684  fz1eqin  42746  fnwe2lem2  43028  islmodfg  43046  islssfg2  43048  lnr2i  43093  rp-fakeinunass  43492  fiinfi  43550  elinintab  43552  elinintrab  43554  elinlem  43575  cnvcnvintabd  43577  ntrneikb  44071  ntrneik3  44073  ntrneik13  44075  ismnushort  44278  radcnvrat  44291  nzin  44295  onfrALTlem2  44524  onfrALTlem2VD  44866  relpmin  44930  pwclaxpow  44962  dfac5prim  44968  modelac8prim  44970  permac8prim  44992  iooabslt  45484  iccintsng  45508  lptioo2cn  45630  lptioo1cn  45631  cncfuni  45871  icccncfext  45872  stoweidlem44  46029  fourierdlem42  46134  fourierdlem80  46171  sge00  46361  eldmressn  47025  afvres  47160  afv2res  47227  prproropf1olem0  47490  31prm  47585  rngccatidALTV  48260  rhmsubcALTVlem3  48271  funcringcsetcALTV2lem7  48284  ringccatidALTV  48294  ringcbasbasALTV  48300  funcringcsetclem7ALTV  48307  fldhmsubcALTV  48321  ssnn0ssfz  48337  elbigo2  48541  itsclinecirc0in  48764  resinsnALT  48861  opndisj  48891  clddisj  48892  i0oii  48908  io1ii  48909