Theorem elin 3930

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 3468	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 3468	. . 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 3921	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 3647	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 378	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

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

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 3449  df-in 3921

This theorem is referenced by:  elini  4162  elind  4163  elinel1  4164  elinel2  4165  elin2  4166  elin3  4169  ineqri  4175  nfin  4187  inass  4191  ssin  4202  ssrin  4205  ralin  4212  rexin  4213  dfss4  4232  difin  4235  indi  4247  undi  4248  unineq  4251  indifdi  4257  difin2  4264  inrab2  4280  ndisj  4333  inn0f  4334  difin0ss  4336  inssdif0  4337  inelcm  4428  inundif  4442  elinsn  4674  uniin  4895  intun  4944  intprg  4945  elrint  4953  iunin2  5035  iinin2  5042  elriin  5045  disjor  5089  disjiun  5095  brin  5159  trin  5226  inex1  5272  inuni  5305  wefrc  5632  inopab  5792  inxp  5795  inxpOLD  5796  dmin  5875  dfres3  5955  intasym  6088  asymref  6089  dminss  6126  imainss  6127  inimasn  6129  cnvresima  6203  dfco2a  6219  ordtri3or  6364  2elresin  6639  respreima  7038  fvcofneq  7065  tpres  7175  isomin  7312  isoini  7313  offval  7662  ordpwsuc  7790  frpoins3xpg  8119  frpoins3xp3g  8120  xpord3pred  8131  ressuppss  8162  frrlem13  8277  fprlem1  8279  uniinqs  8770  mapval2  8845  ixpin  8896  boxriin  8913  disjen  9098  ssenen  9115  onfin2  9180  elfpw  9305  fiin  9373  inf3lem2  9582  epfrs  9684  cp  9844  dfac5lem1  10076  dfac5lem5  10080  dfac5  10082  kmlem3  10106  kmlem14  10117  kmlem15  10118  fin23lem26  10278  pwxpndom2  10618  ingru  10768  gruina  10771  grur1  10773  axgroth4  10785  grothprim  10787  ixxdisj  13321  icodisj  13437  fzdisj  13512  nn0disj  13605  fzouzdisj  13656  cotr2g  14942  limsupgle  15443  ello12  15482  elo12  15493  lo1resb  15530  rlimresb  15531  o1resb  15532  lo1eq  15534  rlimeq  15535  fsumsplit  15707  sumsplit  15734  fsum2dlem  15736  fprod2dlem  15946  bitsmod  16406  saddisjlem  16434  sadadd  16437  sadass  16441  smuval2  16452  smupval  16458  smueqlem  16460  smumul  16463  isprm7  16678  prmreclem5  16891  prmrec  16893  4sqlem12  16927  vdwmc  16949  setsstruct2  17144  acsfn  17620  iszeroo  17960  iszeroi  17971  fpwipodrs  18499  psss  18539  insubm  18745  subgacs  19093  nsgacs  19094  resscntz  19265  gsmsymgreq  19362  sylow2a  19549  lsmmod  19605  lsmdisj2  19612  gsumzsplit  19857  subgdmdprd  19966  dprdcntz2  19970  dprddisj2  19971  pgpfac1lem3  20009  rnghmval2  20353  isrhm  20387  subsubrng2  20473  subsubrg2  20508  rnghmsubcsetclem1  20540  funcrngcsetcALT  20550  zrinitorngc  20551  zrtermorngc  20552  rhmsubcsetclem1  20569  rhmsubcrngclem1  20575  ringcbasbas  20582  zrtermoringc  20584  srhmsubclem1  20586  fldhmsubc  20694  acsfn1p  20708  subrgacs  20709  sdrgacs  20710  lssacs  20873  lspdisj  21035  lspdisjb  21036  dfprm2  21383  irinitoringc  21389  ocvin  21583  unocv  21589  iunocv  21590  obselocv  21637  isassa  21765  aspid  21784  aspval2  21807  pmatcoe1fsupp  22588  isbasis2g  22835  tgval2  22843  tgcl  22856  ppttop  22894  epttop  22896  ssntr  22945  ntreq0  22964  isclo  22974  restntr  23069  restlp  23070  cnpresti  23175  cnprest  23176  cnprest2  23177  lmss  23185  haust1  23239  nrmsep3  23242  isnrm2  23245  lmmo  23267  fincmp  23280  cmpsublem  23286  cmpsub  23287  uncmp  23290  hauscmplem  23293  dfconn2  23306  iunconnlem  23314  unconn  23316  is1stc2  23329  1stcrest  23340  1stcelcls  23348  llyi  23361  nllyi  23362  subislly  23368  lly1stc  23383  txcnp  23507  txcnmpt  23511  hausdiag  23532  kqcldsat  23620  isfbas2  23722  isfil2  23743  fbasfip  23755  elfg  23758  filconn  23770  rnelfmlem  23839  rnelfm  23840  fmfnfmlem2  23842  fmfnfmlem4  23844  fmfnfm  23845  flimrest  23870  hauspwpwf1  23874  fclsrest  23911  alexsubALTlem2  23935  alexsubALTlem3  23936  alexsubALTlem4  23937  alexsubALT  23938  istmd  23961  istgp  23964  tsmssubm  24030  tsmssplit  24039  istrg  24051  istdrg  24053  istlm  24072  ustfilxp  24100  utoptop  24122  utop3cls  24139  bldisj  24286  blin  24309  blres  24319  lpbl  24391  metrest  24412  restmetu  24458  isngp  24484  isnlm  24563  isnmhm  24634  xrtgioo  24695  xrsmopn  24701  icccmplem2  24712  reconnlem2  24716  icoopnst  24836  iocopnst  24837  bndth  24857  zclmncvs  25048  isncvsngp  25049  ncvsprp  25052  ncvsm1  25054  ncvsdif  25055  ncvspi  25056  ncvs1  25057  ncvspds  25061  iscph  25070  tcphcph  25137  cfilfcls  25174  cmetcaulem  25188  isbn  25238  cldcss2  25342  hlhil  25343  ovolfcl  25367  ovolicc2lem2  25419  ovolicc2  25423  shftmbl  25439  volfiniun  25448  mbfmax  25550  mbfimaopnlem  25556  mbfaddlem  25561  i1faddlem  25594  i1fmullem  25595  i1fres  25606  itg1climres  25615  mbfi1fseqlem4  25619  itg2splitlem  25649  itg2split  25650  itgresr  25680  ellimc2  25778  ellimc3  25780  limcun  25796  dvreslem  25810  dvne0  25916  itgsubstlem  25955  ig1pval3  26083  aaliou2  26248  aaliou2b  26249  pilem1  26361  rlimcnp2  26876  fsumharmonic  26922  ppisval2  27015  prmorcht  27088  fsumvma2  27125  pclogsum  27126  vmasum  27127  chpchtsum  27130  chpub  27131  rpvmasum2  27423  madeval2  27761  tglineineq  28570  trlsegvdeg  30156  frgrncvvdeqlem7  30234  frgrncvvdeqlem9  30236  minvecolem1  30803  minvecolem4a  30806  minvecolem4b  30807  minvecolem4  30809  h2hcau  30908  axhcompl-zf  30927  hhcmpl  31129  hhcms  31132  ocin  31225  ocnel  31227  shmodsi  31318  pjhthlem2  31321  omlsilem  31331  pjoc1i  31360  spansnm0i  31579  nonbooli  31580  5oalem7  31589  3oalem3  31593  pjssmii  31610  mayete3i  31657  nmcopex  31958  nmcoplb  31959  lncnopbd  31966  nmcfnex  31982  nmcfnlb  31983  riesz4  31993  riesz1  31994  riesz2  31995  cnlnadjlem3  31998  cnlnadjlem5  32000  cnlnadjlem9  32004  cnlnadjeu  32007  rnbra  32036  pjimai  32105  pjclem4a  32127  pj3lem1  32135  jpi  32199  sumdmdii  32344  sumdmdlem  32347  sumdmdlem2  32348  cdjreui  32361  cdj3lem1  32363  iunin1f  32486  disjorf  32508  ofpreima  32589  1stpreima  32630  2ndpreima  32631  iocinioc2  32702  ssnnssfz  32710  cntzun  33008  isorng  33277  kerunit  33297  prmidl0  33421  ressply1mon1p  33537  ccfldextdgrr  33667  crefdf  33838  cmpcref  33840  cmppcmp  33848  cnre2csqima  33901  ordtconnlem1  33914  lmxrge0  33942  isrrext  33990  esum0  34039  esumcst  34053  esumpcvgval  34068  esumcvg  34076  measvuni  34204  eulerpartlemt0  34360  eulerpartlemr  34365  eulerpartlemgf  34370  eulerpartlemgs2  34371  eulerpartlemn  34372  fiblem  34389  oddprm2  34646  bnj1173  34992  bnj1174  34993  bnj1279  35008  elima4  35763  dfon2lem4  35774  ellimits  35898  dfom5b  35900  brapply  35926  brcap  35928  dfrecs2  35938  dfrdg4  35939  finminlem  36306  neibastop2lem  36348  neibastop2  36349  neifg  36359  tailfb  36365  onsucconni  36425  onintopssconn  36428  onsucsuccmpi  36431  limsucncmpi  36433  onint1  36437  bj-inrab  36915  bj-rcleqf  37013  bj-restuni  37085  bj-opelresdm  37133  bj-idres  37148  bj-opelidres  37149  bj-eldiag  37164  bj-eldiag2  37165  bj-ccinftydisj  37201  taupilem3  37307  isbasisrelowllem1  37343  isbasisrelowllem2  37344  nlpineqsn  37396  fvineqsneu  37399  ptrest  37613  poimirlem29  37643  poimirlem30  37644  mblfinlem2  37652  mbfposadd  37661  itg2gt0cn  37669  dvasin  37698  inixp  37722  0totbnd  37767  sstotbnd3  37770  heibor1lem  37803  heibor1  37804  heiborlem6  37810  isexid2  37849  smgrpismgmOLD  37856  issmgrpOLD  37857  mndoissmgrpOLD  37862  ismndo  37866  exidresid  37873  rngo1cl  37933  isfld2  37999  ineleq  38336  refressn  38434  eleccossin  38474  elrefsymrelsrel  38562  dfeldisj3  38711  disjlem14  38790  prtlem14  38867  lshpdisj  38980  lkrin  39157  ishlat1  39345  pmodlem2  39841  pclfinN  39894  pclcmpatN  39895  osumcllem4N  39953  pexmidlem1N  39964  dihmeetlem1N  41284  dihglblem5apreN  41285  dihmeetlem4preN  41300  dihmeetlem13N  41313  dochnel2  41386  lcdlss  41613  mapd1o  41642  baerlem3lem2  41704  baerlem5alem2  41705  baerlem5blem2  41706  redvmptabs  42348  cmpfiiin  42685  mrefg2  42695  fz1eqin  42757  fnwe2lem2  43040  islmodfg  43058  islssfg2  43060  lnr2i  43105  rp-fakeinunass  43504  fiinfi  43562  elinintab  43564  elinintrab  43566  elinlem  43587  cnvcnvintabd  43589  ntrneikb  44083  ntrneik3  44085  ntrneik13  44087  ismnushort  44290  radcnvrat  44303  nzin  44307  onfrALTlem2  44536  onfrALTlem2VD  44878  relpmin  44942  pwclaxpow  44974  dfac5prim  44980  modelac8prim  44982  permac8prim  45004  iooabslt  45497  iccintsng  45521  lptioo2cn  45643  lptioo1cn  45644  cncfuni  45884  icccncfext  45885  stoweidlem44  46042  fourierdlem42  46147  fourierdlem80  46184  sge00  46374  eldmressn  47038  afvres  47173  afv2res  47240  prproropf1olem0  47503  31prm  47598  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