Theorem elin 3899

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 3440	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 3440	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	adantl 481	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2826	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2826	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	4, 5	anbi12d 630	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
7		df-in 3890	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 3604	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 379	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108  Vcvv 3422   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890

This theorem is referenced by:  dfss2  3903  elini  4123  elind  4124  elinel1  4125  elinel2  4126  elin2  4127  elin3  4130  incomOLD  4132  ineqri  4135  inass  4150  ssin  4161  ssrin  4164  rexin  4170  dfss4  4189  difin  4192  indi  4204  undi  4205  unineq  4208  indifdi  4214  indifdirOLD  4216  difin2  4222  inrab2  4238  ndisj  4298  difin0ss  4299  inssdif0  4300  inelcm  4395  inundif  4409  elinsn  4643  uniin  4862  intun  4908  intprg  4909  intprOLD  4911  elrint  4919  iunin2  4996  iinin2  5003  elriin  5006  disjor  5050  disjiun  5057  brin  5122  trin  5197  inex1  5236  inuni  5262  wefrc  5574  inopab  5728  inxp  5730  dmin  5809  dfres3  5885  intasym  6009  asymref  6010  dminss  6045  imainss  6046  inimasn  6048  cnvresima  6122  dfco2a  6139  ordtri3or  6283  2elresin  6537  respreima  6925  fvcofneq  6951  tpres  7058  isomin  7188  isoini  7189  offval  7520  ordpwsuc  7637  ressuppss  7970  frrlem13  8085  fprlem1  8087  wfrlem5OLD  8115  uniinqs  8544  mapval2  8618  ixpin  8669  boxriin  8686  disjen  8870  ssenen  8887  onfin2  8945  elfpw  9051  fiin  9111  inf3lem2  9317  epfrs  9420  cp  9580  dfac5lem1  9810  dfac5lem5  9814  dfac5  9815  kmlem3  9839  kmlem14  9850  kmlem15  9851  fin23lem26  10012  pwxpndom2  10352  ingru  10502  gruina  10505  grur1  10507  axgroth4  10519  grothprim  10521  ixxdisj  13023  icodisj  13137  fzdisj  13212  nn0disj  13301  fzouzdisj  13351  cotr2g  14615  limsupgle  15114  ello12  15153  elo12  15164  lo1resb  15201  rlimresb  15202  o1resb  15203  lo1eq  15205  rlimeq  15206  fsumsplit  15381  sumsplit  15408  fsum2dlem  15410  fprod2dlem  15618  bitsmod  16071  saddisjlem  16099  sadadd  16102  sadass  16106  smuval2  16117  smupval  16123  smueqlem  16125  smumul  16128  isprm7  16341  prmreclem5  16549  prmrec  16551  4sqlem12  16585  vdwmc  16607  setsstruct2  16803  acsfn  17285  iszeroo  17629  iszeroi  17640  fpwipodrs  18173  psss  18213  insubm  18372  subgacs  18704  nsgacs  18705  resscntz  18853  gsmsymgreq  18955  sylow2a  19139  lsmmod  19196  lsmdisj2  19203  gsumzsplit  19443  subgdmdprd  19552  dprdcntz2  19556  dprddisj2  19557  pgpfac1lem3  19595  isrhm  19880  subsubrg2  19966  acsfn1p  19982  subrgacs  19983  sdrgacs  19984  lssacs  20144  lspdisj  20302  lspdisjb  20303  dfprm2  20607  ocvin  20791  unocv  20797  iunocv  20798  obselocv  20845  isassa  20973  aspid  20989  aspval2  21012  pmatcoe1fsupp  21758  isbasis2g  22006  tgval2  22014  tgcl  22027  ppttop  22065  epttop  22067  ssntr  22117  ntreq0  22136  isclo  22146  restntr  22241  restlp  22242  cnpresti  22347  cnprest  22348  cnprest2  22349  lmss  22357  haust1  22411  nrmsep3  22414  isnrm2  22417  lmmo  22439  fincmp  22452  cmpsublem  22458  cmpsub  22459  uncmp  22462  hauscmplem  22465  dfconn2  22478  iunconnlem  22486  unconn  22488  is1stc2  22501  1stcrest  22512  1stcelcls  22520  llyi  22533  nllyi  22534  subislly  22540  lly1stc  22555  txcnp  22679  txcnmpt  22683  hausdiag  22704  kqcldsat  22792  isfbas2  22894  isfil2  22915  fbasfip  22927  elfg  22930  filconn  22942  rnelfmlem  23011  rnelfm  23012  fmfnfmlem2  23014  fmfnfmlem4  23016  fmfnfm  23017  flimrest  23042  hauspwpwf1  23046  fclsrest  23083  alexsubALTlem2  23107  alexsubALTlem3  23108  alexsubALTlem4  23109  alexsubALT  23110  istmd  23133  istgp  23136  tsmssubm  23202  tsmssplit  23211  istrg  23223  istdrg  23225  istlm  23244  ustfilxp  23272  utoptop  23294  utop3cls  23311  bldisj  23459  blin  23482  blres  23492  lpbl  23565  metrest  23586  restmetu  23632  isngp  23658  isnlm  23745  isnmhm  23816  xrtgioo  23875  xrsmopn  23881  icccmplem2  23892  reconnlem2  23896  icoopnst  24008  iocopnst  24009  bndth  24027  zclmncvs  24217  isncvsngp  24218  ncvsprp  24221  ncvsm1  24223  ncvsdif  24224  ncvspi  24225  ncvs1  24226  ncvspds  24230  iscph  24239  tcphcph  24306  cfilfcls  24343  cmetcaulem  24357  isbn  24407  cldcss2  24511  hlhil  24512  ovolfcl  24535  ovolicc2lem2  24587  ovolicc2  24591  shftmbl  24607  volfiniun  24616  mbfmax  24718  mbfimaopnlem  24724  mbfaddlem  24729  i1faddlem  24762  i1fmullem  24763  i1fres  24775  itg1climres  24784  mbfi1fseqlem4  24788  itg2splitlem  24818  itg2split  24819  itgresr  24848  ellimc2  24946  ellimc3  24948  limcun  24964  dvreslem  24978  dvne0  25080  itgsubstlem  25117  ig1pval3  25244  aaliou2  25405  aaliou2b  25406  pilem1  25515  rlimcnp2  26021  fsumharmonic  26066  ppisval2  26159  prmorcht  26232  fsumvma2  26267  pclogsum  26268  vmasum  26269  chpchtsum  26272  chpub  26273  rpvmasum2  26565  tglineineq  26908  trlsegvdeg  28492  frgrncvvdeqlem7  28570  frgrncvvdeqlem9  28572  minvecolem1  29137  minvecolem4a  29140  minvecolem4b  29141  minvecolem4  29143  h2hcau  29242  axhcompl-zf  29261  hhcmpl  29463  hhcms  29466  ocin  29559  ocnel  29561  shmodsi  29652  pjhthlem2  29655  omlsilem  29665  pjoc1i  29694  spansnm0i  29913  nonbooli  29914  5oalem7  29923  3oalem3  29927  pjssmii  29944  mayete3i  29991  nmcopex  30292  nmcoplb  30293  lncnopbd  30300  nmcfnex  30316  nmcfnlb  30317  riesz4  30327  riesz1  30328  riesz2  30329  cnlnadjlem3  30332  cnlnadjlem5  30334  cnlnadjlem9  30338  cnlnadjeu  30341  rnbra  30370  pjimai  30439  pjclem4a  30461  pj3lem1  30469  jpi  30533  sumdmdii  30678  sumdmdlem  30681  sumdmdlem2  30682  cdjreui  30695  cdj3lem1  30697  iunin1f  30798  disjorf  30819  ofpreima  30904  1stpreima  30941  2ndpreima  30942  iocinioc2  31002  ssnnssfz  31010  cntzun  31222  isorng  31400  kerunit  31424  prmidl0  31528  ccfldextdgrr  31644  crefdf  31700  cmpcref  31702  cmppcmp  31710  cnre2csqima  31763  ordtconnlem1  31776  lmxrge0  31804  isrrext  31850  esum0  31917  esumcst  31931  esumpcvgval  31946  esumcvg  31954  measvuni  32082  eulerpartlemt0  32236  eulerpartlemr  32241  eulerpartlemgf  32246  eulerpartlemgs2  32247  eulerpartlemn  32248  fiblem  32265  oddprm2  32535  bnj521  32616  bnj1173  32882  bnj1174  32883  bnj1279  32898  elima4  33656  dfon2lem4  33668  frpoins3xpg  33714  frpoins3xp3g  33715  xpord3pred  33725  madeval2  33964  ellimits  34139  dfom5b  34141  brapply  34167  brcap  34169  dfrecs2  34179  dfrdg4  34180  finminlem  34434  neibastop2lem  34476  neibastop2  34477  neifg  34487  tailfb  34493  onsucconni  34553  onintopssconn  34556  onsucsuccmpi  34559  limsucncmpi  34561  onint1  34565  bj-inrab  35042  bj-rcleqf  35142  bj-restuni  35195  bj-opelresdm  35243  bj-idres  35258  bj-opelidres  35259  bj-eldiag  35274  bj-eldiag2  35275  bj-ccinftydisj  35311  taupilem3  35417  isbasisrelowllem1  35453  isbasisrelowllem2  35454  nlpineqsn  35506  fvineqsneu  35509  ptrest  35703  poimirlem29  35733  poimirlem30  35734  mblfinlem2  35742  mbfposadd  35751  itg2gt0cn  35759  dvasin  35788  inixp  35813  0totbnd  35858  sstotbnd3  35861  heibor1lem  35894  heibor1  35895  heiborlem6  35901  isexid2  35940  smgrpismgmOLD  35947  issmgrpOLD  35948  mndoissmgrpOLD  35953  ismndo  35957  exidresid  35964  rngo1cl  36024  isfld2  36090  ineleq  36413  eleccossin  36528  elrefsymrelsrel  36612  dfeldisj3  36757  prtlem14  36815  lshpdisj  36928  lkrin  37105  ishlat1  37293  pmodlem2  37788  pclfinN  37841  pclcmpatN  37842  osumcllem4N  37900  pexmidlem1N  37911  dihmeetlem1N  39231  dihglblem5apreN  39232  dihmeetlem4preN  39247  dihmeetlem13N  39260  dochnel2  39333  lcdlss  39560  mapd1o  39589  baerlem3lem2  39651  baerlem5alem2  39652  baerlem5blem2  39653  mhphf  40208  cmpfiiin  40435  mrefg2  40445  fz1eqin  40507  fnwe2lem2  40792  islmodfg  40810  islssfg2  40812  lnr2i  40857  rp-fakeinunass  41020  fiinfi  41069  elinintab  41072  elinintrab  41074  elinlem  41095  cnvcnvintabd  41097  ntrneikb  41593  ntrneik3  41595  ntrneik13  41597  ismnushort  41808  radcnvrat  41821  nzin  41825  onfrALTlem2  42055  onfrALTlem2VD  42398  inn0f  42510  iooabslt  42927  iccintsng  42951  lptioo2cn  43076  lptioo1cn  43077  cncfuni  43317  icccncfext  43318  stoweidlem44  43475  fourierdlem42  43580  fourierdlem80  43617  sge00  43804  eldmressn  44418  afvres  44551  afv2res  44618  prproropf1olem0  44842  31prm  44937  rnghmval2  45341  rnghmsubcsetclem1  45421  rngccatidALTV  45435  funcrngcsetcALT  45445  zrinitorngc  45446  zrtermorngc  45447  rhmsubcsetclem1  45467  rhmsubcrngclem1  45473  ringcbasbas  45480  funcringcsetcALTV2lem7  45488  ringccatidALTV  45498  ringcbasbasALTV  45504  funcringcsetclem7ALTV  45511  irinitoringc  45515  zrtermoringc  45516  srhmsubclem1  45519  fldhmsubc  45530  fldhmsubcALTV  45548  rhmsubcALTVlem3  45552  ssnn0ssfz  45573  elbigo2  45786  itsclinecirc0in  46009  opndisj  46084  clddisj  46085  i0oii  46101  io1ii  46102