Theorem elun 3222

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 2700	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 2700	. . 3 |- ( A e. B -> A e. _V )
3		elex 2700	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 706	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2203	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2203	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
7	5, 6	orbi12d 783	. . 3 |- ( x = A -> ( ( x e. B \/ x e. C ) <-> ( A e. B \/ A e. C ) ) )
8		df-un 3080	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 2835	. 2 |- ( A e. _V -> ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) ) )
10	1, 4, 9	pm5.21nii 694	1 |- ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) )

Syntax hints:   <-> wb 104   \/ wo 698   = wceq 1332   e. wcel 1481   _Vcvv 2689   u. cun 3074

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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-un 3080

This theorem is referenced by:  uneqri  3223  uncom  3225  uneq1  3228  unass  3238  ssun1  3244  unss1  3250  ssequn1  3251  unss  3255  rexun  3261  ralunb  3262  unssdif  3316  unssin  3320  inssun  3321  indi  3328  undi  3329  difundi  3333  difindiss  3335  undif3ss  3342  symdifxor  3347  rabun2  3360  reuun2  3364  undif4  3430  ssundifim  3451  dcun  3478  dfpr2  3551  eltpg  3576  pwprss  3740  pwtpss  3741  uniun  3763  intun  3810  iunun  3899  iunxun  3900  iinuniss  3903  brun  3987  undifexmid  4125  exmidundif  4137  exmidundifim  4138  pwunss  4213  elsuci  4333  elsucg  4334  elsuc2g  4335  ordsucim  4424  sucprcreg  4472  opthprc  4598  xpundi  4603  xpundir  4604  funun  5175  mptun  5262  unpreima  5553  reldmtpos  6158  dftpos4  6168  tpostpos  6169  onunsnss  6813  unfidisj  6818  undifdcss  6819  fidcenumlemrks  6849  djulclb  6948  eldju  6961  eldju2ndl  6965  eldju2ndr  6966  ctssdccl  7004  elnn0  9003  un0addcl  9034  un0mulcl  9035  elxnn0  9066  ltxr  9592  elxr  9593  fzsplit2  9861  elfzp1  9883  uzsplit  9903  elfzp12  9910  fz01or  9922  fzosplit  9985  fzouzsplit  9987  elfzonlteqm1  10018  fzosplitsni  10043  hashinfuni  10555  hashennnuni  10557  hashunlem  10582  zfz1isolemiso  10614  summodclem3  11181  fsumsplit  11208  fsumsplitsn  11211  sumsplitdc  11233  reopnap  12746  djulclALT  13179  djurclALT  13180  bj-nntrans  13320  bj-nnelirr  13322  exmid1stab  13368