Theorem elun 3125

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 2621	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 2621	. . 3 |- ( A e. B -> A e. _V )
3		elex 2621	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 669	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2145	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2145	. . . 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 2988	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 2750	. 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 1285   e. wcel 1434   _Vcvv 2612   u. cun 2982

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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065

This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-v 2614  df-un 2988

This theorem is referenced by:  uneqri  3126  uncom  3128  uneq1  3131  unass  3141  ssun1  3147  unss1  3153  ssequn1  3154  unss  3158  rexun  3164  ralunb  3165  unssdif  3217  unssin  3221  inssun  3222  indi  3229  undi  3230  difundi  3234  difindiss  3236  undif3ss  3243  symdifxor  3248  rabun2  3261  reuun2  3265  undif4  3327  ssundifim  3347  dfpr2  3441  eltpg  3462  pwprss  3623  pwtpss  3624  uniun  3646  intun  3693  iunun  3781  iunxun  3782  iinuniss  3784  brun  3857  undifexmid  3991  exmidundif  3998  pwunss  4073  elsuci  4193  elsucg  4194  elsuc2g  4195  ordsucim  4279  sucprcreg  4327  opthprc  4446  xpundi  4451  xpundir  4452  funun  5010  mptun  5096  unpreima  5368  reldmtpos  5949  dftpos4  5959  tpostpos  5960  onunsnss  6553  unfidisj  6558  undifdcss  6559  djulclb  6653  djur  6663  eldju  6665  djuun  6666  eldju2ndl  6669  eldju2ndr  6670  elnn0  8566  un0addcl  8597  un0mulcl  8598  elxnn0  8631  ltxr  9140  elxr  9141  fzsplit2  9358  elfzp1  9378  uzsplit  9398  elfzp12  9405  fz01or  9417  fzosplit  9476  fzouzsplit  9478  elfzonlteqm1  9509  fzosplitsni  9534  hashinfuni  10019  hashennnuni  10021  hashunlem  10046  djulclALT  11043  djurclALT  11044  bj-nntrans  11188  bj-nnelirr  11190