Theorem elun 3268

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 2741	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 2741	. . 3 |- ( A e. B -> A e. _V )
3		elex 2741	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 711	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2233	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2233	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
7	5, 6	orbi12d 788	. . 3 |- ( x = A -> ( ( x e. B \/ x e. C ) <-> ( A e. B \/ A e. C ) ) )
8		df-un 3125	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 2877	. 2 |- ( A e. _V -> ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) ) )
10	1, 4, 9	pm5.21nii 699	1 |- ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) )

Syntax hints:   <-> wb 104   \/ wo 703   = wceq 1348   e. wcel 2141   _Vcvv 2730   u. cun 3119

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125

This theorem is referenced by:  uneqri  3269  uncom  3271  uneq1  3274  unass  3284  ssun1  3290  unss1  3296  ssequn1  3297  unss  3301  rexun  3307  ralunb  3308  unssdif  3362  unssin  3366  inssun  3367  indi  3374  undi  3375  difundi  3379  difindiss  3381  undif3ss  3388  symdifxor  3393  rabun2  3406  reuun2  3410  undif4  3477  ssundifim  3498  dcun  3525  dfpr2  3602  eltpg  3628  pwprss  3792  pwtpss  3793  uniun  3815  intun  3862  iunun  3951  iunxun  3952  iinuniss  3955  brun  4040  undifexmid  4179  exmidundif  4192  exmidundifim  4193  pwunss  4268  elsuci  4388  elsucg  4389  elsuc2g  4390  ordsucim  4484  sucprcreg  4533  opthprc  4662  xpundi  4667  xpundir  4668  funun  5242  mptun  5329  unpreima  5621  reldmtpos  6232  dftpos4  6242  tpostpos  6243  onunsnss  6894  unfidisj  6899  undifdcss  6900  fidcenumlemrks  6930  djulclb  7032  eldju  7045  eldju2ndl  7049  eldju2ndr  7050  ctssdccl  7088  pw1nel3  7208  sucpw1nel3  7210  elnn0  9137  un0addcl  9168  un0mulcl  9169  elxnn0  9200  ltxr  9732  elxr  9733  fzsplit2  10006  elfzp1  10028  uzsplit  10048  elfzp12  10055  fz01or  10067  fzosplit  10133  fzouzsplit  10135  elfzonlteqm1  10166  fzosplitsni  10191  hashinfuni  10711  hashennnuni  10713  hashunlem  10739  zfz1isolemiso  10774  summodclem3  11343  fsumsplit  11370  fsumsplitsn  11373  sumsplitdc  11395  fprodsplitdc  11559  fprodsplit  11560  fprodunsn  11567  fprodsplitsn  11596  nnnn0modprm0  12209  prm23lt5  12217  reopnap  13332  lgsdir2  13728  djulclALT  13836  djurclALT  13837  bj-charfun  13842  bj-nntrans  13986  bj-nnelirr  13988  exmid1stab  14033