Theorem elin 2999

Description: Expansion of membership in an intersection of two classes. Theorem 12 of [Suppes] p. 25.

Assertion

Ref	Expression
elin	|- (A e. (B i^i C) <-> (A e. B /\ A e. C))

Proof of Theorem elin

Step	Hyp	Ref	Expression
1		elisset 2547	. 2 |- (A e. (B i^i C) -> A e. _V)
2		elisset 2547	. . 3 |- (A e. C -> A e. _V)
3	2	adantl 448	. 2 |- ((A e. B /\ A e. C) -> A e. _V)
4		eleq1 2204	. . . 4 |- (x = A -> (x e. B <-> A e. B))
5		eleq1 2204	. . . 4 |- (x = A -> (x e. C <-> A e. C))
6	4, 5	anbi12d 763	. . 3 |- (x = A -> ((x e. B /\ x e. C) <-> (A e. B /\ A e. C)))
7		df-in 2834	. . 3 |- (B i^i C) = {x | (x e. B /\ x e. C)}
8	6, 7	elab2g 2647	. 2 |- (A e. _V -> (A e. (B i^i C) <-> (A e. B /\ A e. C)))
9	1, 3, 8	pm5.21nii 1005	1 |- (A e. (B i^i C) <-> (A e. B /\ A e. C))

Syntax hints:   <-> wb 219   /\ wa 337   = wceq 1586   e. wcel 1588  _Vcvv 2538   i^i cin 2826

