Theorem elin 3933

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3450   ∩ cin 3916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-in 3924

This theorem is referenced by:  elini  4165  elind  4166  elinel1  4167  elinel2  4168  elin2  4169  elin3  4172  ineqri  4178  nfin  4190  inass  4194  ssin  4205  ssrin  4208  ralin  4215  rexin  4216  dfss4  4235  difin  4238  indi  4250  undi  4251  unineq  4254  indifdi  4260  difin2  4267  inrab2  4283  ndisj  4336  inn0f  4337  difin0ss  4339  inssdif0  4340  inelcm  4431  inundif  4445  elinsn  4677  uniin  4898  intun  4947  intprg  4948  elrint  4956  iunin2  5038  iinin2  5045  elriin  5048  disjor  5092  disjiun  5098  brin  5162  trin  5229  inex1  5275  inuni  5308  wefrc  5635  inopab  5795  inxp  5798  inxpOLD  5799  dmin  5878  dfres3  5958  intasym  6091  asymref  6092  dminss  6129  imainss  6130  inimasn  6132  cnvresima  6206  dfco2a  6222  ordtri3or  6367  2elresin  6642  respreima  7041  fvcofneq  7068  tpres  7178  isomin  7315  isoini  7316  offval  7665  ordpwsuc  7793  frpoins3xpg  8122  frpoins3xp3g  8123  xpord3pred  8134  ressuppss  8165  frrlem13  8280  fprlem1  8282  uniinqs  8773  mapval2  8848  ixpin  8899  boxriin  8916  disjen  9104  ssenen  9121  onfin2  9186  elfpw  9312  fiin  9380  inf3lem2  9589  epfrs  9691  cp  9851  dfac5lem1  10083  dfac5lem5  10087  dfac5  10089  kmlem3  10113  kmlem14  10124  kmlem15  10125  fin23lem26  10285  pwxpndom2  10625  ingru  10775  gruina  10778  grur1  10780  axgroth4  10792  grothprim  10794  ixxdisj  13328  icodisj  13444  fzdisj  13519  nn0disj  13612  fzouzdisj  13663  cotr2g  14949  limsupgle  15450  ello12  15489  elo12  15500  lo1resb  15537  rlimresb  15538  o1resb  15539  lo1eq  15541  rlimeq  15542  fsumsplit  15714  sumsplit  15741  fsum2dlem  15743  fprod2dlem  15953  bitsmod  16413  saddisjlem  16441  sadadd  16444  sadass  16448  smuval2  16459  smupval  16465  smueqlem  16467  smumul  16470  isprm7  16685  prmreclem5  16898  prmrec  16900  4sqlem12  16934  vdwmc  16956  setsstruct2  17151  acsfn  17627  iszeroo  17967  iszeroi  17978  fpwipodrs  18506  psss  18546  insubm  18752  subgacs  19100  nsgacs  19101  resscntz  19272  gsmsymgreq  19369  sylow2a  19556  lsmmod  19612  lsmdisj2  19619  gsumzsplit  19864  subgdmdprd  19973  dprdcntz2  19977  dprddisj2  19978  pgpfac1lem3  20016  rnghmval2  20360  isrhm  20394  subsubrng2  20480  subsubrg2  20515  rnghmsubcsetclem1  20547  funcrngcsetcALT  20557  zrinitorngc  20558  zrtermorngc  20559  rhmsubcsetclem1  20576  rhmsubcrngclem1  20582  ringcbasbas  20589  zrtermoringc  20591  srhmsubclem1  20593  fldhmsubc  20701  acsfn1p  20715  subrgacs  20716  sdrgacs  20717  lssacs  20880  lspdisj  21042  lspdisjb  21043  dfprm2  21390  irinitoringc  21396  ocvin  21590  unocv  21596  iunocv  21597  obselocv  21644  isassa  21772  aspid  21791  aspval2  21814  pmatcoe1fsupp  22595  isbasis2g  22842  tgval2  22850  tgcl  22863  ppttop  22901  epttop  22903  ssntr  22952  ntreq0  22971  isclo  22981  restntr  23076  restlp  23077  cnpresti  23182  cnprest  23183  cnprest2  23184  lmss  23192  haust1  23246  nrmsep3  23249  isnrm2  23252  lmmo  23274  fincmp  23287  cmpsublem  23293  cmpsub  23294  uncmp  23297  hauscmplem  23300  dfconn2  23313  iunconnlem  23321  unconn  23323  is1stc2  23336  1stcrest  23347  1stcelcls  23355  llyi  23368  nllyi  23369  subislly  23375  lly1stc  23390  txcnp  23514  txcnmpt  23518  hausdiag  23539  kqcldsat  23627  isfbas2  23729  isfil2  23750  fbasfip  23762  elfg  23765  filconn  23777  rnelfmlem  23846  rnelfm  23847  fmfnfmlem2  23849  fmfnfmlem4  23851  fmfnfm  23852  flimrest  23877  hauspwpwf1  23881  fclsrest  23918  alexsubALTlem2  23942  alexsubALTlem3  23943  alexsubALTlem4  23944  alexsubALT  23945  istmd  23968  istgp  23971  tsmssubm  24037  tsmssplit  24046  istrg  24058  istdrg  24060  istlm  24079  ustfilxp  24107  utoptop  24129  utop3cls  24146  bldisj  24293  blin  24316  blres  24326  lpbl  24398  metrest  24419  restmetu  24465  isngp  24491  isnlm  24570  isnmhm  24641  xrtgioo  24702  xrsmopn  24708  icccmplem2  24719  reconnlem2  24723  icoopnst  24843  iocopnst  24844  bndth  24864  zclmncvs  25055  isncvsngp  25056  ncvsprp  25059  ncvsm1  25061  ncvsdif  25062  ncvspi  25063  ncvs1  25064  ncvspds  25068  iscph  25077  tcphcph  25144  cfilfcls  25181  cmetcaulem  25195  isbn  25245  cldcss2  25349  hlhil  25350  ovolfcl  25374  ovolicc2lem2  25426  ovolicc2  25430  shftmbl  25446  volfiniun  25455  mbfmax  25557  mbfimaopnlem  25563  mbfaddlem  25568  i1faddlem  25601  i1fmullem  25602  i1fres  25613  itg1climres  25622  mbfi1fseqlem4  25626  itg2splitlem  25656  itg2split  25657  itgresr  25687  ellimc2  25785  ellimc3  25787  limcun  25803  dvreslem  25817  dvne0  25923  itgsubstlem  25962  ig1pval3  26090  aaliou2  26255  aaliou2b  26256  pilem1  26368  rlimcnp2  26883  fsumharmonic  26929  ppisval2  27022  prmorcht  27095  fsumvma2  27132  pclogsum  27133  vmasum  27134  chpchtsum  27137  chpub  27138  rpvmasum2  27430  madeval2  27768  tglineineq  28577  trlsegvdeg  30163  frgrncvvdeqlem7  30241  frgrncvvdeqlem9  30243  minvecolem1  30810  minvecolem4a  30813  minvecolem4b  30814  minvecolem4  30816  h2hcau  30915  axhcompl-zf  30934  hhcmpl  31136  hhcms  31139  ocin  31232  ocnel  31234  shmodsi  31325  pjhthlem2  31328  omlsilem  31338  pjoc1i  31367  spansnm0i  31586  nonbooli  31587  5oalem7  31596  3oalem3  31600  pjssmii  31617  mayete3i  31664  nmcopex  31965  nmcoplb  31966  lncnopbd  31973  nmcfnex  31989  nmcfnlb  31990  riesz4  32000  riesz1  32001  riesz2  32002  cnlnadjlem3  32005  cnlnadjlem5  32007  cnlnadjlem9  32011  cnlnadjeu  32014  rnbra  32043  pjimai  32112  pjclem4a  32134  pj3lem1  32142  jpi  32206  sumdmdii  32351  sumdmdlem  32354  sumdmdlem2  32355  cdjreui  32368  cdj3lem1  32370  iunin1f  32493  disjorf  32515  ofpreima  32596  1stpreima  32637  2ndpreima  32638  iocinioc2  32709  ssnnssfz  32717  cntzun  33015  isorng  33284  kerunit  33304  prmidl0  33428  ressply1mon1p  33544  ccfldextdgrr  33674  crefdf  33845  cmpcref  33847  cmppcmp  33855  cnre2csqima  33908  ordtconnlem1  33921  lmxrge0  33949  isrrext  33997  esum0  34046  esumcst  34060  esumpcvgval  34075  esumcvg  34083  measvuni  34211  eulerpartlemt0  34367  eulerpartlemr  34372  eulerpartlemgf  34377  eulerpartlemgs2  34378  eulerpartlemn  34379  fiblem  34396  oddprm2  34653  bnj1173  34999  bnj1174  35000  bnj1279  35015  elima4  35770  dfon2lem4  35781  ellimits  35905  dfom5b  35907  brapply  35933  brcap  35935  dfrecs2  35945  dfrdg4  35946  finminlem  36313  neibastop2lem  36355  neibastop2  36356  neifg  36366  tailfb  36372  onsucconni  36432  onintopssconn  36435  onsucsuccmpi  36438  limsucncmpi  36440  onint1  36444  bj-inrab  36922  bj-rcleqf  37020  bj-restuni  37092  bj-opelresdm  37140  bj-idres  37155  bj-opelidres  37156  bj-eldiag  37171  bj-eldiag2  37172  bj-ccinftydisj  37208  taupilem3  37314  isbasisrelowllem1  37350  isbasisrelowllem2  37351  nlpineqsn  37403  fvineqsneu  37406  ptrest  37620  poimirlem29  37650  poimirlem30  37651  mblfinlem2  37659  mbfposadd  37668  itg2gt0cn  37676  dvasin  37705  inixp  37729  0totbnd  37774  sstotbnd3  37777  heibor1lem  37810  heibor1  37811  heiborlem6  37817  isexid2  37856  smgrpismgmOLD  37863  issmgrpOLD  37864  mndoissmgrpOLD  37869  ismndo  37873  exidresid  37880  rngo1cl  37940  isfld2  38006  ineleq  38343  refressn  38441  eleccossin  38481  elrefsymrelsrel  38569  dfeldisj3  38718  disjlem14  38797  prtlem14  38874  lshpdisj  38987  lkrin  39164  ishlat1  39352  pmodlem2  39848  pclfinN  39901  pclcmpatN  39902  osumcllem4N  39960  pexmidlem1N  39971  dihmeetlem1N  41291  dihglblem5apreN  41292  dihmeetlem4preN  41307  dihmeetlem13N  41320  dochnel2  41393  lcdlss  41620  mapd1o  41649  baerlem3lem2  41711  baerlem5alem2  41712  baerlem5blem2  41713  redvmptabs  42355  cmpfiiin  42692  mrefg2  42702  fz1eqin  42764  fnwe2lem2  43047  islmodfg  43065  islssfg2  43067  lnr2i  43112  rp-fakeinunass  43511  fiinfi  43569  elinintab  43571  elinintrab  43573  elinlem  43594  cnvcnvintabd  43596  ntrneikb  44090  ntrneik3  44092  ntrneik13  44094  ismnushort  44297  radcnvrat  44310  nzin  44314  onfrALTlem2  44543  onfrALTlem2VD  44885  relpmin  44949  pwclaxpow  44981  dfac5prim  44987  modelac8prim  44989  permac8prim  45011  iooabslt  45504  iccintsng  45528  lptioo2cn  45650  lptioo1cn  45651  cncfuni  45891  icccncfext  45892  stoweidlem44  46049  fourierdlem42  46154  fourierdlem80  46191  sge00  46381  eldmressn  47042  afvres  47177  afv2res  47244  prproropf1olem0  47507  31prm  47602  rngccatidALTV  48264  rhmsubcALTVlem3  48275  funcringcsetcALTV2lem7  48288  ringccatidALTV  48298  ringcbasbasALTV  48304  funcringcsetclem7ALTV  48311  fldhmsubcALTV  48325  ssnn0ssfz  48341  elbigo2  48545  itsclinecirc0in  48768  resinsnALT  48865  opndisj  48895  clddisj  48896  i0oii  48912  io1ii  48913