Theorem elun 3130

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 2624	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 2624	. . 3 |- ( A e. B -> A e. _V )
3		elex 2624	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 669	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2147	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2147	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
7	5, 6	orbi12d 740	. . 3 |- ( x = A -> ( ( x e. B \/ x e. C ) <-> ( A e. B \/ A e. C ) ) )
8		df-un 2992	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 2753	. 2 |- ( A e. _V -> ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) ) )
10	1, 4, 9	pm5.21nii 653	1 |- ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) )

Syntax hints:   <-> wb 103   \/ wo 662   = wceq 1287   e. wcel 1436   _Vcvv 2615   u. cun 2986

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-un 2992

This theorem is referenced by:  uneqri  3131  uncom  3133  uneq1  3136  unass  3146  ssun1  3152  unss1  3158  ssequn1  3159  unss  3163  rexun  3169  ralunb  3170  unssdif  3223  unssin  3227  inssun  3228  indi  3235  undi  3236  difundi  3240  difindiss  3242  undif3ss  3249  symdifxor  3254  rabun2  3267  reuun2  3271  undif4  3333  ssundifim  3353  dfpr2  3450  eltpg  3471  pwprss  3632  pwtpss  3633  uniun  3655  intun  3702  iunun  3790  iunxun  3791  iinuniss  3793  brun  3866  undifexmid  4002  exmidundif  4009  pwunss  4084  elsuci  4204  elsucg  4205  elsuc2g  4206  ordsucim  4290  sucprcreg  4338  opthprc  4457  xpundi  4462  xpundir  4463  funun  5023  mptun  5109  unpreima  5387  reldmtpos  5972  dftpos4  5982  tpostpos  5983  onunsnss  6579  unfidisj  6584  undifdcss  6585  djulclb  6691  djur  6701  eldju  6703  djuun  6704  eldju2ndl  6707  eldju2ndr  6708  elnn0  8608  un0addcl  8639  un0mulcl  8640  elxnn0  8671  ltxr  9178  elxr  9179  fzsplit2  9396  elfzp1  9416  uzsplit  9436  elfzp12  9443  fz01or  9455  fzosplit  9516  fzouzsplit  9518  elfzonlteqm1  9549  fzosplitsni  9574  hashinfuni  10081  hashennnuni  10083  hashunlem  10108  zfz1isolemiso  10140  isummolem3  10659  djulclALT  11139  djurclALT  11140  bj-nntrans  11284  bj-nnelirr  11286