This theorem is referenced by:  incom 3000  ineqri 3001  ineq1 3002  hbin 3012  inass 3016  inss1 3026  ssin 3028  ssrin 3030  dfss4 3038  dfin2 3040  difin 3041  indi 3049  undi 3050  unineq 3053  indifdir 3059  difin2 3064  inrab2 3074  inelcm 3131  difin0ss 3140  inssdif0 3141  inundif 3151  uniin 3386  intun 3430  intpr 3431  iunin2 3490  iinxprg 3496  brin 3559  trin 3589  inex1 3619  inuni 3638  frirr 3789  wefrc 3806  ordtri3or 3843  ordpwsuc 4039  brinxp2 4190  inopab 4238  inxp 4239  dmin 4290  opelres 4345  intasym 4422  asymref 4423  cnvin 4433  dminss 4439  imainss 4440  ssrnres 4460  dfco2a 4496  2elresin 4623  nfvres 4791  inpreima 4871  respreima 4872  ressnop0 4901  funfvima 4920  isomin 4972  isoini 4973  smores 5263  tfrlem5 5287  tz7.48-2OLD 5330  mapval2 5555  pw2en 5671  sbthcl 5688  ssenen 5789  onfin2 5806  fipreima 5879  inf3lem2 5952  zfregs 5990  onfrALTlem2 6080  cp 6091  bnd2 6093  aceq5lem1 6189  aceq5lem5 6193  aceq5 6194  onacda 6259  kmlem3 6339  kmlem14 6350  kmlem15 6351  ltpiord 6533  ltxr 6854  clm4i 8736  infpss 9237  isbasis2g 9732  tgval2 9738  tgcl 9745  tgss3 9759  basgen 9761  opnin 10012  lmss 10097  isphg 10686  ishl 10807  axgroth4 11010  grothprim 11012  istoset 11041  uptx 11061  subtopmetlem 11093  subtopmet 11094  isfbas2 11101  filintf 11112  elfg 11122  sfvlim 11134  cncomp 11169  fintopcomp 11171  usinuniop 11179  isexid2 11210  smgrpismgm 11217  smgrpisass 11218  issmgrp 11219  mndissmgrp 11224  mndisexid 11225  mndmgmid 11227  ismnd 11228  ismnd2 11230  ring1cl 11253  axhcompl 11338  hhcmpl 11538  ocin 11636  ocnel 11637  chocunii 11639  projlemHIL 11685  omlsilem 11711  pjoc1i 11731  shmodsi 11829  spansnm0i 12062  nonbooli 12063  5oalem1 12066  5oalem2 12067  5oalem4 12069  5oalem5 12070  5oalem7 12072  3oalem2 12075  3oalem3 12076  pjssmii 12093  mayete3i 12140  mayete3OLDi 12141  nmcopex 12428  nmcoplb 12429  lncnopbd 12435  nmcfnex 12457  nmcfnlb 12458  riesz4 12466  riesz1 12467  riesz2 12468  cnlnadjlem3 12471  cnlnadjlem4 12472  cnlnadjlem5 12473  cnlnadjlem9 12477  cnlnadjeu 12480  rnbra 12509  pjimai 12579  dfpjop 12586  pjclem4a 12602  pjclem4 12603  pj3lem1 12610  pj3si 12611  jpi 12673  sumdmdii 12818  sumdmdlem 12821  sumdmdlem2 12822  cdjreui 12835  cdj3lem1 12837  bnj521 13295  bnj1153 13717  bnj1164 13727  bnj1269 13798  bnj1380 13868  bnj1172 14211  bnj1173 14212  indifdiOLD 14453  dfon2lem4 14486  elpredim 14529  elpred 14530  elpredg 14531  predel 14536  wfrlem5 14614  frrlem5 14638  sltres 14670  axfelem18 14716  ellimits 14771  dfiota3 14777  dfoprab4spop 15047  uninqs 15048  splint 15060  omslim 15132  inposet 15359  pospos 15374  tostos 15376  isdir2 15379  ablcomgrp 15437  expus 15461  symgfo 15465  fprodsub 15477  isfld 15528  fldi 15529  zrfld 15537  zintdom 15540  unint2t 15619  intcont 15679  sinempcomp 15731  indcomp 15733  topunfincomp 15735  stfincomp 15737  bwt2 15738  vtarsuelt 16082  partarelt2 16084  eltintpar 16086  inttaror 16087  inttarcar 16088  carinttar 16089  cardtar 16091  cartarlim 16092  elcarelcl 16093  isplibg 16129  cnvresima 16183  ioodisj 16188  finminlem 16191  subntr 16249  compsublem 16254  compsub 16255  cptclsscpt 16256  uncomp 16257  hscptsscld 16258  compfipin0lem 16259  compfipin0 16260  alexsublem2 16262  alexsublem3 16263  alexsublem4 16264  alexsub 16265  dfcon2 16266  cnconn 16268  reconnlem1 16270  reconnlem3 16272  reconnlem4 16273  reconnlem5 16274  is1stc3 16293  isfne2 16305  lfinpfin 16337  comppfsc 16341  neifg 16383  ufprim 16393  filssufillem 16394  filcon 16404  rnelfmlem 16416  rnelfm 16417  fmfnfmlem2 16419  fmfnfmlem4 16421  fmfnfm 16422  tailfb 16463  difin2OLD 16500  inpreimaOLD 16506  respreimaOLD 16508  inixp 16546  fipreimaOLD 16580  fzdisj 16617  blssp 16668  icoopnst 16700  iocopnst 16701  cnresima 16715  sstotbnd 16760  totbndss 16761  heiborlem1 16779  heiborlem10 16788  heiborlem11 16789  heiborlem13 16791  heiborlem18 16796  heiborlem21 16799  heiborlem23 16801  heiborlem32 16810  heiborlem38 16816  heiborlem41 16819  exidresid 16856  iscring 16969  fldcrng 16976  isfld2 16977  isdmn 17026  prtlem14 17101  smoresOLD 17268  onfrALTlem2VD 17547  isolat 17606  ishlat1 17748  issdrng 17891  pmodlem1 18278  pmodlem2 18279  osumcllem4 18372  pexmidlem1 18383

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-ex 1616  df-sb 1816  df-clab 2129  df-cleq 2134  df-clel 2137  df-v 2540  df-in 2834

Copyright terms: Public domain