Theorem elun 3276

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 2748	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 2748	. . 3 |- ( A e. B -> A e. _V )
3		elex 2748	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 716	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2240	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2240	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
7	5, 6	orbi12d 793	. . 3 |- ( x = A -> ( ( x e. B \/ x e. C ) <-> ( A e. B \/ A e. C ) ) )
8		df-un 3133	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 2884	. 2 |- ( A e. _V -> ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) ) )
10	1, 4, 9	pm5.21nii 704	1 |- ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) )

Syntax hints:   <-> wb 105   \/ wo 708   = wceq 1353   e. wcel 2148   _Vcvv 2737   u. cun 3127

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133

This theorem is referenced by:  uneqri  3277  uncom  3279  uneq1  3282  unass  3292  ssun1  3298  unss1  3304  ssequn1  3305  unss  3309  rexun  3315  ralunb  3316  unssdif  3370  unssin  3374  inssun  3375  indi  3382  undi  3383  difundi  3387  difindiss  3389  undif3ss  3396  symdifxor  3401  rabun2  3414  reuun2  3418  undif4  3485  ssundifim  3506  dcun  3533  dfpr2  3611  eltpg  3637  pwprss  3804  pwtpss  3805  uniun  3827  intun  3874  iunun  3963  iunxun  3964  iinuniss  3967  brun  4052  undifexmid  4191  exmidundif  4204  exmidundifim  4205  exmid1stab  4206  pwunss  4281  elsuci  4401  elsucg  4402  elsuc2g  4403  ordsucim  4497  sucprcreg  4546  opthprc  4675  xpundi  4680  xpundir  4681  funun  5257  mptun  5344  unpreima  5638  reldmtpos  6249  dftpos4  6259  tpostpos  6260  onunsnss  6911  unfidisj  6916  undifdcss  6917  fidcenumlemrks  6947  djulclb  7049  eldju  7062  eldju2ndl  7066  eldju2ndr  7067  ctssdccl  7105  pw1nel3  7225  sucpw1nel3  7227  elnn0  9172  un0addcl  9203  un0mulcl  9204  elxnn0  9235  ltxr  9769  elxr  9770  fzsplit2  10043  elfzp1  10065  uzsplit  10085  elfzp12  10092  fz01or  10104  fzosplit  10170  fzouzsplit  10172  elfzonlteqm1  10203  fzosplitsni  10228  hashinfuni  10748  hashennnuni  10750  hashunlem  10775  zfz1isolemiso  10810  summodclem3  11379  fsumsplit  11406  fsumsplitsn  11409  sumsplitdc  11431  fprodsplitdc  11595  fprodsplit  11596  fprodunsn  11603  fprodsplitsn  11632  nnnn0modprm0  12245  prm23lt5  12253  reopnap  13820  lgsdir2  14216  djulclALT  14324  djurclALT  14325  bj-charfun  14330  bj-nntrans  14474  bj-nnelirr  14476