Theorem elun 3217

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 2697	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 2697	. . 3 |- ( A e. B -> A e. _V )
3		elex 2697	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 705	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2202	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2202	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
7	5, 6	orbi12d 782	. . 3 |- ( x = A -> ( ( x e. B \/ x e. C ) <-> ( A e. B \/ A e. C ) ) )
8		df-un 3075	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 2831	. 2 |- ( A e. _V -> ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) ) )
10	1, 4, 9	pm5.21nii 693	1 |- ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) )

Syntax hints:   <-> wb 104   \/ wo 697   = wceq 1331   e. wcel 1480   _Vcvv 2686   u. cun 3069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688  df-un 3075

This theorem is referenced by:  uneqri  3218  uncom  3220  uneq1  3223  unass  3233  ssun1  3239  unss1  3245  ssequn1  3246  unss  3250  rexun  3256  ralunb  3257  unssdif  3311  unssin  3315  inssun  3316  indi  3323  undi  3324  difundi  3328  difindiss  3330  undif3ss  3337  symdifxor  3342  rabun2  3355  reuun2  3359  undif4  3425  ssundifim  3446  dcun  3473  dfpr2  3546  eltpg  3569  pwprss  3732  pwtpss  3733  uniun  3755  intun  3802  iunun  3891  iunxun  3892  iinuniss  3895  brun  3979  undifexmid  4117  exmidundif  4129  exmidundifim  4130  pwunss  4205  elsuci  4325  elsucg  4326  elsuc2g  4327  ordsucim  4416  sucprcreg  4464  opthprc  4590  xpundi  4595  xpundir  4596  funun  5167  mptun  5254  unpreima  5545  reldmtpos  6150  dftpos4  6160  tpostpos  6161  onunsnss  6805  unfidisj  6810  undifdcss  6811  fidcenumlemrks  6841  djulclb  6940  eldju  6953  eldju2ndl  6957  eldju2ndr  6958  ctssdccl  6996  elnn0  8979  un0addcl  9010  un0mulcl  9011  elxnn0  9042  ltxr  9562  elxr  9563  fzsplit2  9830  elfzp1  9852  uzsplit  9872  elfzp12  9879  fz01or  9891  fzosplit  9954  fzouzsplit  9956  elfzonlteqm1  9987  fzosplitsni  10012  hashinfuni  10523  hashennnuni  10525  hashunlem  10550  zfz1isolemiso  10582  summodclem3  11149  fsumsplit  11176  fsumsplitsn  11179  sumsplitdc  11201  reopnap  12707  djulclALT  13008  djurclALT  13009  bj-nntrans  13149  bj-nnelirr  13151  exmid1stab  13195