Theorem elun 3346

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 2812	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 2812	. . 3 |- ( A e. B -> A e. _V )
3		elex 2812	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 721	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2292	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2292	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
7	5, 6	orbi12d 798	. . 3 |- ( x = A -> ( ( x e. B \/ x e. C ) <-> ( A e. B \/ A e. C ) ) )
8		df-un 3202	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 2951	. 2 |- ( A e. _V -> ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) ) )
10	1, 4, 9	pm5.21nii 709	1 |- ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) )

Syntax hints:   <-> wb 105   \/ wo 713   = wceq 1395   e. wcel 2200   _Vcvv 2800   u. cun 3196

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-un 3202

This theorem is referenced by:  uneqri  3347  uncom  3349  uneq1  3352  unass  3362  ssun1  3368  unss1  3374  ssequn1  3375  unss  3379  rexun  3385  ralunb  3386  unssdif  3440  unssin  3444  inssun  3445  indi  3452  undi  3453  difundi  3457  difindiss  3459  undif3ss  3466  symdifxor  3471  rabun2  3484  reuun2  3488  undif4  3555  ssundifim  3576  dcun  3602  dfpr2  3686  eltpg  3712  pwprss  3887  pwtpss  3888  uniun  3910  intun  3957  iunun  4047  iunxun  4048  iinuniss  4051  brun  4138  undifexmid  4281  exmidundif  4294  exmidundifim  4295  exmid1stab  4296  pwunss  4378  elsuci  4498  elsucg  4499  elsuc2g  4500  ordsucim  4596  sucprcreg  4645  opthprc  4775  xpundi  4780  xpundir  4781  funun  5368  mptun  5461  unpreima  5768  reldmtpos  6414  dftpos4  6424  tpostpos  6425  elssdc  7087  onunsnss  7102  unfidisj  7107  undifdcss  7108  fidcenumlemrks  7143  djulclb  7245  eldju  7258  eldju2ndl  7262  eldju2ndr  7263  ctssdccl  7301  pw1nel3  7439  sucpw1nel3  7441  elnn0  9394  un0addcl  9425  un0mulcl  9426  elxnn0  9457  ltxr  10000  elxr  10001  fzsplit2  10275  elfzp1  10297  uzsplit  10317  elfzp12  10324  fz01or  10336  fzosplit  10404  fzouzsplit  10406  elfzonlteqm1  10445  fzosplitsni  10471  hashinfuni  11029  hashennnuni  11031  hashunlem  11057  zfz1isolemiso  11093  ccatrn  11176  cats1un  11292  summodclem3  11931  fsumsplit  11958  fsumsplitsn  11961  sumsplitdc  11983  fprodsplitdc  12147  fprodsplit  12148  fprodunsn  12155  fprodsplitsn  12184  nnnn0modprm0  12818  prm23lt5  12826  reopnap  15260  plyaddlem1  15461  plymullem1  15462  plycoeid3  15471  plycj  15475  lgsdir2  15752  2lgslem3  15820  2lgsoddprmlem3  15830  vtxdfifiun  16103  djulclALT  16333  djurclALT  16334  bj-charfun  16338  bj-nntrans  16482  bj-nnelirr  16484