Theorem elun 3359

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 2824	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 2824	. . 3 |- ( A e. B -> A e. _V )
3		elex 2824	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 724	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2295	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2295	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
7	5, 6	orbi12d 801	. . 3 |- ( x = A -> ( ( x e. B \/ x e. C ) <-> ( A e. B \/ A e. C ) ) )
8		df-un 3214	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 2963	. 2 |- ( A e. _V -> ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) ) )
10	1, 4, 9	pm5.21nii 712	1 |- ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) )

Syntax hints:   <-> wb 105   \/ wo 716   = wceq 1398   e. wcel 2203   _Vcvv 2812   u. cun 3208

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2814  df-un 3214

This theorem is referenced by:  uneqri  3360  uncom  3362  uneq1  3365  unass  3375  ssun1  3381  unss1  3387  ssequn1  3388  unss  3392  rexun  3398  ralunb  3399  unssdif  3455  unssin  3459  inssun  3460  indi  3467  undi  3468  difundi  3472  difindiss  3474  undif3ss  3481  symdifxor  3486  rabun2  3499  reuun2  3503  undif4  3570  ssundifim  3592  dcun  3618  dfpr2  3707  eltpg  3733  pwprss  3909  pwtpss  3910  uniun  3932  intun  3979  iunun  4069  iunxun  4070  iinuniss  4073  brun  4160  undifexmid  4305  exmidundif  4318  exmidundifim  4319  exmid1stab  4320  pwunss  4403  elsuci  4523  elsucg  4524  elsuc2g  4525  ordsucim  4621  sucprcreg  4670  opthprc  4800  xpundi  4805  xpundir  4806  funun  5396  mptun  5489  unpreima  5801  reldmtpos  6483  dftpos4  6493  tpostpos  6494  elssdc  7161  onunsnss  7176  unfidisj  7181  undifdcss  7182  fidcenumlemrks  7222  djulclb  7345  eldju  7358  eldju2ndl  7362  eldju2ndr  7363  ctssdccl  7401  pw1nel3  7540  sucpw1nel3  7542  elnn0  9497  un0addcl  9528  un0mulcl  9529  elxnn0  9564  ltxr  10107  elxr  10108  fzsplit2  10383  elfzp1  10405  uzsplit  10425  elfzp12  10432  fz01or  10444  fzosplit  10512  fzouzsplit  10514  elfzonlteqm1  10554  fzosplitsni  10580  hashinfuni  11138  hashennnuni  11140  hashunlem  11166  zfz1isolemiso  11207  ccatrn  11293  cats1un  11409  summodclem3  12062  fsumsplit  12089  fsumsplitsn  12092  sumsplitdc  12114  fprodsplitdc  12278  fprodsplit  12279  fprodunsn  12286  fprodsplitsn  12315  nnnn0modprm0  12949  prm23lt5  12957  reopnap  15403  plyaddlem1  15604  plymullem1  15605  plycoeid3  15614  plycj  15618  lgsdir2  15898  2lgslem3  15966  2lgsoddprmlem3  15976  vtxdfifiun  16284  djulclALT  16565  djurclALT  16566  bj-charfun  16569  bj-nntrans  16713  bj-nnelirr  16715