Theorem elun 3638

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 3115	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 3115	. . 3 |- ( A e. B -> A e. _V )
3		elex 3115	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 379	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2532	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2532	. . . 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 3474	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 3245	. 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 1374   e. wcel 1762   _Vcvv 3106   u. cun 3467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-v 3108  df-un 3474

This theorem is referenced by:  uneqri  3639  uncom  3641  uneq1  3644  unass  3654  ssun1  3660  unss1  3666  ssequn1  3667  unss  3671  rexun  3677  ralunb  3678  indi  3737  undi  3738  unineq  3741  undif3  3752  symdif2  3757  rabun2  3770  reuun2  3774  undif4  3876  ssundif  3903  dfpr2  4035  elpwunsn  4061  eltpg  4062  pwpr  4234  pwtp  4235  uniun  4257  intun  4307  iinun2  4384  iunun  4399  iunxun  4400  iinuni  4402  brun  4488  pwunss  4778  pwssun  4779  elsuci  4937  elsucg  4938  elsuc2g  4939  opthprc  5039  xpundi  5044  xpundir  5045  difxp  5422  sossfld  5445  funun  5621  mptun  5703  unpreima  5998  suceloni  6619  ordsucun  6631  fnse  6890  reldmtpos  6953  dftpos4  6964  tpostpos  6965  oarec  7201  brdom2  7535  unxpdomlem3  7716  domunfican  7782  dfsup2  7891  dfsup2OLD  7892  wemapso2OLD  7966  wemapso2lem  7967  unwdomg  7999  unxpwdom2  8003  sucprcregOLD  8015  cantnfp1lem3  8088  cantnfp1lem3OLD  8114  rankunb  8257  iscard3  8463  kmlem2  8520  ssfin4  8679  dffin7-2  8767  fin1a2lem11  8779  fin1a2lem12  8780  cfpwsdom  8948  elgch  8989  fpwwe2lem13  9009  canthp1lem2  9020  gch2  9042  elnn0  10786  un0addcl  10818  un0mulcl  10819  ltxr  11313  elxr  11314  xrsupexmnf  11485  xrinfmexpnf  11486  supxrun  11496  ixxun  11534  difreicc  11641  iccsplit  11642  fzsplit2  11699  elfzp1  11719  uzsplit  11739  elfzp12  11746  fzosplit  11815  fzouzsplit  11817  elfzonlteqm1  11848  fzosplitsni  11877  hashnn0pnf  12370  hashf1lem2  12458  hash2pwpr  12472  pr2pwpr  12473  cats1un  12651  fsumsplit  13511  sumsplit  13532  rpnnen2  13809  saddisjlem  13962  nnnn0modprm0  14179  vdwapun  14340  ramubcl  14384  xpsfrnel2  14809  mreexmrid  14887  lubun  15599  symgextf1  16234  gsumzsplit  16728  gsumzsplitOLD  16729  gsumzunsnd  16766  gsumunsnfd  16767  dprddisj2  16870  dprddisj2OLD  16871  dmdprdsplit2lem  16877  dmdprdsplit2  16878  dprdsplit  16880  mplcoe1  17891  mplcoe5  17895  mplcoe2OLD  17897  evlslem4OLD  17937  evlslem4  17938  mdetunilem9  18882  maducoeval2  18902  madugsum  18905  clslp  19408  islpi  19409  restntr  19442  pnfnei  19480  mnfnei  19481  iuncon  19688  xkoptsub  19883  ptunhmeo  20037  fbun  20069  filcon  20112  fixufil  20151  ufildr  20160  alexsubALTlem2  20276  alexsubALTlem3  20277  alexsubALTlem4  20278  tsmssplit  20382  xrtgioo  21039  reconnlem2  21060  iccpnfcnv  21172  iccpnfhmeo  21173  rrxcph  21552  rrxdstprj1  21564  mbfss  21781  mbfmax  21784  itg2splitlem  21883  itg2split  21884  iblss2  21940  itgsplit  21970  limcdif  22008  ellimc2  22009  limcmpt  22015  limcres  22018  limccnp  22023  limccnp2  22024  limcco  22025  rollelem  22118  dvivthlem1  22137  dvne0  22140  lhop  22145  degltlem1  22200  ply1rem  22292  fta1glem2  22295  plypf1  22337  plyaddlem1  22338  plymullem1  22339  plycj  22401  ofmulrt  22405  taylfval  22481  abelthlem2  22554  abelthlem3  22555  reasinsin  22948  scvxcvx  23036  ppinprm  23147  chtnprm  23149  dchrfi  23251  lgsdir2  23324  usgraexmpl  24063  vdgrf  24560  vdgrun  24563  vdgrfiun  24564  shunssi  25812  atomli  26827  atoml2i  26828  isoun  27042  fzsplit3  27117  eliccioo  27145  ordtconlem1  27392  xrge0iifcnv  27401  xrge0iifiso  27403  xrge0iifhom  27405  esumsplit  27553  measvuni  27675  sxbrsigalem0  27732  subfacp1lem4  28117  subfacp1lem5  28118  kur14lem7  28146  fprodsplit  28522  dftrpred3g  28743  wfrlem14  28783  wfrlem15  28784  elsymdif  28900  brcup  29016  tan2h  29475  ftc1anclem1  29518  ftc1anclem5  29522  dvasin  29531  dvacos  29532  refssfne  29617  eqfnun  29666  smprngopr  29903  lzunuz  30156  jm2.23  30395  unxpwdom3  30498  hbtlem5  30534  fnchoice  30801  elunnel1  30811  elunnel2  30812  unima  30838  limciccioolb  30982  limcicciooub  30998  icccncfext  31045  cncfiooicclem1  31051  fourierdlem70  31296  fourierdlem80  31306  fourierdlem93  31319  fourierdlem101  31327  vdgfrgragt2  31746  frgrawopreglem2  31764  undif3VD  32637  iunconlem2  32690  bnj1138  32801  bnj1137  33005  bj-eltag  33491  bj-0eltag  33492  bj-sngltag  33497  bj-projun  33508  elpadd  34470  paddval0  34481  hdmaplem4  36446  mapdh9a  36462