Theorem elun 3485

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 2971	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 2971	. . 3 |- ( A e. B -> A e. _V )
3		elex 2971	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 379	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2493	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2493	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
7	5, 6	orbi12d 702	. . 3 |- ( x = A -> ( ( x e. B \/ x e. C ) <-> ( A e. B \/ A e. C ) ) )
8		df-un 3321	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 3097	. 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 1362   e. wcel 1755   _Vcvv 2962   u. cun 3314

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-un 3321

This theorem is referenced by:  uneqri  3486  uncom  3488  uneq1  3491  unass  3501  ssun1  3507  unss1  3513  ssequn1  3514  unss  3518  rexun  3524  ralunb  3525  indi  3584  undi  3585  unineq  3588  undif3  3599  symdif2  3604  rabun2  3617  reuun2  3621  undif4  3723  ssundif  3750  dfpr2  3880  elpwunsn  3905  eltpg  3906  pwpr  4075  pwtp  4076  uniun  4098  intun  4148  iinun2  4224  iunun  4239  iunxun  4240  iinuni  4242  brun  4328  pwunss  4613  pwssun  4614  elsuci  4772  elsucg  4773  elsuc2g  4774  opthprc  4873  xpundi  4878  xpundir  4879  difxp  5250  sossfld  5273  funun  5448  mptun  5529  unpreima  5817  suceloni  6413  ordsucun  6425  fnse  6678  reldmtpos  6742  dftpos4  6753  tpostpos  6754  oarec  6989  brdom2  7327  unxpdomlem3  7507  domunfican  7572  dfsup2  7680  dfsup2OLD  7681  wemapso2OLD  7754  wemapso2lem  7755  unwdomg  7787  unxpwdom2  7791  sucprcregOLD  7803  cantnfp1lem3  7876  cantnfp1lem3OLD  7902  rankunb  8045  iscard3  8251  kmlem2  8308  ssfin4  8467  dffin7-2  8555  fin1a2lem11  8567  fin1a2lem12  8568  cfpwsdom  8736  elgch  8777  fpwwe2lem13  8797  canthp1lem2  8808  gch2  8830  elnn0  10569  un0addcl  10601  un0mulcl  10602  ltxr  11083  elxr  11084  xrsupexmnf  11255  xrinfmexpnf  11256  supxrun  11266  ixxun  11304  difreicc  11404  iccsplit  11405  fzsplit2  11461  elfzp1  11490  uzsplit  11514  elfzp12  11523  fzosplit  11566  fzouzsplit  11568  fzosplitsni  11618  hashnn0pnf  12097  hash2pwpr  12166  pr2pwpr  12167  hashf1lem2  12193  cats1un  12354  fsumsplit  13200  sumsplit  13219  rpnnen2  13491  saddisjlem  13643  nnnn0modprm0  13857  vdwapun  14018  ramubcl  14062  xpsfrnel2  14486  mreexmrid  14564  lubun  15276  symgextf1  15906  gsumzsplit  16398  gsumzsplitOLD  16399  gsumunsnd  16427  dprddisj2  16511  dprddisj2OLD  16512  dmdprdsplit2lem  16518  dmdprdsplit2  16519  dprdsplit  16521  mplcoe1  17478  mplcoe2  17481  mplcoe2OLD  17482  evlslem4OLD  17518  evlslem4  17519  mdetunilem9  18268  maducoeval2  18288  madugsum  18291  clslp  18594  islpi  18595  restntr  18628  pnfnei  18666  mnfnei  18667  iuncon  18874  xkoptsub  19069  ptunhmeo  19223  fbun  19255  filcon  19298  fixufil  19337  ufildr  19346  alexsubALTlem2  19462  alexsubALTlem3  19463  alexsubALTlem4  19464  tsmssplit  19568  xrtgioo  20225  reconnlem2  20246  iccpnfcnv  20358  iccpnfhmeo  20359  rrxcph  20738  rrxdstprj1  20750  mbfss  20966  mbfmax  20969  itg2splitlem  21068  itg2split  21069  iblss2  21125  itgsplit  21155  limcdif  21193  ellimc2  21194  limcmpt  21200  limcres  21203  limccnp  21208  limccnp2  21209  limcco  21210  rollelem  21303  dvivthlem1  21322  dvne0  21325  lhop  21330  degltlem1  21428  ply1rem  21520  fta1glem2  21523  plypf1  21565  plyaddlem1  21566  plymullem1  21567  plycj  21629  ofmulrt  21633  taylfval  21709  abelthlem2  21782  abelthlem3  21783  reasinsin  22176  scvxcvx  22264  ppinprm  22375  chtnprm  22377  dchrfi  22479  lgsdir2  22552  usgraexmpl  23142  vdgrf  23391  vdgrun  23394  vdgrfiun  23395  shunssi  24594  atomli  25609  atoml2i  25610  isoun  25821  fzsplit3  25901  eliccioo  25929  gsumunsnf  26097  ordtconlem1  26208  xrge0iifcnv  26217  xrge0iifiso  26219  xrge0iifhom  26221  esumsplit  26360  measvuni  26482  sxbrsigalem0  26540  subfacp1lem4  26919  subfacp1lem5  26920  kur14lem7  26948  fprodsplit  27323  dftrpred3g  27544  wfrlem14  27584  wfrlem15  27585  elsymdif  27701  brcup  27817  tan2h  28268  ftc1anclem1  28311  ftc1anclem5  28315  dvasin  28324  dvacos  28325  refssfne  28410  eqfnun  28459  smprngopr  28696  lzunuz  28951  jm2.23  29190  unxpwdom3  29293  hbtlem5  29329  fnchoice  29596  elfzonlteqm1  30071  vdgfrgragt2  30466  frgrawopreglem2  30484  undif3VD  31320  iunconlem2  31373  bnj1138  31484  bnj1137  31688  bj-eltag  32053  bj-0eltag  32054  bj-sngltag  32059  bj-projun  32070  elpadd  33016  paddval0  33027  hdmaplem4  34992  mapdh9a  35008