Theorem elin 4169

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 3512	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 3512	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	adantl 484	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2900	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2900	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	4, 5	anbi12d 632	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
7		df-in 3943	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 3668	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 382	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  Vcvv 3494   ∩ cin 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3943

This theorem is referenced by:  elini  4170  elind  4171  elinel1  4172  elinel2  4173  elin2  4174  elin3  4177  incomOLD  4179  ineqri  4180  ineq1OLD  4182  inass  4196  ssin  4207  ssrin  4210  rexin  4216  dfss4  4235  difin  4238  indi  4250  undi  4251  unineq  4254  indifdir  4260  difin2  4266  inrab2  4276  ndisj  4327  difin0ss  4328  inssdif0  4329  inelcm  4414  inundif  4427  elinsn  4646  uniin  4862  intun  4908  intpr  4909  elrint  4917  iunin2  4993  iinin2  5000  elriin  5003  disjor  5046  disjiun  5053  brin  5118  trin  5182  inex1  5221  inuni  5246  wefrc  5549  inopab  5701  inxp  5703  dmin  5780  dfres3  5858  intasym  5975  asymref  5976  dminss  6010  imainss  6011  inimasn  6013  cnvresima  6087  dfco2a  6099  ordtri3or  6223  2elresin  6468  respreima  6836  fvcofneq  6859  tpres  6963  isomin  7090  isoini  7091  offval  7416  ordpwsuc  7530  ressuppss  7849  wfrlem5  7959  uniinqs  8377  mapval2  8436  ixpin  8487  boxriin  8504  disjen  8674  ssenen  8691  onfin2  8710  elfpw  8826  fiin  8886  inf3lem2  9092  epfrs  9173  cp  9320  dfac5lem1  9549  dfac5lem5  9553  dfac5  9554  kmlem3  9578  kmlem14  9589  kmlem15  9590  fin23lem26  9747  pwxpndom2  10087  ingru  10237  gruina  10240  grur1  10242  axgroth4  10254  grothprim  10256  ixxdisj  12754  icodisj  12863  fzdisj  12935  nn0disj  13024  fzouzdisj  13074  cotr2g  14336  limsupgle  14834  ello12  14873  elo12  14884  lo1resb  14921  rlimresb  14922  o1resb  14923  lo1eq  14925  rlimeq  14926  fsumsplit  15097  sumsplit  15123  fsum2dlem  15125  fprod2dlem  15334  bitsmod  15785  saddisjlem  15813  sadadd  15816  sadass  15820  smuval2  15831  smupval  15837  smueqlem  15839  smumul  15842  isprm7  16052  prmreclem5  16256  prmrec  16258  4sqlem12  16292  vdwmc  16314  setsstruct2  16521  acsfn  16930  iszeroo  17262  iszeroi  17269  fpwipodrs  17774  psss  17824  insubm  17983  subgacs  18313  nsgacs  18314  resscntz  18462  gsmsymgreq  18560  sylow2a  18744  lsmmod  18801  lsmdisj2  18808  gsumzsplit  19047  subgdmdprd  19156  dprdcntz2  19160  dprddisj2  19161  pgpfac1lem3  19199  isrhm  19473  subsubrg2  19562  acsfn1p  19578  subrgacs  19579  sdrgacs  19580  lssacs  19739  lspdisj  19897  lspdisjb  19898  isassa  20088  aspid  20104  aspval2  20127  dfprm2  20641  ocvin  20818  unocv  20824  iunocv  20825  obselocv  20872  pmatcoe1fsupp  21309  isbasis2g  21556  tgval2  21564  tgcl  21577  ppttop  21615  epttop  21617  ssntr  21666  ntreq0  21685  isclo  21695  restntr  21790  restlp  21791  cnpresti  21896  cnprest  21897  cnprest2  21898  lmss  21906  haust1  21960  nrmsep3  21963  isnrm2  21966  lmmo  21988  fincmp  22001  cmpsublem  22007  cmpsub  22008  uncmp  22011  hauscmplem  22014  dfconn2  22027  iunconnlem  22035  unconn  22037  is1stc2  22050  1stcrest  22061  1stcelcls  22069  llyi  22082  nllyi  22083  subislly  22089  lly1stc  22104  txcnp  22228  txcnmpt  22232  hausdiag  22253  kqcldsat  22341  isfbas2  22443  isfil2  22464  fbasfip  22476  elfg  22479  filconn  22491  rnelfmlem  22560  rnelfm  22561  fmfnfmlem2  22563  fmfnfmlem4  22565  fmfnfm  22566  flimrest  22591  hauspwpwf1  22595  fclsrest  22632  alexsubALTlem2  22656  alexsubALTlem3  22657  alexsubALTlem4  22658  alexsubALT  22659  istmd  22682  istgp  22685  tsmssubm  22751  tsmssplit  22760  istrg  22772  istdrg  22774  istlm  22793  ustfilxp  22821  utoptop  22843  utop3cls  22860  bldisj  23008  blin  23031  blres  23041  lpbl  23113  metrest  23134  restmetu  23180  isngp  23205  isnlm  23284  isnmhm  23355  xrtgioo  23414  xrsmopn  23420  icccmplem2  23431  reconnlem2  23435  icoopnst  23543  iocopnst  23544  bndth  23562  zclmncvs  23752  isncvsngp  23753  ncvsprp  23756  ncvsm1  23758  ncvsdif  23759  ncvspi  23760  ncvs1  23761  ncvspds  23765  iscph  23774  tcphcph  23840  cfilfcls  23877  cmetcaulem  23891  isbn  23941  cldcss2  24045  hlhil  24046  ovolfcl  24067  ovolicc2lem2  24119  ovolicc2  24123  shftmbl  24139  volfiniun  24148  mbfmax  24250  mbfimaopnlem  24256  mbfaddlem  24261  i1faddlem  24294  i1fmullem  24295  i1fres  24306  itg1climres  24315  mbfi1fseqlem4  24319  itg2splitlem  24349  itg2split  24350  itgresr  24379  ellimc2  24475  ellimc3  24477  limcun  24493  dvreslem  24507  dvne0  24608  itgsubstlem  24645  ig1pval3  24768  aaliou2  24929  aaliou2b  24930  pilem1  25039  rlimcnp2  25544  fsumharmonic  25589  ppisval2  25682  prmorcht  25755  fsumvma2  25790  pclogsum  25791  vmasum  25792  chpchtsum  25795  chpub  25796  rpvmasum2  26088  tglineineq  26429  trlsegvdeg  28006  frgrncvvdeqlem7  28084  frgrncvvdeqlem9  28086  minvecolem1  28651  minvecolem4a  28654  minvecolem4b  28655  minvecolem4  28657  h2hcau  28756  axhcompl-zf  28775  hhcmpl  28977  hhcms  28980  ocin  29073  ocnel  29075  shmodsi  29166  pjhthlem2  29169  omlsilem  29179  pjoc1i  29208  spansnm0i  29427  nonbooli  29428  5oalem7  29437  3oalem3  29441  pjssmii  29458  mayete3i  29505  nmcopex  29806  nmcoplb  29807  lncnopbd  29814  nmcfnex  29830  nmcfnlb  29831  riesz4  29841  riesz1  29842  riesz2  29843  cnlnadjlem3  29846  cnlnadjlem5  29848  cnlnadjlem9  29852  cnlnadjeu  29855  rnbra  29884  pjimai  29953  pjclem4a  29975  pj3lem1  29983  jpi  30047  sumdmdii  30192  sumdmdlem  30195  sumdmdlem2  30196  cdjreui  30209  cdj3lem1  30211  iunin1f  30309  disjorf  30329  ofpreima  30410  1stpreima  30442  2ndpreima  30443  iocinioc2  30502  ssnnssfz  30510  cntzun  30695  isorng  30872  kerunit  30896  ccfldextdgrr  31057  crefdf  31112  cmpcref  31114  cmppcmp  31122  cnre2csqima  31154  ordtconnlem1  31167  lmxrge0  31195  isrrext  31241  esum0  31308  esumcst  31322  esumpcvgval  31337  esumcvg  31345  measvuni  31473  eulerpartlemt0  31627  eulerpartlemr  31632  eulerpartlemgf  31637  eulerpartlemgs2  31638  eulerpartlemn  31639  fiblem  31656  oddprm2  31926  bnj521  32007  bnj1173  32274  bnj1174  32275  bnj1279  32290  elima4  33019  dfon2lem4  33031  frrlem13  33135  fprlem1  33137  madeval2  33290  ellimits  33371  dfom5b  33373  brapply  33399  brcap  33401  dfrecs2  33411  dfrdg4  33412  finminlem  33666  neibastop2lem  33708  neibastop2  33709  neifg  33719  tailfb  33725  onsucconni  33785  onintopssconn  33788  onsucsuccmpi  33791  limsucncmpi  33793  onint1  33797  bj-inrab  34248  bj-rcleqf  34340  bj-restuni  34391  bj-opelresdm  34440  bj-idres  34455  bj-opelidres  34456  bj-eldiag  34471  bj-eldiag2  34472  bj-ccinftydisj  34498  taupilem3  34603  isbasisrelowllem1  34639  isbasisrelowllem2  34640  nlpineqsn  34692  fvineqsneu  34695  ptrest  34906  poimirlem29  34936  poimirlem30  34937  mblfinlem2  34945  mbfposadd  34954  itg2gt0cn  34962  dvasin  34993  inixp  35018  0totbnd  35066  sstotbnd3  35069  heibor1lem  35102  heibor1  35103  heiborlem6  35109  isexid2  35148  smgrpismgmOLD  35155  issmgrpOLD  35156  mndoissmgrpOLD  35161  ismndo  35165  exidresid  35172  rngo1cl  35232  isfld2  35298  ineleq  35623  eleccossin  35738  elrefsymrelsrel  35822  dfeldisj3  35967  prtlem14  36025  lshpdisj  36138  lkrin  36315  ishlat1  36503  pmodlem2  36998  pclfinN  37051  pclcmpatN  37052  osumcllem4N  37110  pexmidlem1N  37121  dihmeetlem1N  38441  dihglblem5apreN  38442  dihmeetlem4preN  38457  dihmeetlem13N  38470  dochnel2  38543  lcdlss  38770  mapd1o  38799  baerlem3lem2  38861  baerlem5alem2  38862  baerlem5blem2  38863  cmpfiiin  39343  mrefg2  39353  fz1eqin  39415  fnwe2lem2  39700  islmodfg  39718  islssfg2  39720  lnr2i  39765  rp-fakeinunass  39930  fiinfi  39981  elinintab  39984  elinintrab  39986  elinlem  40007  cnvcnvintabd  40009  ntrneikb  40493  ntrneik3  40495  ntrneik13  40497  radcnvrat  40695  nzin  40699  onfrALTlem2  40929  onfrALTlem2VD  41272  inn0f  41384  iooabslt  41823  iccintsng  41848  lptioo2cn  41975  lptioo1cn  41976  cncfuni  42218  icccncfext  42219  stoweidlem44  42378  fourierdlem42  42483  fourierdlem80  42520  sge00  42707  eldmressn  43321  afvres  43420  afv2res  43487  prproropf1olem0  43713  31prm  43809  rnghmval2  44215  rnghmsubcsetclem1  44295  rngccatidALTV  44309  funcrngcsetcALT  44319  zrinitorngc  44320  zrtermorngc  44321  rhmsubcsetclem1  44341  rhmsubcrngclem1  44347  ringcbasbas  44354  funcringcsetcALTV2lem7  44362  ringccatidALTV  44372  ringcbasbasALTV  44378  funcringcsetclem7ALTV  44385  irinitoringc  44389  zrtermoringc  44390  srhmsubclem1  44393  fldhmsubc  44404  fldhmsubcALTV  44422  rhmsubcALTVlem3  44426  ssnn0ssfz  44446  elbigo2  44661  itsclinecirc0in  44811