Theorem elun 3370

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 2833	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 2833	. . 3 |- ( A e. B -> A e. _V )
3		elex 2833	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 728	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2301	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2301	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
7	5, 6	orbi12d 805	. . 3 |- ( x = A -> ( ( x e. B \/ x e. C ) <-> ( A e. B \/ A e. C ) ) )
8		df-un 3224	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 2973	. 2 |- ( A e. _V -> ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) ) )
10	1, 4, 9	pm5.21nii 716	1 |- ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) )

Syntax hints:   <-> wb 105   \/ wo 720   = wceq 1402   e. wcel 2209   _Vcvv 2821   u. cun 3218

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224

This theorem is referenced by:  uneqri  3371  uncom  3373  uneq1  3376  unass  3386  ssun1  3392  unss1  3398  ssequn1  3399  unss  3403  rexun  3409  ralunb  3410  unssdif  3466  unssin  3470  inssun  3471  indi  3478  undi  3479  difundi  3483  difindiss  3485  undif3ss  3492  symdifxor  3497  rabun2  3512  reuun2  3516  undif4  3586  ssundifim  3608  dcun  3634  dfpr2  3724  eltpg  3750  pwprss  3926  pwtpss  3927  uniun  3949  intun  3996  iunun  4086  iunxun  4087  iinuniss  4090  brun  4177  undifexmid  4325  exmidundif  4338  exmidundifim  4339  exmid1stab  4340  pwunss  4423  elsuci  4543  elsucg  4544  elsuc2g  4545  ordsucim  4642  sucprcreg  4691  opthprc  4821  xpundi  4826  xpundir  4827  funun  5417  mptun  5510  unpreima  5824  reldmtpos  6514  dftpos4  6524  tpostpos  6525  elssdc  7199  onunsnss  7214  unfidisj  7219  undifdcss  7220  fidcenumlemrks  7260  djulclb  7385  eldju  7398  eldju2ndl  7402  eldju2ndr  7403  ctssdccl  7441  pw1nel3  7580  sucpw1nel3  7582  elnn0  9544  un0addcl  9575  un0mulcl  9576  elxnn0  9611  ltxr  10156  elxr  10157  fzsplit2  10433  fzsplit3  10436  elfzp1  10457  uzsplit  10477  elfzp12  10484  fz01or  10496  fzosplit  10564  fzouzsplit  10566  elfzonlteqm1  10606  fzosplitsni  10632  hashinfuni  11194  hashennnuni  11196  hashunlem  11222  hashf1lem2  11264  zfz1isolemiso  11269  ccatrn  11355  cats1un  11471  summodclem3  12125  fsumsplit  12152  fsumsplitsn  12155  sumsplitdc  12177  fprodsplitdc  12341  fprodsplit  12342  fprodunsn  12349  fprodsplitsn  12378  nnnn0modprm0  13012  prm23lt5  13020  gsumfsum  14895  reopnap  15570  plyaddlem1  15771  plymullem1  15772  plycoeid3  15781  plycj  15785  lgsdir2  16066  2lgslem3  16134  2lgsoddprmlem3  16144  vtxdfifiun  16452  djulclALT  16743  djurclALT  16744  bj-charfun  16747  bj-nntrans  16891  bj-nnelirr  16893