Theorem elun 3492

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 2976	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 2976	. . 3 |- ( A e. B -> A e. _V )
3		elex 2976	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 379	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2498	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2498	. . . 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 3328	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 3103	. 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 1369   e. wcel 1756   _Vcvv 2967   u. cun 3321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-un 3328

This theorem is referenced by:  uneqri  3493  uncom  3495  uneq1  3498  unass  3508  ssun1  3514  unss1  3520  ssequn1  3521  unss  3525  rexun  3531  ralunb  3532  indi  3591  undi  3592  unineq  3595  undif3  3606  symdif2  3611  rabun2  3624  reuun2  3628  undif4  3730  ssundif  3757  dfpr2  3887  elpwunsn  3912  eltpg  3913  pwpr  4082  pwtp  4083  uniun  4105  intun  4155  iinun2  4231  iunun  4246  iunxun  4247  iinuni  4249  brun  4335  pwunss  4621  pwssun  4622  elsuci  4780  elsucg  4781  elsuc2g  4782  opthprc  4881  xpundi  4886  xpundir  4887  difxp  5257  sossfld  5280  funun  5455  mptun  5536  unpreima  5824  suceloni  6419  ordsucun  6431  fnse  6684  reldmtpos  6748  dftpos4  6759  tpostpos  6760  oarec  6993  brdom2  7331  unxpdomlem3  7511  domunfican  7576  dfsup2  7684  dfsup2OLD  7685  wemapso2OLD  7758  wemapso2lem  7759  unwdomg  7791  unxpwdom2  7795  sucprcregOLD  7807  cantnfp1lem3  7880  cantnfp1lem3OLD  7906  rankunb  8049  iscard3  8255  kmlem2  8312  ssfin4  8471  dffin7-2  8559  fin1a2lem11  8571  fin1a2lem12  8572  cfpwsdom  8740  elgch  8781  fpwwe2lem13  8801  canthp1lem2  8812  gch2  8834  elnn0  10573  un0addcl  10605  un0mulcl  10606  ltxr  11087  elxr  11088  xrsupexmnf  11259  xrinfmexpnf  11260  supxrun  11270  ixxun  11308  difreicc  11409  iccsplit  11410  fzsplit2  11466  elfzp1  11497  uzsplit  11522  elfzp12  11531  fzosplit  11574  fzouzsplit  11576  fzosplitsni  11626  hashnn0pnf  12105  hash2pwpr  12174  pr2pwpr  12175  hashf1lem2  12201  cats1un  12362  fsumsplit  13208  sumsplit  13227  rpnnen2  13500  saddisjlem  13652  nnnn0modprm0  13866  vdwapun  14027  ramubcl  14071  xpsfrnel2  14495  mreexmrid  14573  lubun  15285  symgextf1  15917  gsumzsplit  16409  gsumzsplitOLD  16410  gsumzunsnd  16441  gsumunsnd  16442  dprddisj2  16527  dprddisj2OLD  16528  dmdprdsplit2lem  16534  dmdprdsplit2  16535  dprdsplit  16537  mplcoe1  17524  mplcoe5  17528  mplcoe2OLD  17530  evlslem4OLD  17570  evlslem4  17571  mdetunilem9  18406  maducoeval2  18426  madugsum  18429  clslp  18732  islpi  18733  restntr  18766  pnfnei  18804  mnfnei  18805  iuncon  19012  xkoptsub  19207  ptunhmeo  19361  fbun  19393  filcon  19436  fixufil  19475  ufildr  19484  alexsubALTlem2  19600  alexsubALTlem3  19601  alexsubALTlem4  19602  tsmssplit  19706  xrtgioo  20363  reconnlem2  20384  iccpnfcnv  20496  iccpnfhmeo  20497  rrxcph  20876  rrxdstprj1  20888  mbfss  21104  mbfmax  21107  itg2splitlem  21206  itg2split  21207  iblss2  21263  itgsplit  21293  limcdif  21331  ellimc2  21332  limcmpt  21338  limcres  21341  limccnp  21346  limccnp2  21347  limcco  21348  rollelem  21441  dvivthlem1  21460  dvne0  21463  lhop  21468  degltlem1  21523  ply1rem  21615  fta1glem2  21618  plypf1  21660  plyaddlem1  21661  plymullem1  21662  plycj  21724  ofmulrt  21728  taylfval  21804  abelthlem2  21877  abelthlem3  21878  reasinsin  22271  scvxcvx  22359  ppinprm  22470  chtnprm  22472  dchrfi  22574  lgsdir2  22647  usgraexmpl  23287  vdgrf  23536  vdgrun  23539  vdgrfiun  23540  shunssi  24739  atomli  25754  atoml2i  25755  isoun  25965  fzsplit3  26046  eliccioo  26074  gsumunsnf  26213  ordtconlem1  26323  xrge0iifcnv  26332  xrge0iifiso  26334  xrge0iifhom  26336  esumsplit  26475  measvuni  26597  sxbrsigalem0  26655  subfacp1lem4  27040  subfacp1lem5  27041  kur14lem7  27069  fprodsplit  27445  dftrpred3g  27666  wfrlem14  27706  wfrlem15  27707  elsymdif  27823  brcup  27939  tan2h  28395  ftc1anclem1  28438  ftc1anclem5  28442  dvasin  28451  dvacos  28452  refssfne  28537  eqfnun  28586  smprngopr  28823  lzunuz  29077  jm2.23  29316  unxpwdom3  29419  hbtlem5  29455  fnchoice  29722  elfzonlteqm1  30196  vdgfrgragt2  30591  frgrawopreglem2  30609  undif3VD  31547  iunconlem2  31600  bnj1138  31711  bnj1137  31915  bj-eltag  32370  bj-0eltag  32371  bj-sngltag  32376  bj-projun  32387  elpadd  33336  paddval0  33347  hdmaplem4  35312  mapdh9a  35328