Theorem elin 3919

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3442   ∩ cin 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-in 3910

This theorem is referenced by:  elini  4153  elind  4154  elinel1  4155  elinel2  4156  elin2  4157  elin3  4160  ineqri  4166  nfin  4178  inass  4182  ssin  4193  ssrin  4196  ralin  4203  rexin  4204  dfss4  4223  difin  4226  indi  4238  undi  4239  unineq  4242  indifdi  4248  difin2  4255  inrab2  4271  ndisj  4324  inn0f  4325  difin0ss  4327  inssdif0  4328  inelcm  4419  inundif  4433  elinsn  4669  uniin  4889  intun  4937  intprg  4938  elrint  4946  iunin2  5028  iinin2  5035  elriin  5038  disjor  5082  disjiun  5088  brin  5152  trin  5218  inex1  5264  inuni  5297  wefrc  5626  inopab  5786  inxp  5788  inxpOLD  5789  dmin  5868  dfres3  5951  intasym  6080  asymref  6081  dminss  6119  imainss  6120  inimasn  6122  cnvresima  6196  dfco2a  6212  ordtri3or  6357  2elresin  6621  respreima  7020  fvcofneq  7047  tpres  7157  isomin  7293  isoini  7294  offval  7641  ordpwsuc  7767  frpoins3xpg  8092  frpoins3xp3g  8093  xpord3pred  8104  ressuppss  8135  frrlem13  8250  fprlem1  8252  uniinqs  8746  mapval2  8822  ixpin  8873  boxriin  8890  disjen  9074  ssenen  9091  onfin2  9153  elfpw  9266  fiin  9337  inf3lem2  9550  epfrs  9652  cp  9815  dfac5lem1  10045  dfac5lem5  10049  dfac5  10051  kmlem3  10075  kmlem14  10086  kmlem15  10087  fin23lem26  10247  pwxpndom2  10588  ingru  10738  gruina  10741  grur1  10743  axgroth4  10755  grothprim  10757  ixxdisj  13288  icodisj  13404  fzdisj  13479  nn0disj  13572  fzouzdisj  13623  cotr2g  14911  limsupgle  15412  ello12  15451  elo12  15462  lo1resb  15499  rlimresb  15500  o1resb  15501  lo1eq  15503  rlimeq  15504  fsumsplit  15676  sumsplit  15703  fsum2dlem  15705  fprod2dlem  15915  bitsmod  16375  saddisjlem  16403  sadadd  16406  sadass  16410  smuval2  16421  smupval  16427  smueqlem  16429  smumul  16432  isprm7  16647  prmreclem5  16860  prmrec  16862  4sqlem12  16896  vdwmc  16918  setsstruct2  17113  acsfn  17594  iszeroo  17934  iszeroi  17945  fpwipodrs  18475  psss  18515  insubm  18755  subgacs  19102  nsgacs  19103  resscntz  19274  gsmsymgreq  19373  sylow2a  19560  lsmmod  19616  lsmdisj2  19623  gsumzsplit  19868  subgdmdprd  19977  dprdcntz2  19981  dprddisj2  19982  pgpfac1lem3  20020  rnghmval2  20392  isrhm  20426  subsubrng2  20509  subsubrg2  20544  rnghmsubcsetclem1  20576  funcrngcsetcALT  20586  zrinitorngc  20587  zrtermorngc  20588  rhmsubcsetclem1  20605  rhmsubcrngclem1  20611  ringcbasbas  20618  zrtermoringc  20620  srhmsubclem1  20622  fldhmsubc  20730  acsfn1p  20744  subrgacs  20745  sdrgacs  20746  isorng  20806  lssacs  20930  lspdisj  21092  lspdisjb  21093  dfprm2  21440  irinitoringc  21446  ocvin  21641  unocv  21647  iunocv  21648  obselocv  21695  isassa  21823  aspid  21842  aspval2  21866  pmatcoe1fsupp  22657  isbasis2g  22904  tgval2  22912  tgcl  22925  ppttop  22963  epttop  22965  ssntr  23014  ntreq0  23033  isclo  23043  restntr  23138  restlp  23139  cnpresti  23244  cnprest  23245  cnprest2  23246  lmss  23254  haust1  23308  nrmsep3  23311  isnrm2  23314  lmmo  23336  fincmp  23349  cmpsublem  23355  cmpsub  23356  uncmp  23359  hauscmplem  23362  dfconn2  23375  iunconnlem  23383  unconn  23385  is1stc2  23398  1stcrest  23409  1stcelcls  23417  llyi  23430  nllyi  23431  subislly  23437  lly1stc  23452  txcnp  23576  txcnmpt  23580  hausdiag  23601  kqcldsat  23689  isfbas2  23791  isfil2  23812  fbasfip  23824  elfg  23827  filconn  23839  rnelfmlem  23908  rnelfm  23909  fmfnfmlem2  23911  fmfnfmlem4  23913  fmfnfm  23914  flimrest  23939  hauspwpwf1  23943  fclsrest  23980  alexsubALTlem2  24004  alexsubALTlem3  24005  alexsubALTlem4  24006  alexsubALT  24007  istmd  24030  istgp  24033  tsmssubm  24099  tsmssplit  24108  istrg  24120  istdrg  24122  istlm  24141  ustfilxp  24169  utoptop  24190  utop3cls  24207  bldisj  24354  blin  24377  blres  24387  lpbl  24459  metrest  24480  restmetu  24526  isngp  24552  isnlm  24631  isnmhm  24702  xrtgioo  24763  xrsmopn  24769  icccmplem2  24780  reconnlem2  24784  icoopnst  24904  iocopnst  24905  bndth  24925  zclmncvs  25116  isncvsngp  25117  ncvsprp  25120  ncvsm1  25122  ncvsdif  25123  ncvspi  25124  ncvs1  25125  ncvspds  25129  iscph  25138  tcphcph  25205  cfilfcls  25242  cmetcaulem  25256  isbn  25306  cldcss2  25410  hlhil  25411  ovolfcl  25435  ovolicc2lem2  25487  ovolicc2  25491  shftmbl  25507  volfiniun  25516  mbfmax  25618  mbfimaopnlem  25624  mbfaddlem  25629  i1faddlem  25662  i1fmullem  25663  i1fres  25674  itg1climres  25683  mbfi1fseqlem4  25687  itg2splitlem  25717  itg2split  25718  itgresr  25748  ellimc2  25846  ellimc3  25848  limcun  25864  dvreslem  25878  dvne0  25984  itgsubstlem  26023  ig1pval3  26151  aaliou2  26316  aaliou2b  26317  pilem1  26429  rlimcnp2  26944  fsumharmonic  26990  ppisval2  27083  prmorcht  27156  fsumvma2  27193  pclogsum  27194  vmasum  27195  chpchtsum  27198  chpub  27199  rpvmasum2  27491  madeval2  27841  tglineineq  28727  trlsegvdeg  30314  frgrncvvdeqlem7  30392  frgrncvvdeqlem9  30394  minvecolem1  30962  minvecolem4a  30965  minvecolem4b  30966  minvecolem4  30968  h2hcau  31067  axhcompl-zf  31086  hhcmpl  31288  hhcms  31291  ocin  31384  ocnel  31386  shmodsi  31477  pjhthlem2  31480  omlsilem  31490  pjoc1i  31519  spansnm0i  31738  nonbooli  31739  5oalem7  31748  3oalem3  31752  pjssmii  31769  mayete3i  31816  nmcopex  32117  nmcoplb  32118  lncnopbd  32125  nmcfnex  32141  nmcfnlb  32142  riesz4  32152  riesz1  32153  riesz2  32154  cnlnadjlem3  32157  cnlnadjlem5  32159  cnlnadjlem9  32163  cnlnadjeu  32166  rnbra  32195  pjimai  32264  pjclem4a  32286  pj3lem1  32294  jpi  32358  sumdmdii  32503  sumdmdlem  32506  sumdmdlem2  32507  cdjreui  32520  cdj3lem1  32522  iunin1f  32644  disjorf  32666  ofpreima  32755  1stpreima  32797  2ndpreima  32798  iocinioc2  32870  ssnnssfz  32878  cntzun  33173  kerunit  33418  prmidl0  33543  ressply1mon1p  33661  ccfldextdgrr  33850  crefdf  34026  cmpcref  34028  cmppcmp  34036  cnre2csqima  34089  ordtconnlem1  34102  lmxrge0  34130  isrrext  34178  esum0  34227  esumcst  34241  esumpcvgval  34256  esumcvg  34264  measvuni  34392  eulerpartlemt0  34547  eulerpartlemr  34552  eulerpartlemgf  34557  eulerpartlemgs2  34558  eulerpartlemn  34559  fiblem  34576  oddprm2  34833  bnj1173  35178  bnj1174  35179  bnj1279  35194  elima4  35992  dfon2lem4  36000  ellimits  36124  dfom5b  36126  brapply  36152  brcap  36154  dfrecs2  36166  dfrdg4  36167  finminlem  36534  neibastop2lem  36576  neibastop2  36577  neifg  36587  tailfb  36593  onsucconni  36653  onintopssconn  36656  onsucsuccmpi  36659  limsucncmpi  36661  onint1  36665  bj-inrab  37175  bj-rcleqf  37273  bj-restuni  37350  bj-opelresdm  37400  bj-idres  37415  bj-opelidres  37416  bj-eldiag  37431  bj-eldiag2  37432  bj-ccinftydisj  37468  taupilem3  37574  isbasisrelowllem1  37610  isbasisrelowllem2  37611  nlpineqsn  37663  fvineqsneu  37666  ptrest  37870  poimirlem29  37900  poimirlem30  37901  mblfinlem2  37909  mbfposadd  37918  itg2gt0cn  37926  dvasin  37955  inixp  37979  0totbnd  38024  sstotbnd3  38027  heibor1lem  38060  heibor1  38061  heiborlem6  38067  isexid2  38106  smgrpismgmOLD  38113  issmgrpOLD  38114  mndoissmgrpOLD  38119  ismndo  38123  exidresid  38130  rngo1cl  38190  isfld2  38256  ineleq  38605  refressn  38784  eleccossin  38824  elrefsymrelsrel  38906  dfeldisj3  39062  eldisjdmqsim  39068  disjlem14  39152  prtlem14  39250  lshpdisj  39363  lkrin  39540  ishlat1  39728  pmodlem2  40223  pclfinN  40276  pclcmpatN  40277  osumcllem4N  40335  pexmidlem1N  40346  dihmeetlem1N  41666  dihglblem5apreN  41667  dihmeetlem4preN  41682  dihmeetlem13N  41695  dochnel2  41768  lcdlss  41995  mapd1o  42024  baerlem3lem2  42086  baerlem5alem2  42087  baerlem5blem2  42088  redvmptabs  42730  cmpfiiin  43054  mrefg2  43064  fz1eqin  43126  fnwe2lem2  43408  islmodfg  43426  islssfg2  43428  lnr2i  43473  rp-fakeinunass  43871  fiinfi  43929  elinintab  43931  elinintrab  43933  elinlem  43954  cnvcnvintabd  43956  ntrneikb  44450  ntrneik3  44452  ntrneik13  44454  ismnushort  44657  radcnvrat  44670  nzin  44674  onfrALTlem2  44902  onfrALTlem2VD  45244  relpmin  45308  pwclaxpow  45340  dfac5prim  45346  modelac8prim  45348  permac8prim  45370  iooabslt  45859  iccintsng  45883  lptioo2cn  46003  lptioo1cn  46004  cncfuni  46244  icccncfext  46245  stoweidlem44  46402  fourierdlem42  46507  fourierdlem80  46544  sge00  46734  eldmressn  47397  afvres  47532  afv2res  47599  prproropf1olem0  47862  31prm  47957  rngccatidALTV  48632  rhmsubcALTVlem3  48643  funcringcsetcALTV2lem7  48656  ringccatidALTV  48666  ringcbasbasALTV  48672  funcringcsetclem7ALTV  48679  fldhmsubcALTV  48693  ssnn0ssfz  48709  elbigo2  48912  itsclinecirc0in  49135  resinsnALT  49232  opndisj  49262  clddisj  49263  i0oii  49279  io1ii  49280