Theorem elun 3291

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 2763	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 2763	. . 3 |- ( A e. B -> A e. _V )
3		elex 2763	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 717	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2252	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2252	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
7	5, 6	orbi12d 794	. . 3 |- ( x = A -> ( ( x e. B \/ x e. C ) <-> ( A e. B \/ A e. C ) ) )
8		df-un 3148	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 2899	. 2 |- ( A e. _V -> ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) ) )
10	1, 4, 9	pm5.21nii 705	1 |- ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) )

Syntax hints:   <-> wb 105   \/ wo 709   = wceq 1364   e. wcel 2160   _Vcvv 2752   u. cun 3142

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-un 3148

This theorem is referenced by:  uneqri  3292  uncom  3294  uneq1  3297  unass  3307  ssun1  3313  unss1  3319  ssequn1  3320  unss  3324  rexun  3330  ralunb  3331  unssdif  3385  unssin  3389  inssun  3390  indi  3397  undi  3398  difundi  3402  difindiss  3404  undif3ss  3411  symdifxor  3416  rabun2  3429  reuun2  3433  undif4  3500  ssundifim  3521  dcun  3548  dfpr2  3626  eltpg  3652  pwprss  3820  pwtpss  3821  uniun  3843  intun  3890  iunun  3980  iunxun  3981  iinuniss  3984  brun  4069  undifexmid  4211  exmidundif  4224  exmidundifim  4225  exmid1stab  4226  pwunss  4301  elsuci  4421  elsucg  4422  elsuc2g  4423  ordsucim  4517  sucprcreg  4566  opthprc  4695  xpundi  4700  xpundir  4701  funun  5279  mptun  5366  unpreima  5662  reldmtpos  6279  dftpos4  6289  tpostpos  6290  onunsnss  6946  unfidisj  6951  undifdcss  6952  fidcenumlemrks  6983  djulclb  7085  eldju  7098  eldju2ndl  7102  eldju2ndr  7103  ctssdccl  7141  pw1nel3  7261  sucpw1nel3  7263  elnn0  9209  un0addcl  9240  un0mulcl  9241  elxnn0  9272  ltxr  9807  elxr  9808  fzsplit2  10082  elfzp1  10104  uzsplit  10124  elfzp12  10131  fz01or  10143  fzosplit  10209  fzouzsplit  10211  elfzonlteqm1  10242  fzosplitsni  10267  hashinfuni  10792  hashennnuni  10794  hashunlem  10819  zfz1isolemiso  10854  summodclem3  11423  fsumsplit  11450  fsumsplitsn  11453  sumsplitdc  11475  fprodsplitdc  11639  fprodsplit  11640  fprodunsn  11647  fprodsplitsn  11676  nnnn0modprm0  12290  prm23lt5  12298  reopnap  14515  lgsdir2  14912  2lgsoddprmlem3  14937  djulclALT  15031  djurclALT  15032  bj-charfun  15037  bj-nntrans  15181  bj-nnelirr  15183