Theorem elin 3906

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-in 3897

This theorem is referenced by:  elini  4140  elind  4141  elinel1  4142  elinel2  4143  elin2  4144  elin3  4147  ineqri  4153  nfin  4165  inass  4169  ssin  4180  ssrin  4183  ralin  4190  rexin  4191  dfss4  4210  difin  4213  indi  4225  undi  4226  unineq  4229  indifdi  4235  difin2  4242  inrab2  4258  ndisj  4311  inn0f  4312  difin0ss  4314  inssdif0  4315  inelcm  4406  inundif  4420  elinsn  4655  uniin  4875  intun  4923  intprg  4924  elrint  4932  iunin2  5014  iinin2  5021  elriin  5024  disjor  5068  disjiun  5074  brin  5138  trin  5205  inex1  5255  inuni  5288  wefrc  5619  inopab  5779  inxp  5781  inxpOLD  5782  dmin  5861  dfres3  5944  intasym  6073  asymref  6074  dminss  6112  imainss  6113  inimasn  6115  cnvresima  6189  dfco2a  6205  ordtri3or  6350  2elresin  6614  respreima  7013  fvcofneq  7040  tpres  7150  isomin  7286  isoini  7287  offval  7634  ordpwsuc  7760  frpoins3xpg  8084  frpoins3xp3g  8085  xpord3pred  8096  ressuppss  8127  frrlem13  8242  fprlem1  8244  uniinqs  8738  mapval2  8814  ixpin  8865  boxriin  8882  disjen  9066  ssenen  9083  onfin2  9145  elfpw  9258  fiin  9329  inf3lem2  9544  epfrs  9646  cp  9809  dfac5lem1  10039  dfac5lem5  10043  dfac5  10045  kmlem3  10069  kmlem14  10080  kmlem15  10081  fin23lem26  10241  pwxpndom2  10582  ingru  10732  gruina  10735  grur1  10737  axgroth4  10749  grothprim  10751  ixxdisj  13307  icodisj  13423  fzdisj  13499  nn0disj  13592  fzouzdisj  13644  cotr2g  14932  limsupgle  15433  ello12  15472  elo12  15483  lo1resb  15520  rlimresb  15521  o1resb  15522  lo1eq  15524  rlimeq  15525  fsumsplit  15697  sumsplit  15724  fsum2dlem  15726  fprod2dlem  15939  bitsmod  16399  saddisjlem  16427  sadadd  16430  sadass  16434  smuval2  16445  smupval  16451  smueqlem  16453  smumul  16456  isprm7  16672  prmreclem5  16885  prmrec  16887  4sqlem12  16921  vdwmc  16943  setsstruct2  17138  acsfn  17619  iszeroo  17959  iszeroi  17970  fpwipodrs  18500  psss  18540  insubm  18780  subgacs  19130  nsgacs  19131  resscntz  19302  gsmsymgreq  19401  sylow2a  19588  lsmmod  19644  lsmdisj2  19651  gsumzsplit  19896  subgdmdprd  20005  dprdcntz2  20009  dprddisj2  20010  pgpfac1lem3  20048  rnghmval2  20418  isrhm  20452  subsubrng2  20535  subsubrg2  20570  rnghmsubcsetclem1  20602  funcrngcsetcALT  20612  zrinitorngc  20613  zrtermorngc  20614  rhmsubcsetclem1  20631  rhmsubcrngclem1  20637  ringcbasbas  20644  zrtermoringc  20646  srhmsubclem1  20648  fldhmsubc  20756  acsfn1p  20770  subrgacs  20771  sdrgacs  20772  isorng  20832  lssacs  20956  lspdisj  21118  lspdisjb  21119  dfprm2  21466  irinitoringc  21472  ocvin  21667  unocv  21673  iunocv  21674  obselocv  21721  isassa  21849  aspid  21867  aspval2  21891  pmatcoe1fsupp  22679  isbasis2g  22926  tgval2  22934  tgcl  22947  ppttop  22985  epttop  22987  ssntr  23036  ntreq0  23055  isclo  23065  restntr  23160  restlp  23161  cnpresti  23266  cnprest  23267  cnprest2  23268  lmss  23276  haust1  23330  nrmsep3  23333  isnrm2  23336  lmmo  23358  fincmp  23371  cmpsublem  23377  cmpsub  23378  uncmp  23381  hauscmplem  23384  dfconn2  23397  iunconnlem  23405  unconn  23407  is1stc2  23420  1stcrest  23431  1stcelcls  23439  llyi  23452  nllyi  23453  subislly  23459  lly1stc  23474  txcnp  23598  txcnmpt  23602  hausdiag  23623  kqcldsat  23711  isfbas2  23813  isfil2  23834  fbasfip  23846  elfg  23849  filconn  23861  rnelfmlem  23930  rnelfm  23931  fmfnfmlem2  23933  fmfnfmlem4  23935  fmfnfm  23936  flimrest  23961  hauspwpwf1  23965  fclsrest  24002  alexsubALTlem2  24026  alexsubALTlem3  24027  alexsubALTlem4  24028  alexsubALT  24029  istmd  24052  istgp  24055  tsmssubm  24121  tsmssplit  24130  istrg  24142  istdrg  24144  istlm  24163  ustfilxp  24191  utoptop  24212  utop3cls  24229  bldisj  24376  blin  24399  blres  24409  lpbl  24481  metrest  24502  restmetu  24548  isngp  24574  isnlm  24653  isnmhm  24724  xrtgioo  24785  xrsmopn  24791  icccmplem2  24802  reconnlem2  24806  icoopnst  24919  iocopnst  24920  bndth  24938  zclmncvs  25128  isncvsngp  25129  ncvsprp  25132  ncvsm1  25134  ncvsdif  25135  ncvspi  25136  ncvs1  25137  ncvspds  25141  iscph  25150  tcphcph  25217  cfilfcls  25254  cmetcaulem  25268  isbn  25318  cldcss2  25422  hlhil  25423  ovolfcl  25446  ovolicc2lem2  25498  ovolicc2  25502  shftmbl  25518  volfiniun  25527  mbfmax  25629  mbfimaopnlem  25635  mbfaddlem  25640  i1faddlem  25673  i1fmullem  25674  i1fres  25685  itg1climres  25694  mbfi1fseqlem4  25698  itg2splitlem  25728  itg2split  25729  itgresr  25759  ellimc2  25857  ellimc3  25859  limcun  25875  dvreslem  25889  dvne0  25991  itgsubstlem  26028  ig1pval3  26156  aaliou2  26320  aaliou2b  26321  pilem1  26432  rlimcnp2  26946  fsumharmonic  26992  ppisval2  27085  prmorcht  27158  fsumvma2  27194  pclogsum  27195  vmasum  27196  chpchtsum  27199  chpub  27200  rpvmasum2  27492  madeval2  27842  tglineineq  28728  trlsegvdeg  30315  frgrncvvdeqlem7  30393  frgrncvvdeqlem9  30395  minvecolem1  30963  minvecolem4a  30966  minvecolem4b  30967  minvecolem4  30969  h2hcau  31068  axhcompl-zf  31087  hhcmpl  31289  hhcms  31292  ocin  31385  ocnel  31387  shmodsi  31478  pjhthlem2  31481  omlsilem  31491  pjoc1i  31520  spansnm0i  31739  nonbooli  31740  5oalem7  31749  3oalem3  31753  pjssmii  31770  mayete3i  31817  nmcopex  32118  nmcoplb  32119  lncnopbd  32126  nmcfnex  32142  nmcfnlb  32143  riesz4  32153  riesz1  32154  riesz2  32155  cnlnadjlem3  32158  cnlnadjlem5  32160  cnlnadjlem9  32164  cnlnadjeu  32167  rnbra  32196  pjimai  32265  pjclem4a  32287  pj3lem1  32295  jpi  32359  sumdmdii  32504  sumdmdlem  32507  sumdmdlem2  32508  cdjreui  32521  cdj3lem1  32523  iunin1f  32645  disjorf  32667  ofpreima  32756  1stpreima  32798  2ndpreima  32799  iocinioc2  32870  ssnnssfz  32878  cntzun  33158  kerunit  33403  prmidl0  33528  ressply1mon1p  33646  ccfldextdgrr  33835  crefdf  34011  cmpcref  34013  cmppcmp  34021  cnre2csqima  34074  ordtconnlem1  34087  lmxrge0  34115  isrrext  34163  esum0  34212  esumcst  34226  esumpcvgval  34241  esumcvg  34249  measvuni  34377  eulerpartlemt0  34532  eulerpartlemr  34537  eulerpartlemgf  34542  eulerpartlemgs2  34543  eulerpartlemn  34544  fiblem  34561  oddprm2  34818  bnj1173  35163  bnj1174  35164  bnj1279  35179  elima4  35977  dfon2lem4  35985  ellimits  36109  dfom5b  36111  brapply  36137  brcap  36139  dfrecs2  36151  dfrdg4  36152  finminlem  36519  neibastop2lem  36561  neibastop2  36562  neifg  36572  tailfb  36578  onsucconni  36638  onintopssconn  36641  onsucsuccmpi  36644  limsucncmpi  36646  onint1  36650  mh-infprim2bi  36748  bj-inrab  37253  bj-rcleqf  37351  bj-restuni  37428  bj-opelresdm  37478  bj-idres  37493  bj-opelidres  37494  bj-eldiag  37509  bj-eldiag2  37510  bj-ccinftydisj  37546  taupilem3  37652  isbasisrelowllem1  37688  isbasisrelowllem2  37689  nlpineqsn  37741  fvineqsneu  37744  ptrest  37957  poimirlem29  37987  poimirlem30  37988  mblfinlem2  37996  mbfposadd  38005  itg2gt0cn  38013  dvasin  38042  inixp  38066  0totbnd  38111  sstotbnd3  38114  heibor1lem  38147  heibor1  38148  heiborlem6  38154  isexid2  38193  smgrpismgmOLD  38200  issmgrpOLD  38201  mndoissmgrpOLD  38206  ismndo  38210  exidresid  38217  rngo1cl  38277  isfld2  38343  ineleq  38692  refressn  38871  eleccossin  38911  elrefsymrelsrel  38993  dfeldisj3  39149  eldisjdmqsim  39155  disjlem14  39239  prtlem14  39337  lshpdisj  39450  lkrin  39627  ishlat1  39815  pmodlem2  40310  pclfinN  40363  pclcmpatN  40364  osumcllem4N  40422  pexmidlem1N  40433  dihmeetlem1N  41753  dihglblem5apreN  41754  dihmeetlem4preN  41769  dihmeetlem13N  41782  dochnel2  41855  lcdlss  42082  mapd1o  42111  baerlem3lem2  42173  baerlem5alem2  42174  baerlem5blem2  42175  redvmptabs  42809  cmpfiiin  43146  mrefg2  43156  fz1eqin  43218  fnwe2lem2  43500  islmodfg  43518  islssfg2  43520  lnr2i  43565  rp-fakeinunass  43963  fiinfi  44021  elinintab  44023  elinintrab  44025  elinlem  44046  cnvcnvintabd  44048  ntrneikb  44542  ntrneik3  44544  ntrneik13  44546  ismnushort  44749  radcnvrat  44762  nzin  44766  onfrALTlem2  44994  onfrALTlem2VD  45336  relpmin  45400  pwclaxpow  45432  dfac5prim  45438  modelac8prim  45440  permac8prim  45462  iooabslt  45950  iccintsng  45974  lptioo2cn  46094  lptioo1cn  46095  cncfuni  46335  icccncfext  46336  stoweidlem44  46493  fourierdlem42  46598  fourierdlem80  46635  sge00  46825  eldmressn  47500  afvres  47635  afv2res  47702  prproropf1olem0  47977  31prm  48075  indprmfz  48108  rngccatidALTV  48763  rhmsubcALTVlem3  48774  funcringcsetcALTV2lem7  48787  ringccatidALTV  48797  ringcbasbasALTV  48803  funcringcsetclem7ALTV  48810  fldhmsubcALTV  48824  ssnn0ssfz  48840  elbigo2  49043  itsclinecirc0in  49266  resinsnALT  49363  opndisj  49393  clddisj  49394  i0oii  49410  io1ii  49411