Theorem elun 3350

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 2815	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 2815	. . 3 |- ( A e. B -> A e. _V )
3		elex 2815	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 724	. 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 801	. . 3 |- ( x = A -> ( ( x e. B \/ x e. C ) <-> ( A e. B \/ A e. C ) ) )
8		df-un 3205	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 2954	. 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 2202   _Vcvv 2803   u. cun 3199

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 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-un 3205

This theorem is referenced by:  uneqri  3351  uncom  3353  uneq1  3356  unass  3366  ssun1  3372  unss1  3378  ssequn1  3379  unss  3383  rexun  3389  ralunb  3390  unssdif  3444  unssin  3448  inssun  3449  indi  3456  undi  3457  difundi  3461  difindiss  3463  undif3ss  3470  symdifxor  3475  rabun2  3488  reuun2  3492  undif4  3559  ssundifim  3580  dcun  3606  dfpr2  3692  eltpg  3718  pwprss  3894  pwtpss  3895  uniun  3917  intun  3964  iunun  4054  iunxun  4055  iinuniss  4058  brun  4145  undifexmid  4289  exmidundif  4302  exmidundifim  4303  exmid1stab  4304  pwunss  4386  elsuci  4506  elsucg  4507  elsuc2g  4508  ordsucim  4604  sucprcreg  4653  opthprc  4783  xpundi  4788  xpundir  4789  funun  5378  mptun  5471  unpreima  5780  reldmtpos  6462  dftpos4  6472  tpostpos  6473  elssdc  7137  onunsnss  7152  unfidisj  7157  undifdcss  7158  fidcenumlemrks  7195  djulclb  7297  eldju  7310  eldju2ndl  7314  eldju2ndr  7315  ctssdccl  7353  pw1nel3  7492  sucpw1nel3  7494  elnn0  9446  un0addcl  9477  un0mulcl  9478  elxnn0  9511  ltxr  10054  elxr  10055  fzsplit2  10330  elfzp1  10352  uzsplit  10372  elfzp12  10379  fz01or  10391  fzosplit  10459  fzouzsplit  10461  elfzonlteqm1  10501  fzosplitsni  10527  hashinfuni  11085  hashennnuni  11087  hashunlem  11113  zfz1isolemiso  11149  ccatrn  11235  cats1un  11351  summodclem3  12004  fsumsplit  12031  fsumsplitsn  12034  sumsplitdc  12056  fprodsplitdc  12220  fprodsplit  12221  fprodunsn  12228  fprodsplitsn  12257  nnnn0modprm0  12891  prm23lt5  12899  reopnap  15340  plyaddlem1  15541  plymullem1  15542  plycoeid3  15551  plycj  15555  lgsdir2  15835  2lgslem3  15903  2lgsoddprmlem3  15913  vtxdfifiun  16221  djulclALT  16502  djurclALT  16503  bj-charfun  16506  bj-nntrans  16650  bj-nnelirr  16652