Theorem elun 3248

Description: Expansion of membership in class union. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 7-Aug-1994.)

Assertion

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

Proof of Theorem elun

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 2723	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 2723	. . 3 |- ( A e. B -> A e. _V )
3		elex 2723	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 706	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2220	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2220	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
7	5, 6	orbi12d 783	. . 3 |- ( x = A -> ( ( x e. B \/ x e. C ) <-> ( A e. B \/ A e. C ) ) )
8		df-un 3106	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 2859	. 2 |- ( A e. _V -> ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) ) )
10	1, 4, 9	pm5.21nii 694	1 |- ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) )

Syntax hints:   <-> wb 104   \/ wo 698   = wceq 1335   e. wcel 2128   _Vcvv 2712   u. cun 3100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-v 2714  df-un 3106

This theorem is referenced by:  uneqri  3249  uncom  3251  uneq1  3254  unass  3264  ssun1  3270  unss1  3276  ssequn1  3277  unss  3281  rexun  3287  ralunb  3288  unssdif  3342  unssin  3346  inssun  3347  indi  3354  undi  3355  difundi  3359  difindiss  3361  undif3ss  3368  symdifxor  3373  rabun2  3386  reuun2  3390  undif4  3456  ssundifim  3477  dcun  3504  dfpr2  3579  eltpg  3604  pwprss  3768  pwtpss  3769  uniun  3791  intun  3838  iunun  3927  iunxun  3928  iinuniss  3931  brun  4015  undifexmid  4153  exmidundif  4166  exmidundifim  4167  pwunss  4242  elsuci  4362  elsucg  4363  elsuc2g  4364  ordsucim  4457  sucprcreg  4506  opthprc  4634  xpundi  4639  xpundir  4640  funun  5211  mptun  5298  unpreima  5589  reldmtpos  6194  dftpos4  6204  tpostpos  6205  onunsnss  6854  unfidisj  6859  undifdcss  6860  fidcenumlemrks  6890  djulclb  6989  eldju  7002  eldju2ndl  7006  eldju2ndr  7007  ctssdccl  7045  pw1nel3  7149  sucpw1nel3  7151  elnn0  9075  un0addcl  9106  un0mulcl  9107  elxnn0  9138  ltxr  9664  elxr  9665  fzsplit2  9934  elfzp1  9956  uzsplit  9976  elfzp12  9983  fz01or  9995  fzosplit  10058  fzouzsplit  10060  elfzonlteqm1  10091  fzosplitsni  10116  hashinfuni  10633  hashennnuni  10635  hashunlem  10660  zfz1isolemiso  10692  summodclem3  11259  fsumsplit  11286  fsumsplitsn  11289  sumsplitdc  11311  fprodsplitdc  11475  fprodsplit  11476  fprodunsn  11483  fprodsplitsn  11512  reopnap  12898  djulclALT  13334  djurclALT  13335  bj-charfun  13341  bj-nntrans  13485  bj-nnelirr  13487  exmid1stab  13532