Theorem elun 2176

Description: Expansion of membership in class union. Theorem 12 of [Suppes] p. 25.

Assertion

Ref	Expression
elun	|- (A e. (B u. C) <-> (A e. B \/ A e. C))

Proof of Theorem elun

Step	Hyp	Ref	Expression
1		elisset 1820	. 2 |- (A e. (B u. C) -> A e. V)
2		elisset 1820	. . 3 |- (A e. B -> A e. V)
3		elisset 1820	. . 3 |- (A e. C -> A e. V)
4	2, 3	jaoi 341	. 2 |- ((A e. B \/ A e. C) -> A e. V)
5		eleq1 1537	. . . 4 |- (x = A -> (x e. B <-> A e. B))
6		eleq1 1537	. . . 4 |- (x = A -> (x e. C <-> A e. C))
7	5, 6	orbi12d 629	. . 3 |- (x = A -> ((x e. B \/ x e. C) <-> (A e. B \/ A e. C)))
8		df-un 2053	. . 3 |- (B u. C) = {x | (x e. B \/ x e. C)}
9	7, 8	elab2g 1903	. 2 |- (A e. V -> (A e. (B u. C) <-> (A e. B \/ A e. C)))
10	1, 4, 9	pm5.21nii 681	1 |- (A e. (B u. C) <-> (A e. B \/ A e. C))

Syntax hints:   <-> wb 146   \/ wo 222   = wceq 958   e. wcel 960  Vcvv 1814   u. cun 2048

This theorem is referenced by:  uneqri 2177  uncom 2179  uneq1 2180  hbun 2189  unass 2190  ssun1 2196  unss1 2202  unss 2207  dfun2 2246  indi 2254  undi 2255  unineq 2258  symdif2 2269  unab 2270  reuun2 2281  undif4 2329  disjssun 2330  ssundif 2348  dfpr2 2426  eltp 2443  uniun 2523  intun 2566  iinun2 2614  iunun 2618  iunxun 2619  iinuni 2620  iununi 2621  pwunss 2832  pwssun 2833  pwundif 2834  elpwunsn 2918  elsuci 3041  elsucg 3042  elsuc2g 3043  sucid 3057  suceloni 3068  ordsucun 3088  opthprc 3227  xpundi 3231  xpundir 3232  dmun 3323  cnvun 3461  funun 3560  fopabap 3847  erref 4281  brdom2 4394  sucprcreg 4609  rankun 4701  kmlem2 4776  unxpdomlem 4854  iscard3 4899  pnfxr 5505  mnfxr 5506  ltxrt 5507  elxr 5547  xrsupexmnf 6076  xrinfmexpnf 6077  supxrun 6087  elnn0 6103  icounlem 6413  snunioolem 6415  ioojoint 6417  clslp 7745  islpi 7746  metelcls 7962  efif1lem5 8729  efif1lem7 8731  shunss 9332  atoml 10304  atoml2 10305  cdrci 10480

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-un 2053

Copyright terms: Public domain