Theorem elin 3905

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 3450	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 3450	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	adantl 481	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2824	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2824	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	4, 5	anbi12d 633	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
7		df-in 3896	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 3623	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 378	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3429   ∩ cin 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-in 3896

This theorem is referenced by:  elini  4139  elind  4140  elinel1  4141  elinel2  4142  elin2  4143  elin3  4146  ineqri  4152  nfin  4164  inass  4168  ssin  4179  ssrin  4182  ralin  4189  rexin  4190  dfss4  4209  difin  4212  indi  4224  undi  4225  unineq  4228  indifdi  4234  difin2  4241  inrab2  4257  ndisj  4310  inn0f  4311  difin0ss  4313  inssdif0  4314  inelcm  4405  inundif  4419  elinsn  4654  uniin  4874  intun  4922  intprg  4923  elrint  4931  iunin2  5013  iinin2  5020  elriin  5023  disjor  5067  disjiun  5073  brin  5137  trin  5204  inex1  5258  inuni  5291  wefrc  5625  inopab  5785  inxp  5787  dmin  5866  dfres3  5949  intasym  6078  asymref  6079  dminss  6117  imainss  6118  inimasn  6120  cnvresima  6194  dfco2a  6210  ordtri3or  6355  2elresin  6619  respreima  7018  fvcofneq  7045  tpres  7156  isomin  7292  isoini  7293  offval  7640  ordpwsuc  7766  frpoins3xpg  8090  frpoins3xp3g  8091  xpord3pred  8102  ressuppss  8133  frrlem13  8248  fprlem1  8250  uniinqs  8744  mapval2  8820  ixpin  8871  boxriin  8888  disjen  9072  ssenen  9089  onfin2  9151  elfpw  9264  fiin  9335  inf3lem2  9550  epfrs  9652  cp  9815  dfac5lem1  10045  dfac5lem5  10049  dfac5  10051  kmlem3  10075  kmlem14  10086  kmlem15  10087  fin23lem26  10247  pwxpndom2  10588  ingru  10738  gruina  10741  grur1  10743  axgroth4  10755  grothprim  10757  ixxdisj  13313  icodisj  13429  fzdisj  13505  nn0disj  13598  fzouzdisj  13650  cotr2g  14938  limsupgle  15439  ello12  15478  elo12  15489  lo1resb  15526  rlimresb  15527  o1resb  15528  lo1eq  15530  rlimeq  15531  fsumsplit  15703  sumsplit  15730  fsum2dlem  15732  fprod2dlem  15945  bitsmod  16405  saddisjlem  16433  sadadd  16436  sadass  16440  smuval2  16451  smupval  16457  smueqlem  16459  smumul  16462  isprm7  16678  prmreclem5  16891  prmrec  16893  4sqlem12  16927  vdwmc  16949  setsstruct2  17144  acsfn  17625  iszeroo  17965  iszeroi  17976  fpwipodrs  18506  psss  18546  insubm  18786  subgacs  19136  nsgacs  19137  resscntz  19308  gsmsymgreq  19407  sylow2a  19594  lsmmod  19650  lsmdisj2  19657  gsumzsplit  19902  subgdmdprd  20011  dprdcntz2  20015  dprddisj2  20016  pgpfac1lem3  20054  rnghmval2  20424  isrhm  20458  subsubrng2  20541  subsubrg2  20576  rnghmsubcsetclem1  20608  funcrngcsetcALT  20618  zrinitorngc  20619  zrtermorngc  20620  rhmsubcsetclem1  20637  rhmsubcrngclem1  20643  ringcbasbas  20650  zrtermoringc  20652  srhmsubclem1  20654  fldhmsubc  20762  acsfn1p  20776  subrgacs  20777  sdrgacs  20778  isorng  20838  lssacs  20962  lspdisj  21123  lspdisjb  21124  dfprm2  21453  irinitoringc  21459  ocvin  21654  unocv  21660  iunocv  21661  obselocv  21708  isassa  21836  aspid  21854  aspval2  21878  pmatcoe1fsupp  22666  isbasis2g  22913  tgval2  22921  tgcl  22934  ppttop  22972  epttop  22974  ssntr  23023  ntreq0  23042  isclo  23052  restntr  23147  restlp  23148  cnpresti  23253  cnprest  23254  cnprest2  23255  lmss  23263  haust1  23317  nrmsep3  23320  isnrm2  23323  lmmo  23345  fincmp  23358  cmpsublem  23364  cmpsub  23365  uncmp  23368  hauscmplem  23371  dfconn2  23384  iunconnlem  23392  unconn  23394  is1stc2  23407  1stcrest  23418  1stcelcls  23426  llyi  23439  nllyi  23440  subislly  23446  lly1stc  23461  txcnp  23585  txcnmpt  23589  hausdiag  23610  kqcldsat  23698  isfbas2  23800  isfil2  23821  fbasfip  23833  elfg  23836  filconn  23848  rnelfmlem  23917  rnelfm  23918  fmfnfmlem2  23920  fmfnfmlem4  23922  fmfnfm  23923  flimrest  23948  hauspwpwf1  23952  fclsrest  23989  alexsubALTlem2  24013  alexsubALTlem3  24014  alexsubALTlem4  24015  alexsubALT  24016  istmd  24039  istgp  24042  tsmssubm  24108  tsmssplit  24117  istrg  24129  istdrg  24131  istlm  24150  ustfilxp  24178  utoptop  24199  utop3cls  24216  bldisj  24363  blin  24386  blres  24396  lpbl  24468  metrest  24489  restmetu  24535  isngp  24561  isnlm  24640  isnmhm  24711  xrtgioo  24772  xrsmopn  24778  icccmplem2  24789  reconnlem2  24793  icoopnst  24906  iocopnst  24907  bndth  24925  zclmncvs  25115  isncvsngp  25116  ncvsprp  25119  ncvsm1  25121  ncvsdif  25122  ncvspi  25123  ncvs1  25124  ncvspds  25128  iscph  25137  tcphcph  25204  cfilfcls  25241  cmetcaulem  25255  isbn  25305  cldcss2  25409  hlhil  25410  ovolfcl  25433  ovolicc2lem2  25485  ovolicc2  25489  shftmbl  25505  volfiniun  25514  mbfmax  25616  mbfimaopnlem  25622  mbfaddlem  25627  i1faddlem  25660  i1fmullem  25661  i1fres  25672  itg1climres  25681  mbfi1fseqlem4  25685  itg2splitlem  25715  itg2split  25716  itgresr  25746  ellimc2  25844  ellimc3  25846  limcun  25862  dvreslem  25876  dvne0  25978  itgsubstlem  26015  ig1pval3  26143  aaliou2  26306  aaliou2b  26307  pilem1  26416  rlimcnp2  26930  fsumharmonic  26975  ppisval2  27068  prmorcht  27141  fsumvma2  27177  pclogsum  27178  vmasum  27179  chpchtsum  27182  chpub  27183  rpvmasum2  27475  madeval2  27825  tglineineq  28711  trlsegvdeg  30297  frgrncvvdeqlem7  30375  frgrncvvdeqlem9  30377  minvecolem1  30945  minvecolem4a  30948  minvecolem4b  30949  minvecolem4  30951  h2hcau  31050  axhcompl-zf  31069  hhcmpl  31271  hhcms  31274  ocin  31367  ocnel  31369  shmodsi  31460  pjhthlem2  31463  omlsilem  31473  pjoc1i  31502  spansnm0i  31721  nonbooli  31722  5oalem7  31731  3oalem3  31735  pjssmii  31752  mayete3i  31799  nmcopex  32100  nmcoplb  32101  lncnopbd  32108  nmcfnex  32124  nmcfnlb  32125  riesz4  32135  riesz1  32136  riesz2  32137  cnlnadjlem3  32140  cnlnadjlem5  32142  cnlnadjlem9  32146  cnlnadjeu  32149  rnbra  32178  pjimai  32247  pjclem4a  32269  pj3lem1  32277  jpi  32341  sumdmdii  32486  sumdmdlem  32489  sumdmdlem2  32490  cdjreui  32503  cdj3lem1  32505  iunin1f  32627  disjorf  32649  ofpreima  32738  1stpreima  32780  2ndpreima  32781  iocinioc2  32852  ssnnssfz  32860  cntzun  33140  kerunit  33385  prmidl0  33510  ressply1mon1p  33628  ccfldextdgrr  33816  crefdf  33992  cmpcref  33994  cmppcmp  34002  cnre2csqima  34055  ordtconnlem1  34068  lmxrge0  34096  isrrext  34144  esum0  34193  esumcst  34207  esumpcvgval  34222  esumcvg  34230  measvuni  34358  eulerpartlemt0  34513  eulerpartlemr  34518  eulerpartlemgf  34523  eulerpartlemgs2  34524  eulerpartlemn  34525  fiblem  34542  oddprm2  34799  bnj1173  35144  bnj1174  35145  bnj1279  35160  elima4  35958  dfon2lem4  35966  ellimits  36090  dfom5b  36092  brapply  36118  brcap  36120  dfrecs2  36132  dfrdg4  36133  finminlem  36500  neibastop2lem  36542  neibastop2  36543  neifg  36553  tailfb  36559  onsucconni  36619  onintopssconn  36622  onsucsuccmpi  36625  limsucncmpi  36627  onint1  36631  mh-infprim2bi  36729  bj-inrab  37234  bj-rcleqf  37332  bj-restuni  37409  bj-opelresdm  37459  bj-idres  37474  bj-opelidres  37475  bj-eldiag  37490  bj-eldiag2  37491  bj-ccinftydisj  37527  taupilem3  37633  isbasisrelowllem1  37671  isbasisrelowllem2  37672  nlpineqsn  37724  fvineqsneu  37727  ptrest  37940  poimirlem29  37970  poimirlem30  37971  mblfinlem2  37979  mbfposadd  37988  itg2gt0cn  37996  dvasin  38025  inixp  38049  0totbnd  38094  sstotbnd3  38097  heibor1lem  38130  heibor1  38131  heiborlem6  38137  isexid2  38176  smgrpismgmOLD  38183  issmgrpOLD  38184  mndoissmgrpOLD  38189  ismndo  38193  exidresid  38200  rngo1cl  38260  isfld2  38326  ineleq  38675  refressn  38854  eleccossin  38894  elrefsymrelsrel  38976  dfeldisj3  39132  eldisjdmqsim  39138  disjlem14  39222  prtlem14  39320  lshpdisj  39433  lkrin  39610  ishlat1  39798  pmodlem2  40293  pclfinN  40346  pclcmpatN  40347  osumcllem4N  40405  pexmidlem1N  40416  dihmeetlem1N  41736  dihglblem5apreN  41737  dihmeetlem4preN  41752  dihmeetlem13N  41765  dochnel2  41838  lcdlss  42065  mapd1o  42094  baerlem3lem2  42156  baerlem5alem2  42157  baerlem5blem2  42158  redvmptabs  42792  cmpfiiin  43129  mrefg2  43139  fz1eqin  43201  fnwe2lem2  43479  islmodfg  43497  islssfg2  43499  lnr2i  43544  rp-fakeinunass  43942  fiinfi  44000  elinintab  44002  elinintrab  44004  elinlem  44025  cnvcnvintabd  44027  ntrneikb  44521  ntrneik3  44523  ntrneik13  44525  ismnushort  44728  radcnvrat  44741  nzin  44745  onfrALTlem2  44973  onfrALTlem2VD  45315  relpmin  45379  pwclaxpow  45411  dfac5prim  45417  modelac8prim  45419  permac8prim  45441  iooabslt  45929  iccintsng  45953  lptioo2cn  46073  lptioo1cn  46074  cncfuni  46314  icccncfext  46315  stoweidlem44  46472  fourierdlem42  46577  fourierdlem80  46614  sge00  46804  eldmressn  47485  afvres  47620  afv2res  47687  prproropf1olem0  47962  31prm  48060  indprmfz  48093  rngccatidALTV  48748  rhmsubcALTVlem3  48759  funcringcsetcALTV2lem7  48772  ringccatidALTV  48782  ringcbasbasALTV  48788  funcringcsetclem7ALTV  48795  fldhmsubcALTV  48809  ssnn0ssfz  48825  elbigo2  49028  itsclinecirc0in  49251  resinsnALT  49348  opndisj  49378  clddisj  49379  i0oii  49395  io1ii  49396