Theorem elun 3348

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 2814	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 2814	. . 3 |- ( A e. B -> A e. _V )
3		elex 2814	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 723	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2294	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2294	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
7	5, 6	orbi12d 800	. . 3 |- ( x = A -> ( ( x e. B \/ x e. C ) <-> ( A e. B \/ A e. C ) ) )
8		df-un 3204	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 2953	. 2 |- ( A e. _V -> ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) ) )
10	1, 4, 9	pm5.21nii 711	1 |- ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) )

Syntax hints:   <-> wb 105   \/ wo 715   = wceq 1397   e. wcel 2202   _Vcvv 2802   u. cun 3198

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204

This theorem is referenced by:  uneqri  3349  uncom  3351  uneq1  3354  unass  3364  ssun1  3370  unss1  3376  ssequn1  3377  unss  3381  rexun  3387  ralunb  3388  unssdif  3442  unssin  3446  inssun  3447  indi  3454  undi  3455  difundi  3459  difindiss  3461  undif3ss  3468  symdifxor  3473  rabun2  3486  reuun2  3490  undif4  3557  ssundifim  3578  dcun  3604  dfpr2  3688  eltpg  3714  pwprss  3889  pwtpss  3890  uniun  3912  intun  3959  iunun  4049  iunxun  4050  iinuniss  4053  brun  4140  undifexmid  4283  exmidundif  4296  exmidundifim  4297  exmid1stab  4298  pwunss  4380  elsuci  4500  elsucg  4501  elsuc2g  4502  ordsucim  4598  sucprcreg  4647  opthprc  4777  xpundi  4782  xpundir  4783  funun  5371  mptun  5464  unpreima  5772  reldmtpos  6419  dftpos4  6429  tpostpos  6430  elssdc  7094  onunsnss  7109  unfidisj  7114  undifdcss  7115  fidcenumlemrks  7152  djulclb  7254  eldju  7267  eldju2ndl  7271  eldju2ndr  7272  ctssdccl  7310  pw1nel3  7449  sucpw1nel3  7451  elnn0  9404  un0addcl  9435  un0mulcl  9436  elxnn0  9467  ltxr  10010  elxr  10011  fzsplit2  10285  elfzp1  10307  uzsplit  10327  elfzp12  10334  fz01or  10346  fzosplit  10414  fzouzsplit  10416  elfzonlteqm1  10456  fzosplitsni  10482  hashinfuni  11040  hashennnuni  11042  hashunlem  11068  zfz1isolemiso  11104  ccatrn  11190  cats1un  11306  summodclem3  11959  fsumsplit  11986  fsumsplitsn  11989  sumsplitdc  12011  fprodsplitdc  12175  fprodsplit  12176  fprodunsn  12183  fprodsplitsn  12212  nnnn0modprm0  12846  prm23lt5  12854  reopnap  15289  plyaddlem1  15490  plymullem1  15491  plycoeid3  15500  plycj  15504  lgsdir2  15781  2lgslem3  15849  2lgsoddprmlem3  15859  vtxdfifiun  16167  djulclALT  16448  djurclALT  16449  bj-charfun  16453  bj-nntrans  16597  bj-nnelirr  16599