Theorem elin 4024

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 3430	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 3430	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	adantl 475	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2895	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2895	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	4, 5	anbi12d 626	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
7		df-in 3806	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 3575	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 370	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 198   ∧ wa 386   = wceq 1658   ∈ wcel 2166  Vcvv 3415   ∩ cin 3798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2804

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-v 3417  df-in 3806

This theorem is referenced by:  elini  4025  elind  4026  elinel1  4027  elinel2  4028  elin2  4029  elin3  4032  incom  4033  ineqri  4034  ineq1  4035  inass  4049  ssin  4060  ssrin  4063  rexin  4069  dfss4  4089  difin  4092  indi  4104  undi  4105  unineq  4108  indifdir  4114  difin2  4120  inrab2  4130  ndisj  4176  difin0ss  4177  inssdif0  4178  inelcm  4257  inundif  4270  elinsn  4465  uniin  4681  intun  4730  intpr  4731  elrint  4739  iunin2  4805  iinin2  4811  elriin  4814  disjor  4856  disjiun  4862  brin  4926  trin  4986  inex1  5025  inuni  5049  wefrc  5337  inopab  5486  inxp  5488  dmin  5565  dfres3  5635  opelresgOLD2  5640  intasym  5754  asymref  5755  dminss  5789  imainss  5790  inimasn  5792  cnvresima  5865  dfco2a  5877  ordtri3or  5996  2elresin  6236  respreima  6594  fvcofneq  6617  tpres  6723  isomin  6843  isoini  6844  offval  7165  ordpwsuc  7277  ressuppss  7579  wfrlem5  7686  erdisj  8060  uniinqs  8093  mapval2  8153  ixpin  8201  boxriin  8218  disjen  8387  ssenen  8404  onfin2  8422  elfpw  8538  fiin  8598  inf3lem2  8804  epfrs  8885  cp  9032  bnd2  9034  dfac5lem1  9260  dfac5lem5  9264  dfac5  9265  kmlem3  9290  kmlem14  9301  kmlem15  9302  fin23lem26  9463  isfin1-3  9524  pwxpndom2  9803  ingru  9953  gruina  9956  grur1  9958  axgroth4  9970  grothprim  9972  ixxdisj  12479  icodisj  12589  fzdisj  12662  uzdisj  12708  nn0disj  12751  fzouzdisj  12800  xpcogend  14093  cotr2g  14095  limsupgle  14586  ello12  14625  elo12  14636  lo1resb  14673  rlimresb  14674  o1resb  14675  lo1eq  14677  rlimeq  14678  fsumsplit  14849  sumsplit  14875  fsum2dlem  14877  explecnv  14972  fprod2dlem  15084  bitsmod  15532  saddisjlem  15560  sadadd  15563  sadass  15567  smuval2  15578  smupval  15584  smueqlem  15586  smumul  15589  isprm7  15792  prmreclem5  15996  prmrec  15998  4sqlem12  16032  vdwmc  16054  setsstruct2  16261  acsfn  16673  iszeroo  17005  iszeroi  17012  isdrs2  17293  fpwipodrs  17518  psss  17568  subgacs  17981  nsgacs  17982  resscntz  18115  gsmsymgreq  18203  sylow2a  18386  lsmmod  18440  lsmdisj2  18447  gsumzsplit  18681  subgdmdprd  18788  dprdcntz2  18792  dprddisj2  18793  pgpfac1lem3  18831  isrhm  19078  subsubrg2  19164  lssacs  19327  lspdisj  19485  lspdisjb  19486  isassa  19677  aspid  19692  aspval2  19709  dfprm2  20203  ocvin  20382  unocv  20388  iunocv  20389  obselocv  20436  pmatcoe1fsupp  20877  isbasis2g  21124  tgval2  21132  tgcl  21145  ppttop  21183  epttop  21185  clsval2  21226  ssntr  21234  ntreq0  21253  isclo  21263  restntr  21358  restlp  21359  cnpresti  21464  cnprest  21465  cnprest2  21466  lmss  21474  haust1  21528  nrmsep3  21531  isnrm2  21534  lmmo  21556  fincmp  21568  0cmp  21569  discmp  21573  cmpsublem  21574  cmpsub  21575  uncmp  21578  hauscmplem  21581  dfconn2  21594  iunconnlem  21602  unconn  21604  is1stc2  21617  1stcrest  21628  1stcelcls  21636  llyi  21649  nllyi  21650  subislly  21656  lly1stc  21671  comppfsc  21707  txcnp  21795  txcnmpt  21799  hausdiag  21820  kqcldsat  21908  ptcmpfi  21988  isfbas2  22010  isfil2  22031  fbasfip  22043  elfg  22046  filconn  22058  rnelfmlem  22127  rnelfm  22128  fmfnfmlem2  22130  fmfnfmlem4  22132  fmfnfm  22133  flimrest  22158  hauspwpwf1  22162  fclsrest  22199  alexsubALTlem2  22223  alexsubALTlem3  22224  alexsubALTlem4  22225  alexsubALT  22226  ptcmp  22233  istmd  22249  istgp  22252  tsmssubm  22317  tsmssplit  22326  istrg  22338  istdrg  22340  istlm  22359  ustfilxp  22387  utoptop  22409  utop3cls  22426  bldisj  22574  blin  22597  blin2  22605  blres  22607  lpbl  22679  metrest  22700  restmetu  22746  isngp  22771  isnlm  22850  isnmhm  22921  xrtgioo  22980  xrsmopn  22986  icccmplem2  22997  reconnlem2  23001  icoopnst  23109  iocopnst  23110  bndth  23128  cvsi  23300  cnstrcvs  23311  cncvs  23315  zclmncvs  23318  isncvsngp  23319  ncvsprp  23322  ncvsm1  23324  ncvsdif  23325  ncvspi  23326  ncvs1  23327  ncvspds  23331  iscph  23340  tcphcph  23406  cfilfcls  23443  cmetcaulem  23457  isbn  23507  cldcss2  23611  hlhil  23612  ovolfcl  23633  ovolicc1  23683  ovolicc2lem2  23685  ovolicc2lem4  23687  ovolicc2lem5  23688  ovolicc2  23689  shftmbl  23705  volfiniun  23714  ioorf  23740  mbfmax  23816  mbfimaopnlem  23822  mbfaddlem  23827  mbfadd  23828  mbfsub  23829  i1faddlem  23860  i1fmullem  23861  i1fres  23872  itg1climres  23881  mbfi1fseqlem4  23885  mbfmul  23893  itg2splitlem  23915  itg2split  23916  itgresr  23945  bddmulibl  24005  ellimc2  24041  ellimc3  24043  limcun  24059  dvreslem  24073  dvne0  24174  itgsubstlem  24211  ig1pval3  24334  aaliou2  24495  aaliou2b  24496  pilem1  24605  rlimcnp2  25107  fsumharmonic  25152  ppisval2  25245  prmorcht  25318  fsumvma2  25353  pclogsum  25354  vmasum  25355  chpchtsum  25358  chpub  25359  chebbnd1lem1  25572  rpvmasum2  25615  tglineineq  25956  trlsegvdeg  27605  frgrncvvdeqlem7  27687  frgrncvvdeqlem9  27689  minvecolem1  28286  minvecolem4a  28289  minvecolem4b  28290  minvecolem4  28292  h2hcau  28392  axhcompl-zf  28411  hhcmpl  28613  hhcms  28616  ocin  28711  ocnel  28713  shmodsi  28804  pjhthlem2  28807  omlsilem  28817  pjoc1i  28846  spansnm0i  29065  nonbooli  29066  5oalem7  29075  3oalem3  29079  pjssmii  29096  mayete3i  29143  nmcopex  29444  nmcoplb  29445  lncnopbd  29452  nmcfnex  29468  nmcfnlb  29469  riesz4  29479  riesz1  29480  riesz2  29481  cnlnadjlem3  29484  cnlnadjlem5  29486  cnlnadjlem9  29490  cnlnadjeu  29493  rnbra  29522  pjimai  29591  pjclem4a  29613  pj3lem1  29621  jpi  29685  sumdmdii  29830  sumdmdlem  29833  sumdmdlem2  29834  cdjreui  29847  cdj3lem1  29849  iunin1f  29923  disjorf  29940  ofpreima  30015  1stpreima  30033  2ndpreima  30034  iocinioc2  30089  ssnnssfz  30097  isorng  30345  kerunit  30369  crefdf  30461  cmpcref  30463  cmppcmp  30471  pcmplfin  30473  cnre2csqima  30503  ordtconnlem1  30516  lmxrge0  30544  isrrext  30590  esum0  30657  esumcst  30671  esumpcvgval  30686  esumcvg  30694  measvuni  30823  eulerpartlemt0  30977  eulerpartlemr  30982  eulerpartlemgf  30987  eulerpartlemgs2  30988  eulerpartlemn  30989  fiblem  31007  oddprm2  31283  bnj521  31353  bnj1173  31617  bnj1174  31618  bnj1279  31633  elima4  32218  imaindm  32221  dfon2lem4  32230  frrlem5  32324  madeval2  32476  ellimits  32557  dfom5b  32559  brapply  32585  brcap  32587  dfrecs2  32597  dfrdg4  32598  finminlem  32852  neibastop2lem  32894  neibastop2  32895  neifg  32905  tailfb  32911  onsucconni  32970  onintopssconn  32973  onsucsuccmpi  32976  limsucncmpi  32978  onint1  32982  bj-inrab  33448  bj-restuni  33574  bj-eldiag  33621  bj-eldiag2  33622  bj-ccinftydisj  33641  taupilem3  33712  isbasisrelowllem1  33749  isbasisrelowllem2  33750  ptrest  33953  poimirlem29  33983  poimirlem30  33984  mblfinlem2  33992  mbfposadd  34001  itg2gt0cn  34009  dvasin  34040  inixp  34067  0totbnd  34115  sstotbnd3  34118  heibor1lem  34151  heibor1  34152  heiborlem6  34158  isexid2  34197  smgrpismgmOLD  34204  issmgrpOLD  34205  mndoissmgrpOLD  34210  ismndo  34214  exidresid  34221  rngo1cl  34281  isfld2  34347  ineleq  34668  eleccossin  34782  elrefsymrelsrel  34866  prtlem14  34950  lshpdisj  35063  lkrin  35240  ishlat1  35428  pmodlem2  35923  pclfinN  35976  pclcmpatN  35977  osumcllem4N  36035  pexmidlem1N  36046  dihmeetlem1N  37366  dihglblem5apreN  37367  dihmeetlem4preN  37382  dihmeetlem13N  37395  dochnel2  37468  lcdlss  37695  mapd1o  37724  baerlem3lem2  37786  baerlem5alem2  37787  baerlem5blem2  37788  cmpfiiin  38105  mrefg2  38115  fz1eqin  38177  fnwe2lem2  38465  islmodfg  38483  islssfg2  38485  lnr2i  38530  acsfn1p  38613  subrgacs  38614  sdrgacs  38615  rp-fakeinunass  38703  fiinfi  38720  elinintab  38723  elinintrab  38725  elinlem  38746  cnvcnvintabd  38748  ntrneikb  39233  ntrneik3  39235  ntrneik13  39237  radcnvrat  39354  nzin  39358  onfrALTlem2  39591  onfrALTlem2VD  39944  inn0f  40060  iooabslt  40521  iccintsng  40546  lptioo2cn  40673  lptioo1cn  40674  cncfuni  40895  icccncfext  40896  stoweidlem44  41056  fourierdlem42  41161  fourierdlem80  41198  sge00  41385  eldmressn  41969  afvres  42075  afv2res  42142  31prm  42343  rnghmval2  42743  rnghmsubcsetclem1  42823  rngccatidALTV  42837  funcrngcsetcALT  42847  zrinitorngc  42848  zrtermorngc  42849  rhmsubcsetclem1  42869  rhmsubcrngclem1  42875  ringcbasbas  42882  funcringcsetcALTV2lem7  42890  ringccatidALTV  42900  ringcbasbasALTV  42906  funcringcsetclem7ALTV  42913  irinitoringc  42917  zrtermoringc  42918  srhmsubclem1  42921  fldhmsubc  42932  fldhmsubcALTV  42950  rhmsubcALTVlem3  42954  ssnn0ssfz  42975  elbigo2  43194