Theorem elun 3345

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 2811	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 2811	. . 3 |- ( A e. B -> A e. _V )
3		elex 2811	. . 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 3201	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 2950	. 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 2799   u. cun 3195

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 2801  df-un 3201

This theorem is referenced by:  uneqri  3346  uncom  3348  uneq1  3351  unass  3361  ssun1  3367  unss1  3373  ssequn1  3374  unss  3378  rexun  3384  ralunb  3385  unssdif  3439  unssin  3443  inssun  3444  indi  3451  undi  3452  difundi  3456  difindiss  3458  undif3ss  3465  symdifxor  3470  rabun2  3483  reuun2  3487  undif4  3554  ssundifim  3575  dcun  3601  dfpr2  3685  eltpg  3711  pwprss  3884  pwtpss  3885  uniun  3907  intun  3954  iunun  4044  iunxun  4045  iinuniss  4048  brun  4135  undifexmid  4277  exmidundif  4290  exmidundifim  4291  exmid1stab  4292  pwunss  4374  elsuci  4494  elsucg  4495  elsuc2g  4496  ordsucim  4592  sucprcreg  4641  opthprc  4770  xpundi  4775  xpundir  4776  funun  5362  mptun  5455  unpreima  5762  reldmtpos  6405  dftpos4  6415  tpostpos  6416  elssdc  7075  onunsnss  7090  unfidisj  7095  undifdcss  7096  fidcenumlemrks  7131  djulclb  7233  eldju  7246  eldju2ndl  7250  eldju2ndr  7251  ctssdccl  7289  pw1nel3  7427  sucpw1nel3  7429  elnn0  9382  un0addcl  9413  un0mulcl  9414  elxnn0  9445  ltxr  9983  elxr  9984  fzsplit2  10258  elfzp1  10280  uzsplit  10300  elfzp12  10307  fz01or  10319  fzosplit  10387  fzouzsplit  10389  elfzonlteqm1  10428  fzosplitsni  10453  hashinfuni  11011  hashennnuni  11013  hashunlem  11038  zfz1isolemiso  11074  ccatrn  11157  cats1un  11268  summodclem3  11906  fsumsplit  11933  fsumsplitsn  11936  sumsplitdc  11958  fprodsplitdc  12122  fprodsplit  12123  fprodunsn  12130  fprodsplitsn  12159  nnnn0modprm0  12793  prm23lt5  12801  reopnap  15235  plyaddlem1  15436  plymullem1  15437  plycoeid3  15446  plycj  15450  lgsdir2  15727  2lgslem3  15795  2lgsoddprmlem3  15805  vtxdfifiun  16056  djulclALT  16220  djurclALT  16221  bj-charfun  16225  bj-nntrans  16369  bj-nnelirr  16371