Theorem elin 3992

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2108  Vcvv 3488   ∩ cin 3975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-in 3983

This theorem is referenced by:  elini  4222  elind  4223  elinel1  4224  elinel2  4225  elin2  4226  elin3  4229  ineqri  4233  nfin  4245  inass  4249  ssin  4260  ssrin  4263  rexin  4269  dfss4  4288  difin  4291  indi  4303  undi  4304  unineq  4307  indifdi  4313  difin2  4320  inrab2  4336  ndisj  4393  inn0f  4394  difin0ss  4396  inssdif0  4397  inelcm  4488  inundif  4502  elinsn  4735  uniin  4955  intun  5004  intprg  5005  elrint  5013  iunin2  5094  iinin2  5101  elriin  5104  disjor  5148  disjiun  5154  brin  5218  trin  5295  inex1  5335  inuni  5368  wefrc  5694  inopab  5853  inxp  5856  inxpOLD  5857  dmin  5936  dfres3  6014  intasym  6147  asymref  6148  dminss  6184  imainss  6185  inimasn  6187  cnvresima  6261  dfco2a  6277  ordtri3or  6427  2elresin  6701  respreima  7099  fvcofneq  7127  tpres  7238  isomin  7373  isoini  7374  offval  7723  ordpwsuc  7851  frpoins3xpg  8181  frpoins3xp3g  8182  xpord3pred  8193  ressuppss  8224  frrlem13  8339  fprlem1  8341  wfrlem5OLD  8369  uniinqs  8855  mapval2  8930  ixpin  8981  boxriin  8998  disjen  9200  ssenen  9217  onfin2  9294  elfpw  9424  fiin  9491  inf3lem2  9698  epfrs  9800  cp  9960  dfac5lem1  10192  dfac5lem5  10196  dfac5  10198  kmlem3  10222  kmlem14  10233  kmlem15  10234  fin23lem26  10394  pwxpndom2  10734  ingru  10884  gruina  10887  grur1  10889  axgroth4  10901  grothprim  10903  ixxdisj  13422  icodisj  13536  fzdisj  13611  nn0disj  13701  fzouzdisj  13752  cotr2g  15025  limsupgle  15523  ello12  15562  elo12  15573  lo1resb  15610  rlimresb  15611  o1resb  15612  lo1eq  15614  rlimeq  15615  fsumsplit  15789  sumsplit  15816  fsum2dlem  15818  fprod2dlem  16028  bitsmod  16482  saddisjlem  16510  sadadd  16513  sadass  16517  smuval2  16528  smupval  16534  smueqlem  16536  smumul  16539  isprm7  16755  prmreclem5  16967  prmrec  16969  4sqlem12  17003  vdwmc  17025  setsstruct2  17221  acsfn  17717  iszeroo  18065  iszeroi  18076  fpwipodrs  18610  psss  18650  insubm  18853  subgacs  19201  nsgacs  19202  resscntz  19373  gsmsymgreq  19474  sylow2a  19661  lsmmod  19717  lsmdisj2  19724  gsumzsplit  19969  subgdmdprd  20078  dprdcntz2  20082  dprddisj2  20083  pgpfac1lem3  20121  rnghmval2  20470  isrhm  20504  subsubrng2  20590  subsubrg2  20627  rnghmsubcsetclem1  20653  funcrngcsetcALT  20663  zrinitorngc  20664  zrtermorngc  20665  rhmsubcsetclem1  20682  rhmsubcrngclem1  20688  ringcbasbas  20695  zrtermoringc  20697  srhmsubclem1  20699  fldhmsubc  20808  acsfn1p  20822  subrgacs  20823  sdrgacs  20824  lssacs  20988  lspdisj  21150  lspdisjb  21151  dfprm2  21507  irinitoringc  21513  ocvin  21715  unocv  21721  iunocv  21722  obselocv  21771  isassa  21899  aspid  21918  aspval2  21941  pmatcoe1fsupp  22728  isbasis2g  22976  tgval2  22984  tgcl  22997  ppttop  23035  epttop  23037  ssntr  23087  ntreq0  23106  isclo  23116  restntr  23211  restlp  23212  cnpresti  23317  cnprest  23318  cnprest2  23319  lmss  23327  haust1  23381  nrmsep3  23384  isnrm2  23387  lmmo  23409  fincmp  23422  cmpsublem  23428  cmpsub  23429  uncmp  23432  hauscmplem  23435  dfconn2  23448  iunconnlem  23456  unconn  23458  is1stc2  23471  1stcrest  23482  1stcelcls  23490  llyi  23503  nllyi  23504  subislly  23510  lly1stc  23525  txcnp  23649  txcnmpt  23653  hausdiag  23674  kqcldsat  23762  isfbas2  23864  isfil2  23885  fbasfip  23897  elfg  23900  filconn  23912  rnelfmlem  23981  rnelfm  23982  fmfnfmlem2  23984  fmfnfmlem4  23986  fmfnfm  23987  flimrest  24012  hauspwpwf1  24016  fclsrest  24053  alexsubALTlem2  24077  alexsubALTlem3  24078  alexsubALTlem4  24079  alexsubALT  24080  istmd  24103  istgp  24106  tsmssubm  24172  tsmssplit  24181  istrg  24193  istdrg  24195  istlm  24214  ustfilxp  24242  utoptop  24264  utop3cls  24281  bldisj  24429  blin  24452  blres  24462  lpbl  24537  metrest  24558  restmetu  24604  isngp  24630  isnlm  24717  isnmhm  24788  xrtgioo  24847  xrsmopn  24853  icccmplem2  24864  reconnlem2  24868  icoopnst  24988  iocopnst  24989  bndth  25009  zclmncvs  25201  isncvsngp  25202  ncvsprp  25205  ncvsm1  25207  ncvsdif  25208  ncvspi  25209  ncvs1  25210  ncvspds  25214  iscph  25223  tcphcph  25290  cfilfcls  25327  cmetcaulem  25341  isbn  25391  cldcss2  25495  hlhil  25496  ovolfcl  25520  ovolicc2lem2  25572  ovolicc2  25576  shftmbl  25592  volfiniun  25601  mbfmax  25703  mbfimaopnlem  25709  mbfaddlem  25714  i1faddlem  25747  i1fmullem  25748  i1fres  25760  itg1climres  25769  mbfi1fseqlem4  25773  itg2splitlem  25803  itg2split  25804  itgresr  25834  ellimc2  25932  ellimc3  25934  limcun  25950  dvreslem  25964  dvne0  26070  itgsubstlem  26109  ig1pval3  26237  aaliou2  26400  aaliou2b  26401  pilem1  26513  rlimcnp2  27027  fsumharmonic  27073  ppisval2  27166  prmorcht  27239  fsumvma2  27276  pclogsum  27277  vmasum  27278  chpchtsum  27281  chpub  27282  rpvmasum2  27574  madeval2  27910  tglineineq  28669  trlsegvdeg  30259  frgrncvvdeqlem7  30337  frgrncvvdeqlem9  30339  minvecolem1  30906  minvecolem4a  30909  minvecolem4b  30910  minvecolem4  30912  h2hcau  31011  axhcompl-zf  31030  hhcmpl  31232  hhcms  31235  ocin  31328  ocnel  31330  shmodsi  31421  pjhthlem2  31424  omlsilem  31434  pjoc1i  31463  spansnm0i  31682  nonbooli  31683  5oalem7  31692  3oalem3  31696  pjssmii  31713  mayete3i  31760  nmcopex  32061  nmcoplb  32062  lncnopbd  32069  nmcfnex  32085  nmcfnlb  32086  riesz4  32096  riesz1  32097  riesz2  32098  cnlnadjlem3  32101  cnlnadjlem5  32103  cnlnadjlem9  32107  cnlnadjeu  32110  rnbra  32139  pjimai  32208  pjclem4a  32230  pj3lem1  32238  jpi  32302  sumdmdii  32447  sumdmdlem  32450  sumdmdlem2  32451  cdjreui  32464  cdj3lem1  32466  iunin1f  32580  disjorf  32601  ofpreima  32683  1stpreima  32718  2ndpreima  32719  iocinioc2  32784  ssnnssfz  32792  cntzun  33044  isorng  33294  kerunit  33314  prmidl0  33443  ressply1mon1p  33558  ccfldextdgrr  33682  crefdf  33794  cmpcref  33796  cmppcmp  33804  cnre2csqima  33857  ordtconnlem1  33870  lmxrge0  33898  isrrext  33946  esum0  34013  esumcst  34027  esumpcvgval  34042  esumcvg  34050  measvuni  34178  eulerpartlemt0  34334  eulerpartlemr  34339  eulerpartlemgf  34344  eulerpartlemgs2  34345  eulerpartlemn  34346  fiblem  34363  oddprm2  34632  bnj1173  34978  bnj1174  34979  bnj1279  34994  elima4  35739  dfon2lem4  35750  ellimits  35874  dfom5b  35876  brapply  35902  brcap  35904  dfrecs2  35914  dfrdg4  35915  finminlem  36284  neibastop2lem  36326  neibastop2  36327  neifg  36337  tailfb  36343  onsucconni  36403  onintopssconn  36406  onsucsuccmpi  36409  limsucncmpi  36411  onint1  36415  bj-inrab  36893  bj-rcleqf  36991  bj-restuni  37063  bj-opelresdm  37111  bj-idres  37126  bj-opelidres  37127  bj-eldiag  37142  bj-eldiag2  37143  bj-ccinftydisj  37179  taupilem3  37285  isbasisrelowllem1  37321  isbasisrelowllem2  37322  nlpineqsn  37374  fvineqsneu  37377  ptrest  37579  poimirlem29  37609  poimirlem30  37610  mblfinlem2  37618  mbfposadd  37627  itg2gt0cn  37635  dvasin  37664  inixp  37688  0totbnd  37733  sstotbnd3  37736  heibor1lem  37769  heibor1  37770  heiborlem6  37776  isexid2  37815  smgrpismgmOLD  37822  issmgrpOLD  37823  mndoissmgrpOLD  37828  ismndo  37832  exidresid  37839  rngo1cl  37899  isfld2  37965  ralin  38204  ineleq  38310  refressn  38399  eleccossin  38439  elrefsymrelsrel  38527  dfeldisj3  38675  disjlem14  38754  prtlem14  38830  lshpdisj  38943  lkrin  39120  ishlat1  39308  pmodlem2  39804  pclfinN  39857  pclcmpatN  39858  osumcllem4N  39916  pexmidlem1N  39927  dihmeetlem1N  41247  dihglblem5apreN  41248  dihmeetlem4preN  41263  dihmeetlem13N  41276  dochnel2  41349  lcdlss  41576  mapd1o  41605  baerlem3lem2  41667  baerlem5alem2  41668  baerlem5blem2  41669  cmpfiiin  42653  mrefg2  42663  fz1eqin  42725  fnwe2lem2  43008  islmodfg  43026  islssfg2  43028  lnr2i  43073  rp-fakeinunass  43477  fiinfi  43535  elinintab  43537  elinintrab  43539  elinlem  43560  cnvcnvintabd  43562  ntrneikb  44056  ntrneik3  44058  ntrneik13  44060  ismnushort  44270  radcnvrat  44283  nzin  44287  onfrALTlem2  44517  onfrALTlem2VD  44860  iooabslt  45417  iccintsng  45441  lptioo2cn  45566  lptioo1cn  45567  cncfuni  45807  icccncfext  45808  stoweidlem44  45965  fourierdlem42  46070  fourierdlem80  46107  sge00  46297  eldmressn  46952  afvres  47087  afv2res  47154  prproropf1olem0  47376  31prm  47471  rngccatidALTV  47995  rhmsubcALTVlem3  48006  funcringcsetcALTV2lem7  48019  ringccatidALTV  48029  ringcbasbasALTV  48035  funcringcsetclem7ALTV  48042  fldhmsubcALTV  48056  ssnn0ssfz  48074  elbigo2  48286  itsclinecirc0in  48509  opndisj  48582  clddisj  48583  i0oii  48599  io1ii  48600