Theorem elun 3323

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 2789	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 2789	. . 3 |- ( A e. B -> A e. _V )
3		elex 2789	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 718	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2270	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2270	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
7	5, 6	orbi12d 795	. . 3 |- ( x = A -> ( ( x e. B \/ x e. C ) <-> ( A e. B \/ A e. C ) ) )
8		df-un 3179	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 2928	. 2 |- ( A e. _V -> ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) ) )
10	1, 4, 9	pm5.21nii 706	1 |- ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) )

Syntax hints:   <-> wb 105   \/ wo 710   = wceq 1373   e. wcel 2178   _Vcvv 2777   u. cun 3173

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2779  df-un 3179

This theorem is referenced by:  uneqri  3324  uncom  3326  uneq1  3329  unass  3339  ssun1  3345  unss1  3351  ssequn1  3352  unss  3356  rexun  3362  ralunb  3363  unssdif  3417  unssin  3421  inssun  3422  indi  3429  undi  3430  difundi  3434  difindiss  3436  undif3ss  3443  symdifxor  3448  rabun2  3461  reuun2  3465  undif4  3532  ssundifim  3553  dcun  3579  dfpr2  3663  eltpg  3689  pwprss  3861  pwtpss  3862  uniun  3884  intun  3931  iunun  4021  iunxun  4022  iinuniss  4025  brun  4112  undifexmid  4254  exmidundif  4267  exmidundifim  4268  exmid1stab  4269  pwunss  4349  elsuci  4469  elsucg  4470  elsuc2g  4471  ordsucim  4567  sucprcreg  4616  opthprc  4745  xpundi  4750  xpundir  4751  funun  5335  mptun  5428  unpreima  5730  reldmtpos  6364  dftpos4  6374  tpostpos  6375  onunsnss  7042  unfidisj  7047  undifdcss  7048  fidcenumlemrks  7083  djulclb  7185  eldju  7198  eldju2ndl  7202  eldju2ndr  7203  ctssdccl  7241  pw1nel3  7379  sucpw1nel3  7381  elnn0  9334  un0addcl  9365  un0mulcl  9366  elxnn0  9397  ltxr  9934  elxr  9935  fzsplit2  10209  elfzp1  10231  uzsplit  10251  elfzp12  10258  fz01or  10270  fzosplit  10338  fzouzsplit  10340  elfzonlteqm1  10378  fzosplitsni  10403  hashinfuni  10961  hashennnuni  10963  hashunlem  10988  zfz1isolemiso  11023  ccatrn  11105  cats1un  11214  summodclem3  11852  fsumsplit  11879  fsumsplitsn  11882  sumsplitdc  11904  fprodsplitdc  12068  fprodsplit  12069  fprodunsn  12076  fprodsplitsn  12105  nnnn0modprm0  12739  prm23lt5  12747  reopnap  15179  plyaddlem1  15380  plymullem1  15381  plycoeid3  15390  plycj  15394  lgsdir2  15671  2lgslem3  15739  2lgsoddprmlem3  15749  djulclALT  16045  djurclALT  16046  bj-charfun  16050  bj-nntrans  16194  bj-nnelirr  16196