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

Syntax hints:   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  Vcvv 3431   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-in 3890

This theorem is referenced by:  elini  4128  elind  4129  elinel1  4130  elinel2  4131  elin2  4132  elin3  4135  ineqri  4141  nfin  4153  inass  4156  ssin  4167  ssrin  4170  ralin  4177  rexin  4178  dfss4  4197  difin  4200  indi  4212  undi  4213  unineq  4216  indifdi  4222  difin2  4229  inrab2  4245  ndisj  4298  inn0f  4299  difin0ss  4301  inssdif0  4302  inelcm  4393  inundif  4407  elinsn  4642  uniin  4862  intun  4910  intprg  4911  elrint  4919  iunin2  5000  iinin2  5007  elriin  5010  disjor  5054  disjiun  5060  brin  5124  trin  5191  inex1  5245  inuni  5278  wefrc  5612  inopab  5772  inxp  5774  dmin  5853  dfres3  5936  intasym  6065  asymref  6066  dminss  6104  imainss  6105  inimasn  6107  cnvresima  6181  dfco2a  6197  ordtri3or  6342  2elresin  6606  respreima  7007  fvcofneq  7034  tpres  7145  isomin  7281  isoini  7282  offval  7629  ordpwsuc  7755  frpoins3xpg  8080  frpoins3xp3g  8081  xpord3pred  8092  ressuppss  8123  frrlem13  8238  fprlem1  8240  uniinqs  8734  mapval2  8810  ixpin  8861  boxriin  8878  disjen  9062  ssenen  9079  onfin2  9141  elfpw  9254  fiin  9325  inf3lem2  9541  epfrs  9643  cp  9806  dfac5lem1  10036  dfac5lem5  10040  dfac5  10042  kmlem3  10066  kmlem14  10077  kmlem15  10078  fin23lem26  10238  pwxpndom2  10579  ingru  10729  gruina  10732  grur1  10734  axgroth4  10746  grothprim  10748  ixxdisj  13304  icodisj  13420  fzdisj  13496  nn0disj  13589  fzouzdisj  13641  cotr2g  14929  limsupgle  15430  ello12  15469  elo12  15480  lo1resb  15517  rlimresb  15518  o1resb  15519  lo1eq  15521  rlimeq  15522  fsumsplit  15694  sumsplit  15721  fsum2dlem  15723  fprod2dlem  15936  bitsmod  16396  saddisjlem  16424  sadadd  16427  sadass  16431  smuval2  16442  smupval  16448  smueqlem  16450  smumul  16453  isprm7  16669  prmreclem5  16882  prmrec  16884  4sqlem12  16918  vdwmc  16940  setsstruct2  17135  acsfn  17616  iszeroo  17956  iszeroi  17967  fpwipodrs  18497  psss  18537  insubm  18777  subgacs  19127  nsgacs  19128  resscntz  19299  gsmsymgreq  19398  sylow2a  19585  lsmmod  19641  lsmdisj2  19648  gsumzsplit  19893  subgdmdprd  20002  dprdcntz2  20006  dprddisj2  20007  pgpfac1lem3  20045  rnghmval2  20415  isrhm  20449  subsubrng2  20536  subsubrg2  20571  rnghmsubcsetclem1  20603  funcrngcsetcALT  20613  zrinitorngc  20614  zrtermorngc  20615  rhmsubcsetclem1  20632  rhmsubcrngclem1  20638  ringcbasbas  20645  zrtermoringc  20647  srhmsubclem1  20649  fldhmsubc  20757  acsfn1p  20771  subrgacs  20772  sdrgacs  20773  isorng  20833  lssacs  20957  lspdisj  21118  lspdisjb  21119  dfprm2  21448  irinitoringc  21454  ocvin  21649  unocv  21655  iunocv  21656  obselocv  21703  isassa  21831  aspid  21849  aspval2  21873  pmatcoe1fsupp  22684  isbasis2g  22931  tgval2  22939  tgcl  22952  ppttop  22990  epttop  22992  ssntr  23041  ntreq0  23060  isclo  23070  restntr  23165  restlp  23166  cnpresti  23271  cnprest  23272  cnprest2  23273  lmss  23281  haust1  23335  nrmsep3  23338  isnrm2  23341  lmmo  23363  fincmp  23376  cmpsublem  23382  cmpsub  23383  uncmp  23386  hauscmplem  23389  dfconn2  23402  iunconnlem  23410  unconn  23412  is1stc2  23425  1stcrest  23436  1stcelcls  23444  llyi  23457  nllyi  23458  subislly  23464  lly1stc  23479  txcnp  23603  txcnmpt  23607  hausdiag  23628  kqcldsat  23716  isfbas2  23818  isfil2  23839  fbasfip  23851  elfg  23854  filconn  23866  rnelfmlem  23935  rnelfm  23936  fmfnfmlem2  23938  fmfnfmlem4  23940  fmfnfm  23941  flimrest  23966  hauspwpwf1  23970  fclsrest  24007  alexsubALTlem2  24031  alexsubALTlem3  24032  alexsubALTlem4  24033  alexsubALT  24034  istmd  24057  istgp  24060  tsmssubm  24126  tsmssplit  24135  istrg  24147  istdrg  24149  istlm  24168  ustfilxp  24196  utoptop  24217  utop3cls  24234  bldisj  24381  blin  24404  blres  24414  lpbl  24486  metrest  24507  restmetu  24553  isngp  24579  isnlm  24658  isnmhm  24729  xrtgioo  24790  xrsmopn  24796  icccmplem2  24807  reconnlem2  24811  icoopnst  24924  iocopnst  24925  bndth  24943  zclmncvs  25133  isncvsngp  25134  ncvsprp  25137  ncvsm1  25139  ncvsdif  25140  ncvspi  25141  ncvs1  25142  ncvspds  25146  iscph  25155  tcphcph  25222  cfilfcls  25259  cmetcaulem  25273  isbn  25323  cldcss2  25427  hlhil  25428  ovolfcl  25451  ovolicc2lem2  25503  ovolicc2  25507  shftmbl  25523  volfiniun  25532  mbfmax  25634  mbfimaopnlem  25640  mbfaddlem  25645  i1faddlem  25678  i1fmullem  25679  i1fres  25690  itg1climres  25699  mbfi1fseqlem4  25703  itg2splitlem  25733  itg2split  25734  itgresr  25764  ellimc2  25862  ellimc3  25864  limcun  25880  dvreslem  25894  dvne0  25996  itgsubstlem  26033  ig1pval3  26161  aaliou2  26324  aaliou2b  26325  pilem1  26434  rlimcnp2  26948  fsumharmonic  26993  ppisval2  27086  prmorcht  27159  fsumvma2  27195  pclogsum  27196  vmasum  27197  chpchtsum  27200  chpub  27201  rpvmasum2  27493  madeval2  27843  tglineineq  28729  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  32646  disjorf  32668  ofpreima  32757  1stpreima  32799  2ndpreima  32800  iocinioc2  32871  ssnnssfz  32879  cntzun  33160  kerunit  33408  prmidl0  33533  ressply1mon1p  33651  ccfldextdgrr  33856  crefdf  34032  cmpcref  34034  cmppcmp  34042  cnre2csqima  34095  ordtconnlem1  34108  lmxrge0  34136  isrrext  34184  esum0  34233  esumcst  34247  esumpcvgval  34262  esumcvg  34270  measvuni  34398  eulerpartlemt0  34553  eulerpartlemr  34558  eulerpartlemgf  34563  eulerpartlemgs2  34564  eulerpartlemn  34565  fiblem  34582  oddprm2  34839  bnj1173  35184  bnj1174  35185  bnj1279  35200  elima4  36004  dfon2lem4  36012  ellimits  36136  dfom5b  36138  brapply  36164  brcap  36166  dfrecs2  36178  dfrdg4  36179  finminlem  36546  neibastop2lem  36588  neibastop2  36589  neifg  36599  tailfb  36605  onsucconni  36665  onintopssconn  36668  onsucsuccmpi  36671  limsucncmpi  36673  onint1  36677  mh-infprim2bi  36775  bj-inrab  37280  bj-rcleqf  37378  bj-restuni  37455  bj-opelresdm  37505  bj-idres  37520  bj-opelidres  37521  bj-eldiag  37536  bj-eldiag2  37537  bj-ccinftydisj  37573  taupilem3  37679  isbasisrelowllem1  37717  isbasisrelowllem2  37718  nlpineqsn  37770  fvineqsneu  37773  ptrest  37986  poimirlem29  38016  poimirlem30  38017  mblfinlem2  38025  mbfposadd  38034  itg2gt0cn  38042  dvasin  38071  inixp  38095  0totbnd  38140  sstotbnd3  38143  heibor1lem  38176  heibor1  38177  heiborlem6  38183  isexid2  38222  smgrpismgmOLD  38229  issmgrpOLD  38230  mndoissmgrpOLD  38235  ismndo  38239  exidresid  38246  rngo1cl  38306  isfld2  38372  ineleq  38721  refressn  38900  eleccossin  38940  elrefsymrelsrel  39022  dfeldisj3  39178  eldisjdmqsim  39184  disjlem14  39268  prtlem14  39366  lshpdisj  39479  lkrin  39656  ishlat1  39844  pmodlem2  40339  pclfinN  40392  pclcmpatN  40393  osumcllem4N  40451  pexmidlem1N  40462  dihmeetlem1N  41782  dihglblem5apreN  41783  dihmeetlem4preN  41798  dihmeetlem13N  41811  dochnel2  41884  lcdlss  42111  mapd1o  42140  baerlem3lem2  42202  baerlem5alem2  42203  baerlem5blem2  42204  redvmptabs  42837  cmpfiiin  43146  mrefg2  43156  fz1eqin  43218  fnwe2lem2  43496  islmodfg  43514  islssfg2  43516  lnr2i  43561  rp-fakeinunass  43959  fiinfi  44017  elinintab  44019  elinintrab  44021  elinlem  44042  cnvcnvintabd  44044  ntrneikb  44538  ntrneik3  44540  ntrneik13  44542  ismnushort  44745  radcnvrat  44758  nzin  44762  onfrALTlem2  44990  onfrALTlem2VD  45332  relpmin  45396  pwclaxpow  45428  dfac5prim  45434  modelac8prim  45436  permac8prim  45458  iooabslt  45944  iccintsng  45968  lptioo2cn  46088  lptioo1cn  46089  cncfuni  46329  icccncfext  46330  stoweidlem44  46487  fourierdlem42  46592  fourierdlem80  46629  sge00  46819  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