Theorem elin 3922

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 3478	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 3478	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	adantl 487	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2853	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2853	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	4, 5	anbi12d 644	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
7		df-in 3913	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 3641	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 381	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2146  Vcvv 3457   ∩ cin 3905

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3913

This theorem is used by:  elini  4152  elind  4153  elinel1  4154  elinel2  4155  elin2  4156  elin3  4159  ineqri  4165  nfin  4177  inass  4180  ssin  4191  ssrin  4194  ralin  4202  rexin  4203  dfss4  4222  difin  4225  indi  4237  undi  4238  unineq  4241  indifdi  4247  difin2  4254  inrab2  4270  ndisj  4325  inn0f  4326  difin0ss  4328  inssdif0OLD  4330  inelcm  4425  inundif  4442  elinsn  4678  uniinOLD  4899  intun  4947  intprg  4948  elrint  4956  iunin2  5037  iinin2  5046  elriin  5049  disjor  5093  disjiun  5099  brin  5165  trin  5232  inex1  5288  inuni  5322  wefrc  5657  inopab  5818  inxp  5820  dmin  5903  dfres3  5985  intasym  6117  asymref  6118  dminss  6152  imainss  6153  inimasn  6155  cnvresima  6233  dfco2a  6249  ordtri3or  6397  2elresin  6660  respreima  7065  fvcofneq  7092  tpres  7206  isomin  7344  isoini  7345  offval  7693  ordpwsuc  7817  frpoins3xpg  8142  frpoins3xp3g  8143  xpord3pred  8154  ressuppss  8185  frrlem13  8301  fprlem1  8303  uniinqs  8801  mapval2  8876  ixpin  8927  boxriin  8944  disjen  9129  ssenen  9146  onfin2  9208  elfpw  9318  fiin  9389  inf3lem2  9605  epfrs  9707  cp  9890  dfac5lem1  10123  dfac5lem5  10127  dfac5  10128  kmlem3  10152  kmlem14  10163  kmlem15  10164  fin23lem26  10324  pwxpndom2  10667  ingru  10817  gruina  10820  grur1  10822  axgroth4  10834  grothprim  10836  ixxdisj  13405  icodisj  13521  fzdisj  13598  nn0disj  13691  fzouzdisj  13743  cotr2g  15039  limsupgle  15554  ello12  15593  elo12  15604  lo1resb  15641  rlimresb  15642  o1resb  15643  lo1eq  15645  rlimeq  15646  fsumsplit  15817  sumsplit  15844  fsum2dlem  15846  fprod2dlem  16059  bitsmod  16518  saddisjlem  16546  sadadd  16549  sadass  16553  smuval2  16564  smupval  16570  smueqlem  16572  smumul  16575  isprm7  16791  prmreclem5  17004  prmrec  17006  4sqlem12  17040  vdwmc  17062  setsstruct2  17258  acsfn  17739  iszeroo  18079  iszeroi  18090  fpwipodrs  18620  psss  18660  insubm  18916  subgacs  19273  nsgacs  19274  resscntz  19449  gsmsymgreq  19548  sylow2a  19735  lsmmod  19791  lsmdisj2  19798  gsumzsplit  20043  subgdmdprd  20152  dprdcntz2  20156  dprddisj2  20157  pgpfac1lem3  20195  rnghmval2  20574  isrhm  20609  subsubrng2  20715  subsubrg2  20750  rnghmsubcsetclem1  20782  funcrngcsetcALT  20792  zrinitorngc  20793  zrtermorngc  20794  rhmsubcsetclem1  20811  rhmsubcrngclem1  20817  ringcbasbas  20824  zrtermoringc  20826  srhmsubclem1  20828  fldhmsubc  20940  acsfn1p  20954  subrgacs  20955  sdrgacs  20956  isorng  21016  lssacs  21140  lspdisj  21301  lspdisjb  21302  prmidl0  21530  dfprm2  21675  irinitoringc  21681  ocvin  21876  unocv  21882  iunocv  21883  obselocv  21930  isassa  22058  aspid  22076  aspval2  22100  pmatcoe1fsupp  22910  isbasis2g  23157  tgval2  23165  tgcl  23178  ppttop  23216  epttop  23218  ssntr  23267  ntreq0  23286  isclo  23296  restntr  23391  restlp  23392  cnpresti  23497  cnprest  23498  cnprest2  23499  lmss  23507  haust1  23561  nrmsep3  23564  isnrm2  23567  lmmo  23589  fincmp  23602  cmpsublem  23608  cmpsub  23609  uncmp  23612  hauscmplem  23615  dfconn2  23628  iunconnlem  23636  unconn  23638  is1stc2  23651  1stcrest  23662  1stcelcls  23671  llyi  23684  nllyi  23685  subislly  23691  lly1stc  23706  txcnp  23830  txcnmpt  23834  hausdiag  23855  kqcldsat  23943  isfbas2  24045  isfil2  24066  fbasfip  24078  elfg  24081  filconn  24093  rnelfmlem  24162  rnelfm  24163  fmfnfmlem2  24165  fmfnfmlem4  24167  fmfnfm  24168  flimrest  24193  hauspwpwf1  24197  fclsrest  24234  alexsubALTlem2  24258  alexsubALTlem3  24259  alexsubALTlem4  24260  alexsubALT  24261  istmd  24284  istgp  24287  tsmssubm  24353  tsmssplit  24362  istrg  24374  istdrg  24376  istlm  24395  ustfilxp  24423  utoptop  24444  utop3cls  24461  bldisj  24608  blin  24631  blres  24641  lpbl  24713  metrest  24734  restmetu  24780  isngp  24806  isnlm  24885  isnmhm  24956  xrtgioo  25017  xrsmopn  25023  icccmplem2  25034  reconnlem2  25038  icoopnst  25151  iocopnst  25152  bndth  25170  zclmncvs  25360  isncvsngp  25361  ncvsprp  25364  ncvsm1  25366  ncvsdif  25367  ncvspi  25368  ncvs1  25369  ncvspds  25373  iscph  25382  tcphcph  25449  cfilfcls  25486  cmetcaulem  25500  isbn  25550  cldcss2  25654  hlhil  25655  ovolfcl  25678  ovolicc2lem2  25730  ovolicc2  25734  shftmbl  25750  volfiniun  25759  mbfmax  25861  mbfimaopnlem  25867  mbfaddlem  25872  i1faddlem  25905  i1fmullem  25906  i1fres  25917  itg1climres  25926  mbfi1fseqlem4  25930  itg2splitlem  25960  itg2split  25961  itgresr  25991  ellimc2  26089  ellimc3  26091  limcun  26107  dvreslem  26121  dvne0  26223  itgsubstlem  26260  ig1pval3  26388  aaliou2  26556  aaliou2b  26557  pilem1  26667  rlimcnp2  27184  fsumharmonic  27229  ppisval2  27322  prmorcht  27395  fsumvma2  27431  pclogsum  27432  vmasum  27433  chpchtsum  27436  chpub  27437  rpvmasum2  27729  madeval2  28079  tglineineq  28969  trlsegvdeg  30651  frgrncvvdeqlem7  30729  frgrncvvdeqlem9  30731  minvecolem1  31299  minvecolem4a  31302  minvecolem4b  31303  minvecolem4  31305  h2hcau  31404  axhcompl-zf  31423  hhcmpl  31625  hhcms  31628  ocin  31721  ocnel  31723  shmodsi  31814  pjhthlem2  31817  omlsilem  31827  pjoc1i  31856  spansnm0i  32075  nonbooli  32076  5oalem7  32085  3oalem3  32089  pjssmii  32106  mayete3i  32153  nmcopex  32454  nmcoplb  32455  lncnopbd  32462  nmcfnex  32478  nmcfnlb  32479  riesz4  32489  riesz1  32490  riesz2  32491  cnlnadjlem3  32494  cnlnadjlem5  32496  cnlnadjlem9  32500  cnlnadjeu  32503  rnbra  32532  pjimai  32601  pjclem4a  32623  pj3lem1  32631  jpi  32695  sumdmdii  32840  sumdmdlem  32843  sumdmdlem2  32844  cdjreui  32857  cdj3lem1  32859  iunin1f  32975  disjorf  32997  ofpreima  33083  1stpreima  33125  2ndpreima  33126  iocinioc2  33196  ssnnssfz  33204  cntzun  33465  kerunit  33711  ressply1mon1p  33924  ccfldextdgrr  34128  crefdf  34304  cmpcref  34306  cmppcmp  34314  cnre2csqima  34367  ordtconnlem1  34380  lmxrge0  34408  isrrext  34456  esum0  34505  esumcst  34519  esumpcvgval  34534  esumcvg  34542  measvuni  34671  eulerpartlemt0  34826  eulerpartlemr  34831  eulerpartlemgf  34836  eulerpartlemgs2  34837  eulerpartlemn  34838  fiblem  34855  oddprm2  35109  bnj1173  35457  bnj1174  35458  bnj1279  35473  elima4  36307  dfon2lem4  36315  ellimits  36439  dfom5b  36441  brapply  36467  brcap  36469  dfrecs2  36481  dfrdg4  36482  finminlem  36888  neibastop2lem  36930  neibastop2  36931  neifg  36941  tailfb  36947  onsucconni  37007  onintopssconn  37010  onsucsuccmpi  37013  limsucncmpi  37015  onint1  37019  mh-infprim2bi  37117  bj-inex1gALT  37619  bj-inrab  37622  bj-rcleqf  37720  bj-restuni  37798  bj-opelresdm  37848  bj-idres  37863  bj-opelidres  37864  bj-eldiag  37879  bj-eldiag2  37880  bj-ccinftydisj  37916  taupilem3  38022  isbasisrelowllem1  38060  isbasisrelowllem2  38061  nlpineqsn  38113  fvineqsneu  38116  ptrest  38329  poimirlem29  38359  poimirlem30  38360  mblfinlem2  38368  mbfposadd  38377  itg2gt0cn  38385  dvasin  38414  inixp  38439  0totbnd  38484  sstotbnd3  38487  heibor1lem  38520  heibor1  38521  heiborlem6  38527  isexid2  38566  smgrpismgmOLD  38573  issmgrpOLD  38574  mndoissmgrpOLD  38579  ismndo  38583  exidresid  38590  rngo1cl  38650  isfld2  38716  ineleq  39063  refressn  39242  eleccossin  39282  elrefsymrelsrel  39364  dfeldisj3  39520  eldisjdmqsim  39526  disjlem14  39610  prtlem14  39708  lshpdisj  39821  lkrin  39998  ishlat1  40186  pmodlem2  40681  pclfinN  40734  pclcmpatN  40735  osumcllem4N  40793  pexmidlem1N  40804  dihmeetlem1N  42124  dihglblem5apreN  42125  dihmeetlem4preN  42140  dihmeetlem13N  42153  dochnel2  42226  lcdlss  42453  mapd1o  42482  baerlem3lem2  42544  baerlem5alem2  42545  baerlem5blem2  42546  redvmptabs  43181  cmpfiiin  43488  mrefg2  43498  fz1eqin  43560  fnwe2lem2  43838  islmodfg  43856  islssfg2  43858  lnr2i  43903  rp-fakeinunass  44301  fiinfi  44359  elinintab  44361  elinintrab  44363  elinlem  44384  cnvcnvintabd  44386  ntrneikb  44880  ntrneik3  44882  ntrneik13  44884  ismnushort  45071  radcnvrat  45084  nzin  45088  onfrALTlem2  45315  onfrALTlem2VD  45657  relpmin  45721  pwclaxpow  45753  dfac5prim  45759  modelac8prim  45761  permac8prim  45783  iooabslt  46275  iccintsng  46299  lptioo2cn  46419  lptioo1cn  46420  cncfuni  46660  icccncfext  46661  stoweidlem44  46818  fourierdlem42  46923  fourierdlem80  46960  sge00  47150  eldmressn  47834  afvres  47969  afv2res  48036  prproropf1olem0  48311  31prm  48409  indprmfz  48442  rngccatidALTV  49096  rhmsubcALTVlem3  49107  funcringcsetcALTV2lem7  49120  ringccatidALTV  49130  ringcbasbasALTV  49136  funcringcsetclem7ALTV  49143  fldhmsubcALTV  49157  dfidom2  49167  ssnn0ssfz  49188  elbigo2  49391  itsclinecirc0in  49614  resinsnALT  49710  opndisj  49740  clddisj  49741  i0oii  49757  io1ii  49758