Theorem elun 3595

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 3077	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 3077	. . 3 |- ( A e. B -> A e. _V )
3		elex 3077	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 379	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2523	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2523	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
7	5, 6	orbi12d 709	. . 3 |- ( x = A -> ( ( x e. B \/ x e. C ) <-> ( A e. B \/ A e. C ) ) )
8		df-un 3431	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 3205	. 2 |- ( A e. _V -> ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) ) )
10	1, 4, 9	pm5.21nii 353	1 |- ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) )

Syntax hints:   <-> wb 184   \/ wo 368   = wceq 1370   e. wcel 1758   _Vcvv 3068   u. cun 3424

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3070  df-un 3431

This theorem is referenced by:  uneqri  3596  uncom  3598  uneq1  3601  unass  3611  ssun1  3617  unss1  3623  ssequn1  3624  unss  3628  rexun  3634  ralunb  3635  indi  3694  undi  3695  unineq  3698  undif3  3709  symdif2  3714  rabun2  3727  reuun2  3731  undif4  3833  ssundif  3860  dfpr2  3990  elpwunsn  4015  eltpg  4016  pwpr  4185  pwtp  4186  uniun  4208  intun  4258  iinun2  4334  iunun  4349  iunxun  4350  iinuni  4352  brun  4438  pwunss  4724  pwssun  4725  elsuci  4883  elsucg  4884  elsuc2g  4885  opthprc  4984  xpundi  4989  xpundir  4990  difxp  5360  sossfld  5383  funun  5558  mptun  5639  unpreima  5928  suceloni  6524  ordsucun  6536  fnse  6789  reldmtpos  6853  dftpos4  6864  tpostpos  6865  oarec  7101  brdom2  7439  unxpdomlem3  7620  domunfican  7685  dfsup2  7793  dfsup2OLD  7794  wemapso2OLD  7867  wemapso2lem  7868  unwdomg  7900  unxpwdom2  7904  sucprcregOLD  7916  cantnfp1lem3  7989  cantnfp1lem3OLD  8015  rankunb  8158  iscard3  8364  kmlem2  8421  ssfin4  8580  dffin7-2  8668  fin1a2lem11  8680  fin1a2lem12  8681  cfpwsdom  8849  elgch  8890  fpwwe2lem13  8910  canthp1lem2  8921  gch2  8943  elnn0  10682  un0addcl  10714  un0mulcl  10715  ltxr  11196  elxr  11197  xrsupexmnf  11368  xrinfmexpnf  11369  supxrun  11379  ixxun  11417  difreicc  11518  iccsplit  11519  fzsplit2  11575  elfzp1  11606  uzsplit  11631  elfzp12  11640  fzosplit  11683  fzouzsplit  11685  fzosplitsni  11735  hashnn0pnf  12214  hash2pwpr  12284  pr2pwpr  12285  hashf1lem2  12311  cats1un  12472  fsumsplit  13318  sumsplit  13337  rpnnen2  13610  saddisjlem  13762  nnnn0modprm0  13976  vdwapun  14137  ramubcl  14181  xpsfrnel2  14605  mreexmrid  14683  lubun  15395  symgextf1  16028  gsumzsplit  16522  gsumzsplitOLD  16523  gsumzunsnd  16556  gsumunsnd  16557  dprddisj2  16642  dprddisj2OLD  16643  dmdprdsplit2lem  16649  dmdprdsplit2  16650  dprdsplit  16652  mplcoe1  17651  mplcoe5  17655  mplcoe2OLD  17657  evlslem4OLD  17697  evlslem4  17698  mdetunilem9  18542  maducoeval2  18562  madugsum  18565  clslp  18868  islpi  18869  restntr  18902  pnfnei  18940  mnfnei  18941  iuncon  19148  xkoptsub  19343  ptunhmeo  19497  fbun  19529  filcon  19572  fixufil  19611  ufildr  19620  alexsubALTlem2  19736  alexsubALTlem3  19737  alexsubALTlem4  19738  tsmssplit  19842  xrtgioo  20499  reconnlem2  20520  iccpnfcnv  20632  iccpnfhmeo  20633  rrxcph  21012  rrxdstprj1  21024  mbfss  21240  mbfmax  21243  itg2splitlem  21342  itg2split  21343  iblss2  21399  itgsplit  21429  limcdif  21467  ellimc2  21468  limcmpt  21474  limcres  21477  limccnp  21482  limccnp2  21483  limcco  21484  rollelem  21577  dvivthlem1  21596  dvne0  21599  lhop  21604  degltlem1  21659  ply1rem  21751  fta1glem2  21754  plypf1  21796  plyaddlem1  21797  plymullem1  21798  plycj  21860  ofmulrt  21864  taylfval  21940  abelthlem2  22013  abelthlem3  22014  reasinsin  22407  scvxcvx  22495  ppinprm  22606  chtnprm  22608  dchrfi  22710  lgsdir2  22783  usgraexmpl  23454  vdgrf  23703  vdgrun  23706  vdgrfiun  23707  shunssi  24906  atomli  25921  atoml2i  25922  isoun  26131  fzsplit3  26212  eliccioo  26240  gsumunsnf  26379  ordtconlem1  26488  xrge0iifcnv  26497  xrge0iifiso  26499  xrge0iifhom  26501  esumsplit  26640  measvuni  26762  sxbrsigalem0  26820  subfacp1lem4  27205  subfacp1lem5  27206  kur14lem7  27234  fprodsplit  27610  dftrpred3g  27831  wfrlem14  27871  wfrlem15  27872  elsymdif  27988  brcup  28104  tan2h  28562  ftc1anclem1  28605  ftc1anclem5  28609  dvasin  28618  dvacos  28619  refssfne  28704  eqfnun  28753  smprngopr  28990  lzunuz  29244  jm2.23  29483  unxpwdom3  29586  hbtlem5  29622  fnchoice  29889  elfzonlteqm1  30363  vdgfrgragt2  30758  frgrawopreglem2  30776  undif3VD  31918  iunconlem2  31971  bnj1138  32082  bnj1137  32286  bj-eltag  32770  bj-0eltag  32771  bj-sngltag  32776  bj-projun  32787  elpadd  33749  paddval0  33760  hdmaplem4  35725  mapdh9a  35741