Theorem elun 3360

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 2825	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 2825	. . 3 |- ( A e. B -> A e. _V )
3		elex 2825	. . 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 3215	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 2964	. 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 2813   u. cun 3209

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 2815  df-un 3215

This theorem is referenced by:  uneqri  3361  uncom  3363  uneq1  3366  unass  3376  ssun1  3382  unss1  3388  ssequn1  3389  unss  3393  rexun  3399  ralunb  3400  unssdif  3456  unssin  3460  inssun  3461  indi  3468  undi  3469  difundi  3473  difindiss  3475  undif3ss  3482  symdifxor  3487  rabun2  3500  reuun2  3504  undif4  3571  ssundifim  3593  dcun  3619  dfpr2  3708  eltpg  3734  pwprss  3910  pwtpss  3911  uniun  3933  intun  3980  iunun  4070  iunxun  4071  iinuniss  4074  brun  4161  undifexmid  4306  exmidundif  4319  exmidundifim  4320  exmid1stab  4321  pwunss  4404  elsuci  4524  elsucg  4525  elsuc2g  4526  ordsucim  4622  sucprcreg  4671  opthprc  4801  xpundi  4806  xpundir  4807  funun  5397  mptun  5490  unpreima  5802  reldmtpos  6484  dftpos4  6494  tpostpos  6495  elssdc  7162  onunsnss  7177  unfidisj  7182  undifdcss  7183  fidcenumlemrks  7223  djulclb  7346  eldju  7359  eldju2ndl  7363  eldju2ndr  7364  ctssdccl  7402  pw1nel3  7541  sucpw1nel3  7543  elnn0  9498  un0addcl  9529  un0mulcl  9530  elxnn0  9565  ltxr  10108  elxr  10109  fzsplit2  10384  elfzp1  10406  uzsplit  10426  elfzp12  10433  fz01or  10445  fzosplit  10513  fzouzsplit  10515  elfzonlteqm1  10555  fzosplitsni  10581  hashinfuni  11140  hashennnuni  11142  hashunlem  11168  zfz1isolemiso  11211  ccatrn  11297  cats1un  11413  summodclem3  12066  fsumsplit  12093  fsumsplitsn  12096  sumsplitdc  12118  fprodsplitdc  12282  fprodsplit  12283  fprodunsn  12290  fprodsplitsn  12319  nnnn0modprm0  12953  prm23lt5  12961  reopnap  15411  plyaddlem1  15612  plymullem1  15613  plycoeid3  15622  plycj  15626  lgsdir2  15906  2lgslem3  15974  2lgsoddprmlem3  15984  vtxdfifiun  16292  djulclALT  16573  djurclALT  16574  bj-charfun  16577  bj-nntrans  16721  bj-nnelirr  16723