Theorem elin 3913

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2111  Vcvv 3436   ∩ cin 3896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-in 3904

This theorem is referenced by:  elini  4146  elind  4147  elinel1  4148  elinel2  4149  elin2  4150  elin3  4153  ineqri  4159  nfin  4171  inass  4175  ssin  4186  ssrin  4189  ralin  4196  rexin  4197  dfss4  4216  difin  4219  indi  4231  undi  4232  unineq  4235  indifdi  4241  difin2  4248  inrab2  4264  ndisj  4317  inn0f  4318  difin0ss  4320  inssdif0  4321  inelcm  4412  inundif  4426  elinsn  4660  uniin  4880  intun  4928  intprg  4929  elrint  4937  iunin2  5017  iinin2  5024  elriin  5027  disjor  5071  disjiun  5077  brin  5141  trin  5207  inex1  5253  inuni  5286  wefrc  5608  inopab  5768  inxp  5770  inxpOLD  5771  dmin  5850  dfres3  5932  intasym  6061  asymref  6062  dminss  6100  imainss  6101  inimasn  6103  cnvresima  6177  dfco2a  6193  ordtri3or  6338  2elresin  6602  respreima  6999  fvcofneq  7026  tpres  7135  isomin  7271  isoini  7272  offval  7619  ordpwsuc  7745  frpoins3xpg  8070  frpoins3xp3g  8071  xpord3pred  8082  ressuppss  8113  frrlem13  8228  fprlem1  8230  uniinqs  8721  mapval2  8796  ixpin  8847  boxriin  8864  disjen  9047  ssenen  9064  onfin2  9125  elfpw  9238  fiin  9306  inf3lem2  9519  epfrs  9621  cp  9784  dfac5lem1  10014  dfac5lem5  10018  dfac5  10020  kmlem3  10044  kmlem14  10055  kmlem15  10056  fin23lem26  10216  pwxpndom2  10556  ingru  10706  gruina  10709  grur1  10711  axgroth4  10723  grothprim  10725  ixxdisj  13260  icodisj  13376  fzdisj  13451  nn0disj  13544  fzouzdisj  13595  cotr2g  14883  limsupgle  15384  ello12  15423  elo12  15434  lo1resb  15471  rlimresb  15472  o1resb  15473  lo1eq  15475  rlimeq  15476  fsumsplit  15648  sumsplit  15675  fsum2dlem  15677  fprod2dlem  15887  bitsmod  16347  saddisjlem  16375  sadadd  16378  sadass  16382  smuval2  16393  smupval  16399  smueqlem  16401  smumul  16404  isprm7  16619  prmreclem5  16832  prmrec  16834  4sqlem12  16868  vdwmc  16890  setsstruct2  17085  acsfn  17565  iszeroo  17905  iszeroi  17916  fpwipodrs  18446  psss  18486  insubm  18726  subgacs  19073  nsgacs  19074  resscntz  19245  gsmsymgreq  19344  sylow2a  19531  lsmmod  19587  lsmdisj2  19594  gsumzsplit  19839  subgdmdprd  19948  dprdcntz2  19952  dprddisj2  19953  pgpfac1lem3  19991  rnghmval2  20362  isrhm  20396  subsubrng2  20479  subsubrg2  20514  rnghmsubcsetclem1  20546  funcrngcsetcALT  20556  zrinitorngc  20557  zrtermorngc  20558  rhmsubcsetclem1  20575  rhmsubcrngclem1  20581  ringcbasbas  20588  zrtermoringc  20590  srhmsubclem1  20592  fldhmsubc  20700  acsfn1p  20714  subrgacs  20715  sdrgacs  20716  isorng  20776  lssacs  20900  lspdisj  21062  lspdisjb  21063  dfprm2  21410  irinitoringc  21416  ocvin  21611  unocv  21617  iunocv  21618  obselocv  21665  isassa  21793  aspid  21812  aspval2  21835  pmatcoe1fsupp  22616  isbasis2g  22863  tgval2  22871  tgcl  22884  ppttop  22922  epttop  22924  ssntr  22973  ntreq0  22992  isclo  23002  restntr  23097  restlp  23098  cnpresti  23203  cnprest  23204  cnprest2  23205  lmss  23213  haust1  23267  nrmsep3  23270  isnrm2  23273  lmmo  23295  fincmp  23308  cmpsublem  23314  cmpsub  23315  uncmp  23318  hauscmplem  23321  dfconn2  23334  iunconnlem  23342  unconn  23344  is1stc2  23357  1stcrest  23368  1stcelcls  23376  llyi  23389  nllyi  23390  subislly  23396  lly1stc  23411  txcnp  23535  txcnmpt  23539  hausdiag  23560  kqcldsat  23648  isfbas2  23750  isfil2  23771  fbasfip  23783  elfg  23786  filconn  23798  rnelfmlem  23867  rnelfm  23868  fmfnfmlem2  23870  fmfnfmlem4  23872  fmfnfm  23873  flimrest  23898  hauspwpwf1  23902  fclsrest  23939  alexsubALTlem2  23963  alexsubALTlem3  23964  alexsubALTlem4  23965  alexsubALT  23966  istmd  23989  istgp  23992  tsmssubm  24058  tsmssplit  24067  istrg  24079  istdrg  24081  istlm  24100  ustfilxp  24128  utoptop  24149  utop3cls  24166  bldisj  24313  blin  24336  blres  24346  lpbl  24418  metrest  24439  restmetu  24485  isngp  24511  isnlm  24590  isnmhm  24661  xrtgioo  24722  xrsmopn  24728  icccmplem2  24739  reconnlem2  24743  icoopnst  24863  iocopnst  24864  bndth  24884  zclmncvs  25075  isncvsngp  25076  ncvsprp  25079  ncvsm1  25081  ncvsdif  25082  ncvspi  25083  ncvs1  25084  ncvspds  25088  iscph  25097  tcphcph  25164  cfilfcls  25201  cmetcaulem  25215  isbn  25265  cldcss2  25369  hlhil  25370  ovolfcl  25394  ovolicc2lem2  25446  ovolicc2  25450  shftmbl  25466  volfiniun  25475  mbfmax  25577  mbfimaopnlem  25583  mbfaddlem  25588  i1faddlem  25621  i1fmullem  25622  i1fres  25633  itg1climres  25642  mbfi1fseqlem4  25646  itg2splitlem  25676  itg2split  25677  itgresr  25707  ellimc2  25805  ellimc3  25807  limcun  25823  dvreslem  25837  dvne0  25943  itgsubstlem  25982  ig1pval3  26110  aaliou2  26275  aaliou2b  26276  pilem1  26388  rlimcnp2  26903  fsumharmonic  26949  ppisval2  27042  prmorcht  27115  fsumvma2  27152  pclogsum  27153  vmasum  27154  chpchtsum  27157  chpub  27158  rpvmasum2  27450  madeval2  27794  tglineineq  28621  trlsegvdeg  30207  frgrncvvdeqlem7  30285  frgrncvvdeqlem9  30287  minvecolem1  30854  minvecolem4a  30857  minvecolem4b  30858  minvecolem4  30860  h2hcau  30959  axhcompl-zf  30978  hhcmpl  31180  hhcms  31183  ocin  31276  ocnel  31278  shmodsi  31369  pjhthlem2  31372  omlsilem  31382  pjoc1i  31411  spansnm0i  31630  nonbooli  31631  5oalem7  31640  3oalem3  31644  pjssmii  31661  mayete3i  31708  nmcopex  32009  nmcoplb  32010  lncnopbd  32017  nmcfnex  32033  nmcfnlb  32034  riesz4  32044  riesz1  32045  riesz2  32046  cnlnadjlem3  32049  cnlnadjlem5  32051  cnlnadjlem9  32055  cnlnadjeu  32058  rnbra  32087  pjimai  32156  pjclem4a  32178  pj3lem1  32186  jpi  32250  sumdmdii  32395  sumdmdlem  32398  sumdmdlem2  32399  cdjreui  32412  cdj3lem1  32414  iunin1f  32537  disjorf  32559  ofpreima  32647  1stpreima  32688  2ndpreima  32689  iocinioc2  32762  ssnnssfz  32770  cntzun  33048  kerunit  33290  prmidl0  33415  ressply1mon1p  33531  ccfldextdgrr  33685  crefdf  33861  cmpcref  33863  cmppcmp  33871  cnre2csqima  33924  ordtconnlem1  33937  lmxrge0  33965  isrrext  34013  esum0  34062  esumcst  34076  esumpcvgval  34091  esumcvg  34099  measvuni  34227  eulerpartlemt0  34382  eulerpartlemr  34387  eulerpartlemgf  34392  eulerpartlemgs2  34393  eulerpartlemn  34394  fiblem  34411  oddprm2  34668  bnj1173  35014  bnj1174  35015  bnj1279  35030  elima4  35820  dfon2lem4  35828  ellimits  35952  dfom5b  35954  brapply  35980  brcap  35982  dfrecs2  35994  dfrdg4  35995  finminlem  36362  neibastop2lem  36404  neibastop2  36405  neifg  36415  tailfb  36421  onsucconni  36481  onintopssconn  36484  onsucsuccmpi  36487  limsucncmpi  36489  onint1  36493  bj-inrab  36971  bj-rcleqf  37069  bj-restuni  37141  bj-opelresdm  37189  bj-idres  37204  bj-opelidres  37205  bj-eldiag  37220  bj-eldiag2  37221  bj-ccinftydisj  37257  taupilem3  37363  isbasisrelowllem1  37399  isbasisrelowllem2  37400  nlpineqsn  37452  fvineqsneu  37455  ptrest  37669  poimirlem29  37699  poimirlem30  37700  mblfinlem2  37708  mbfposadd  37717  itg2gt0cn  37725  dvasin  37754  inixp  37778  0totbnd  37823  sstotbnd3  37826  heibor1lem  37859  heibor1  37860  heiborlem6  37866  isexid2  37905  smgrpismgmOLD  37912  issmgrpOLD  37913  mndoissmgrpOLD  37918  ismndo  37922  exidresid  37929  rngo1cl  37989  isfld2  38055  ineleq  38396  refressn  38555  eleccossin  38595  elrefsymrelsrel  38677  dfeldisj3  38827  disjlem14  38906  prtlem14  38983  lshpdisj  39096  lkrin  39273  ishlat1  39461  pmodlem2  39956  pclfinN  40009  pclcmpatN  40010  osumcllem4N  40068  pexmidlem1N  40079  dihmeetlem1N  41399  dihglblem5apreN  41400  dihmeetlem4preN  41415  dihmeetlem13N  41428  dochnel2  41501  lcdlss  41728  mapd1o  41757  baerlem3lem2  41819  baerlem5alem2  41820  baerlem5blem2  41821  redvmptabs  42463  cmpfiiin  42800  mrefg2  42810  fz1eqin  42872  fnwe2lem2  43154  islmodfg  43172  islssfg2  43174  lnr2i  43219  rp-fakeinunass  43618  fiinfi  43676  elinintab  43678  elinintrab  43680  elinlem  43701  cnvcnvintabd  43703  ntrneikb  44197  ntrneik3  44199  ntrneik13  44201  ismnushort  44404  radcnvrat  44417  nzin  44421  onfrALTlem2  44649  onfrALTlem2VD  44991  relpmin  45055  pwclaxpow  45087  dfac5prim  45093  modelac8prim  45095  permac8prim  45117  iooabslt  45609  iccintsng  45633  lptioo2cn  45753  lptioo1cn  45754  cncfuni  45994  icccncfext  45995  stoweidlem44  46152  fourierdlem42  46257  fourierdlem80  46294  sge00  46484  eldmressn  47147  afvres  47282  afv2res  47349  prproropf1olem0  47612  31prm  47707  rngccatidALTV  48382  rhmsubcALTVlem3  48393  funcringcsetcALTV2lem7  48406  ringccatidALTV  48416  ringcbasbasALTV  48422  funcringcsetclem7ALTV  48429  fldhmsubcALTV  48443  ssnn0ssfz  48459  elbigo2  48663  itsclinecirc0in  48886  resinsnALT  48983  opndisj  49013  clddisj  49014  i0oii  49030  io1ii  49031