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  6418  dftpos4  6428  tpostpos  6429  elssdc  7093  onunsnss  7108  unfidisj  7113  undifdcss  7114  fidcenumlemrks  7151  djulclb  7253  eldju  7266  eldju2ndl  7270  eldju2ndr  7271  ctssdccl  7309  pw1nel3  7448  sucpw1nel3  7450  elnn0  9403  un0addcl  9434  un0mulcl  9435  elxnn0  9466  ltxr  10009  elxr  10010  fzsplit2  10284  elfzp1  10306  uzsplit  10326  elfzp12  10333  fz01or  10345  fzosplit  10413  fzouzsplit  10415  elfzonlteqm1  10454  fzosplitsni  10480  hashinfuni  11038  hashennnuni  11040  hashunlem  11066  zfz1isolemiso  11102  ccatrn  11185  cats1un  11301  summodclem3  11940  fsumsplit  11967  fsumsplitsn  11970  sumsplitdc  11992  fprodsplitdc  12156  fprodsplit  12157  fprodunsn  12164  fprodsplitsn  12193  nnnn0modprm0  12827  prm23lt5  12835  reopnap  15269  plyaddlem1  15470  plymullem1  15471  plycoeid3  15480  plycj  15484  lgsdir2  15761  2lgslem3  15829  2lgsoddprmlem3  15839  vtxdfifiun  16147  djulclALT  16397  djurclALT  16398  bj-charfun  16402  bj-nntrans  16546  bj-nnelirr  16548