Theorem elun 3345

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 2811	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 2811	. . 3 |- ( A e. B -> A e. _V )
3		elex 2811	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 721	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2292	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2292	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
7	5, 6	orbi12d 798	. . 3 |- ( x = A -> ( ( x e. B \/ x e. C ) <-> ( A e. B \/ A e. C ) ) )
8		df-un 3201	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 2950	. 2 |- ( A e. _V -> ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) ) )
10	1, 4, 9	pm5.21nii 709	1 |- ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) )

Syntax hints:   <-> wb 105   \/ wo 713   = wceq 1395   e. wcel 2200   _Vcvv 2799   u. cun 3195

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201

This theorem is referenced by:  uneqri  3346  uncom  3348  uneq1  3351  unass  3361  ssun1  3367  unss1  3373  ssequn1  3374  unss  3378  rexun  3384  ralunb  3385  unssdif  3439  unssin  3443  inssun  3444  indi  3451  undi  3452  difundi  3456  difindiss  3458  undif3ss  3465  symdifxor  3470  rabun2  3483  reuun2  3487  undif4  3554  ssundifim  3575  dcun  3601  dfpr2  3685  eltpg  3711  pwprss  3883  pwtpss  3884  uniun  3906  intun  3953  iunun  4043  iunxun  4044  iinuniss  4047  brun  4134  undifexmid  4276  exmidundif  4289  exmidundifim  4290  exmid1stab  4291  pwunss  4373  elsuci  4493  elsucg  4494  elsuc2g  4495  ordsucim  4591  sucprcreg  4640  opthprc  4769  xpundi  4774  xpundir  4775  funun  5361  mptun  5454  unpreima  5759  reldmtpos  6397  dftpos4  6407  tpostpos  6408  onunsnss  7075  unfidisj  7080  undifdcss  7081  fidcenumlemrks  7116  djulclb  7218  eldju  7231  eldju2ndl  7235  eldju2ndr  7236  ctssdccl  7274  pw1nel3  7412  sucpw1nel3  7414  elnn0  9367  un0addcl  9398  un0mulcl  9399  elxnn0  9430  ltxr  9967  elxr  9968  fzsplit2  10242  elfzp1  10264  uzsplit  10284  elfzp12  10291  fz01or  10303  fzosplit  10371  fzouzsplit  10373  elfzonlteqm1  10411  fzosplitsni  10436  hashinfuni  10994  hashennnuni  10996  hashunlem  11021  zfz1isolemiso  11056  ccatrn  11139  cats1un  11248  summodclem3  11886  fsumsplit  11913  fsumsplitsn  11916  sumsplitdc  11938  fprodsplitdc  12102  fprodsplit  12103  fprodunsn  12110  fprodsplitsn  12139  nnnn0modprm0  12773  prm23lt5  12781  reopnap  15214  plyaddlem1  15415  plymullem1  15416  plycoeid3  15425  plycj  15429  lgsdir2  15706  2lgslem3  15774  2lgsoddprmlem3  15784  djulclALT  16123  djurclALT  16124  bj-charfun  16128  bj-nntrans  16272  bj-nnelirr  16274