Theorem elun 2173

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 1817	. 2 |- (A e. (B u. C) -> A e. V)
2		elisset 1817	. . 3 |- (A e. B -> A e. V)
3		elisset 1817	. . 3 |- (A e. C -> A e. V)
4	2, 3	jaoi 341	. 2 |- ((A e. B \/ A e. C) -> A e. V)
5		eleq1 1534	. . . 4 |- (x = A -> (x e. B <-> A e. B))
6		eleq1 1534	. . . 4 |- (x = A -> (x e. C <-> A e. C))
7	5, 6	orbi12d 627	. . 3 |- (x = A -> ((x e. B \/ x e. C) <-> (A e. B \/ A e. C)))
8		df-un 2050	. . 3 |- (B u. C) = {x | (x e. B \/ x e. C)}
9	7, 8	elab2g 1900	. 2 |- (A e. V -> (A e. (B u. C) <-> (A e. B \/ A e. C)))
10	1, 4, 9	pm5.21nii 679	1 |- (A e. (B u. C) <-> (A e. B \/ A e. C))

Syntax hints:   <-> wb 146   \/ wo 222   = wceq 956   e. wcel 958  Vcvv 1811   u. cun 2045

This theorem is referenced by:  uneqri 2174  uncom 2176  uneq1 2177  hbun 2186  unass 2187  ssun1 2193  unss1 2199  unss 2204  dfun2 2243  indi 2251  undi 2252  unineq 2255  symdif2 2266  unab 2267  reuun2 2278  undif4 2325  disjssun 2326  ssundif 2344  dfpr2 2422  eltp 2439  uniun 2519  intun 2562  iinun2 2609  iunun 2613  iunxun 2614  iinuni 2615  iununi 2616  pwunss 2826  pwssun 2827  pwundif 2828  elpwunsn 2912  elsuci 3035  elsucg 3036  elsuc2g 3037  sucid 3051  suceloni 3062  ordsucun 3082  opthprc 3221  xpundi 3225  xpundir 3226  dmun 3317  cnvun 3455  funun 3554  fopabap 3841  erref 4275  brdom2 4388  sucprcreg 4600  rankun 4691  kmlem2 4766  unxpdomlem 4843  iscard3 4888  pnfxr 5493  mnfxr 5494  ltxrt 5495  elxr 5535  xrsupexmnf 6074  xrinfmexpnf 6075  supxrun 6085  elnn0 6101  icounlem 6412  snunioolem 6414  ioojoint 6416  clslp 7748  islpi 7749  metelcls 7965  efif1lem5 8734  efif1lem7 8736  shunss 9337  atoml 10309  atoml2 10310  cdrci 10494

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-un 2050

Copyright terms: Public domain