Theorem elin 3920

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 3475	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 3475	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	adantl 485	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2850	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2850	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	4, 5	anbi12d 641	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
7		df-in 3911	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 3639	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 380	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 208   ∧ wa 399   = wceq 1560   ∈ wcel 2142  Vcvv 3454   ∩ cin 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-in 3911

This theorem is referenced by:  elini  4151  elind  4152  elinel1  4153  elinel2  4154  elin2  4155  elin3  4158  ineqri  4164  nfin  4176  inass  4179  ssin  4190  ssrin  4193  ralin  4201  rexin  4202  dfss4  4221  difin  4224  indi  4236  undi  4237  unineq  4240  indifdi  4246  difin2  4253  inrab2  4269  ndisj  4323  inn0f  4324  difin0ss  4326  inssdif0  4327  inelcm  4419  inundif  4433  elinsn  4669  uniinOLD  4890  intun  4938  intprg  4939  elrint  4947  iunin2  5028  iinin2  5035  elriin  5038  disjor  5082  disjiun  5088  brin  5152  trin  5219  inex1  5273  inuni  5306  wefrc  5641  inopab  5802  inxp  5804  dmin  5887  dfres3  5970  intasym  6102  asymref  6103  dminss  6138  imainss  6139  inimasn  6141  cnvresima  6217  dfco2a  6233  ordtri3or  6378  2elresin  6642  respreima  7047  fvcofneq  7074  tpres  7185  isomin  7321  isoini  7322  offval  7669  ordpwsuc  7795  frpoins3xpg  8120  frpoins3xp3g  8121  xpord3pred  8132  ressuppss  8163  frrlem13  8279  fprlem1  8281  uniinqs  8779  mapval2  8854  ixpin  8905  boxriin  8922  disjen  9106  ssenen  9123  onfin2  9185  elfpw  9297  fiin  9368  inf3lem2  9584  epfrs  9686  cp  9849  dfac5lem1  10079  dfac5lem5  10083  dfac5  10085  kmlem3  10109  kmlem14  10120  kmlem15  10121  fin23lem26  10282  pwxpndom2  10623  ingru  10773  gruina  10776  grur1  10778  axgroth4  10790  grothprim  10792  ixxdisj  13364  icodisj  13480  fzdisj  13556  nn0disj  13649  fzouzdisj  13701  cotr2g  14989  limsupgle  15504  ello12  15543  elo12  15554  lo1resb  15591  rlimresb  15592  o1resb  15593  lo1eq  15595  rlimeq  15596  fsumsplit  15768  sumsplit  15795  fsum2dlem  15797  fprod2dlem  16010  bitsmod  16470  saddisjlem  16498  sadadd  16501  sadass  16505  smuval2  16516  smupval  16522  smueqlem  16524  smumul  16527  isprm7  16743  prmreclem5  16956  prmrec  16958  4sqlem12  16992  vdwmc  17014  setsstruct2  17210  acsfn  17691  iszeroo  18031  iszeroi  18042  fpwipodrs  18572  psss  18612  insubm  18852  subgacs  19202  nsgacs  19203  resscntz  19373  gsmsymgreq  19472  sylow2a  19659  lsmmod  19715  lsmdisj2  19722  gsumzsplit  19967  subgdmdprd  20076  dprdcntz2  20080  dprddisj2  20081  pgpfac1lem3  20119  rnghmval2  20493  isrhm  20527  subsubrng2  20614  subsubrg2  20649  rnghmsubcsetclem1  20681  funcrngcsetcALT  20691  zrinitorngc  20692  zrtermorngc  20693  rhmsubcsetclem1  20710  rhmsubcrngclem1  20716  ringcbasbas  20723  zrtermoringc  20725  srhmsubclem1  20727  fldhmsubc  20834  acsfn1p  20848  subrgacs  20849  sdrgacs  20850  isorng  20910  lssacs  21034  lspdisj  21195  lspdisjb  21196  dfprm2  21525  irinitoringc  21531  ocvin  21726  unocv  21732  iunocv  21733  obselocv  21780  isassa  21908  aspid  21926  aspval2  21950  pmatcoe1fsupp  22761  isbasis2g  23008  tgval2  23016  tgcl  23029  ppttop  23067  epttop  23069  ssntr  23118  ntreq0  23137  isclo  23147  restntr  23242  restlp  23243  cnpresti  23348  cnprest  23349  cnprest2  23350  lmss  23358  haust1  23412  nrmsep3  23415  isnrm2  23418  lmmo  23440  fincmp  23453  cmpsublem  23459  cmpsub  23460  uncmp  23463  hauscmplem  23466  dfconn2  23479  iunconnlem  23487  unconn  23489  is1stc2  23502  1stcrest  23513  1stcelcls  23521  llyi  23534  nllyi  23535  subislly  23541  lly1stc  23556  txcnp  23680  txcnmpt  23684  hausdiag  23705  kqcldsat  23793  isfbas2  23895  isfil2  23916  fbasfip  23928  elfg  23931  filconn  23943  rnelfmlem  24012  rnelfm  24013  fmfnfmlem2  24015  fmfnfmlem4  24017  fmfnfm  24018  flimrest  24043  hauspwpwf1  24047  fclsrest  24084  alexsubALTlem2  24108  alexsubALTlem3  24109  alexsubALTlem4  24110  alexsubALT  24111  istmd  24134  istgp  24137  tsmssubm  24203  tsmssplit  24212  istrg  24224  istdrg  24226  istlm  24245  ustfilxp  24273  utoptop  24294  utop3cls  24311  bldisj  24458  blin  24481  blres  24491  lpbl  24563  metrest  24584  restmetu  24630  isngp  24656  isnlm  24735  isnmhm  24806  xrtgioo  24867  xrsmopn  24873  icccmplem2  24884  reconnlem2  24888  icoopnst  25001  iocopnst  25002  bndth  25020  zclmncvs  25210  isncvsngp  25211  ncvsprp  25214  ncvsm1  25216  ncvsdif  25217  ncvspi  25218  ncvs1  25219  ncvspds  25223  iscph  25232  tcphcph  25299  cfilfcls  25336  cmetcaulem  25350  isbn  25400  cldcss2  25504  hlhil  25505  ovolfcl  25528  ovolicc2lem2  25580  ovolicc2  25584  shftmbl  25600  volfiniun  25609  mbfmax  25711  mbfimaopnlem  25717  mbfaddlem  25722  i1faddlem  25755  i1fmullem  25756  i1fres  25767  itg1climres  25776  mbfi1fseqlem4  25780  itg2splitlem  25810  itg2split  25811  itgresr  25841  ellimc2  25939  ellimc3  25941  limcun  25957  dvreslem  25971  dvne0  26073  itgsubstlem  26110  ig1pval3  26238  aaliou2  26404  aaliou2b  26405  pilem1  26514  rlimcnp2  27031  fsumharmonic  27076  ppisval2  27169  prmorcht  27242  fsumvma2  27278  pclogsum  27279  vmasum  27280  chpchtsum  27283  chpub  27284  rpvmasum2  27576  madeval2  27926  tglineineq  28812  trlsegvdeg  30429  frgrncvvdeqlem7  30507  frgrncvvdeqlem9  30509  minvecolem1  31077  minvecolem4a  31080  minvecolem4b  31081  minvecolem4  31083  h2hcau  31182  axhcompl-zf  31201  hhcmpl  31403  hhcms  31406  ocin  31499  ocnel  31501  shmodsi  31592  pjhthlem2  31595  omlsilem  31605  pjoc1i  31634  spansnm0i  31853  nonbooli  31854  5oalem7  31863  3oalem3  31867  pjssmii  31884  mayete3i  31931  nmcopex  32232  nmcoplb  32233  lncnopbd  32240  nmcfnex  32256  nmcfnlb  32257  riesz4  32267  riesz1  32268  riesz2  32269  cnlnadjlem3  32272  cnlnadjlem5  32274  cnlnadjlem9  32278  cnlnadjeu  32281  rnbra  32310  pjimai  32379  pjclem4a  32401  pj3lem1  32409  jpi  32473  sumdmdii  32618  sumdmdlem  32621  sumdmdlem2  32622  cdjreui  32635  cdj3lem1  32637  iunin1f  32757  disjorf  32779  ofpreima  32867  1stpreima  32909  2ndpreima  32910  iocinioc2  32981  ssnnssfz  32989  cntzun  33259  kerunit  33511  prmidl0  33637  ressply1mon1p  33764  ccfldextdgrr  33969  crefdf  34145  cmpcref  34147  cmppcmp  34155  cnre2csqima  34208  ordtconnlem1  34221  lmxrge0  34249  isrrext  34297  esum0  34346  esumcst  34360  esumpcvgval  34375  esumcvg  34383  measvuni  34511  eulerpartlemt0  34666  eulerpartlemr  34671  eulerpartlemgf  34676  eulerpartlemgs2  34677  eulerpartlemn  34678  fiblem  34695  oddprm2  34949  bnj1173  35297  bnj1174  35298  bnj1279  35313  elima4  36126  dfon2lem4  36134  ellimits  36258  dfom5b  36260  brapply  36286  brcap  36288  dfrecs2  36300  dfrdg4  36301  finminlem  36678  neibastop2lem  36720  neibastop2  36721  neifg  36731  tailfb  36737  onsucconni  36797  onintopssconn  36800  onsucsuccmpi  36803  limsucncmpi  36805  onint1  36809  mh-infprim2bi  36907  bj-inrab  37412  bj-rcleqf  37510  bj-restuni  37587  bj-opelresdm  37637  bj-idres  37652  bj-opelidres  37653  bj-eldiag  37668  bj-eldiag2  37669  bj-ccinftydisj  37705  taupilem3  37811  isbasisrelowllem1  37849  isbasisrelowllem2  37850  nlpineqsn  37902  fvineqsneu  37905  ptrest  38118  poimirlem29  38148  poimirlem30  38149  mblfinlem2  38157  mbfposadd  38166  itg2gt0cn  38174  dvasin  38203  inixp  38227  0totbnd  38272  sstotbnd3  38275  heibor1lem  38308  heibor1  38309  heiborlem6  38315  isexid2  38354  smgrpismgmOLD  38361  issmgrpOLD  38362  mndoissmgrpOLD  38367  ismndo  38371  exidresid  38378  rngo1cl  38438  isfld2  38504  ineleq  38853  refressn  39032  eleccossin  39072  elrefsymrelsrel  39154  dfeldisj3  39310  eldisjdmqsim  39316  disjlem14  39400  prtlem14  39498  lshpdisj  39611  lkrin  39788  ishlat1  39976  pmodlem2  40471  pclfinN  40524  pclcmpatN  40525  osumcllem4N  40583  pexmidlem1N  40594  dihmeetlem1N  41914  dihglblem5apreN  41915  dihmeetlem4preN  41930  dihmeetlem13N  41943  dochnel2  42016  lcdlss  42243  mapd1o  42272  baerlem3lem2  42334  baerlem5alem2  42335  baerlem5blem2  42336  redvmptabs  42969  cmpfiiin  43278  mrefg2  43288  fz1eqin  43350  fnwe2lem2  43628  islmodfg  43646  islssfg2  43648  lnr2i  43693  rp-fakeinunass  44091  fiinfi  44149  elinintab  44151  elinintrab  44153  elinlem  44174  cnvcnvintabd  44176  ntrneikb  44670  ntrneik3  44672  ntrneik13  44674  ismnushort  44877  radcnvrat  44890  nzin  44894  onfrALTlem2  45122  onfrALTlem2VD  45464  relpmin  45528  pwclaxpow  45560  dfac5prim  45566  modelac8prim  45568  permac8prim  45590  iooabslt  46075  iccintsng  46099  lptioo2cn  46219  lptioo1cn  46220  cncfuni  46460  icccncfext  46461  stoweidlem44  46618  fourierdlem42  46723  fourierdlem80  46760  sge00  46950  eldmressn  47631  afvres  47766  afv2res  47833  prproropf1olem0  48108  31prm  48206  indprmfz  48239  rngccatidALTV  48894  rhmsubcALTVlem3  48905  funcringcsetcALTV2lem7  48918  ringccatidALTV  48928  ringcbasbasALTV  48934  funcringcsetclem7ALTV  48941  fldhmsubcALTV  48955  ssnn0ssfz  48971  elbigo2  49174  itsclinecirc0in  49397  resinsnALT  49494  opndisj  49524  clddisj  49525  i0oii  49541  io1ii  49542