Theorem elun 3448

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 2924	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 2924	. . 3 |- ( A e. B -> A e. _V )
3		elex 2924	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 369	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2464	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2464	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
7	5, 6	orbi12d 691	. . 3 |- ( x = A -> ( ( x e. B \/ x e. C ) <-> ( A e. B \/ A e. C ) ) )
8		df-un 3285	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 3044	. 2 |- ( A e. _V -> ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) ) )
10	1, 4, 9	pm5.21nii 343	1 |- ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) )

Syntax hints:   <-> wb 177   \/ wo 358   = wceq 1649   e. wcel 1721   _Vcvv 2916   u. cun 3278

This theorem is referenced by:  uneqri  3449  uncom  3451  uneq1  3454  unass  3464  ssun1  3470  unss1  3476  ssequn1  3477  unss  3481  rexun  3487  ralunb  3488  indi  3547  undi  3548  unineq  3551  undif3  3562  symdif2  3567  rabun2  3580  reuun2  3584  undif4  3644  ssundif  3671  dfpr2  3790  eltpg  3811  pwpr  3971  pwtp  3972  uniun  3994  intun  4042  iinun2  4117  iunun  4131  iunxun  4132  iinuni  4134  brun  4218  pwunss  4448  pwssun  4449  elsuci  4607  elsucg  4608  elsuc2g  4609  elpwunsn  4716  suceloni  4752  ordsucun  4764  opthprc  4884  xpundi  4889  xpundir  4890  sossfld  5276  funun  5454  mptun  5534  unpreima  5815  difxp  6339  fnse  6422  reldmtpos  6446  dftpos4  6457  tpostpos  6458  oarec  6764  brdom2  7096  unxpdomlem3  7274  domunfican  7338  dfsup2  7405  dfsup2OLD  7406  wemapso2  7477  unwdomg  7508  unxpwdom2  7512  sucprcreg  7523  cantnfp1lem3  7592  rankunb  7732  iscard3  7930  kmlem2  7987  ssfin4  8146  dffin7-2  8234  fin1a2lem11  8246  fin1a2lem12  8247  cfpwsdom  8415  elgch  8453  fpwwe2lem13  8473  canthp1lem2  8484  gch2  8510  elnn0  10179  un0addcl  10209  un0mulcl  10210  ltxr  10671  elxr  10672  xrsupexmnf  10839  xrinfmexpnf  10840  supxrun  10850  ixxun  10888  difreicc  10984  iccsplit  10985  fzsplit2  11032  elfzp1  11053  uzsplit  11073  elfzp12  11081  fzosplit  11121  fzouzsplit  11123  fzosplitsni  11151  hashnn0pnf  11581  hashf1lem2  11660  cats1un  11745  fsumsplit  12488  sumsplit  12507  rpnnen2  12780  saddisjlem  12931  vdwapun  13297  ramubcl  13341  xpsfrnel2  13745  mreexmrid  13823  lubun  14505  gsumzsplit  15484  gsumunsn  15499  dprddisj2  15552  dmdprdsplit2lem  15558  dmdprdsplit2  15559  dprdsplit  15561  mplcoe1  16483  mplcoe2  16485  evlslem4  16519  clslp  17166  islpi  17167  restntr  17200  pnfnei  17238  mnfnei  17239  iuncon  17444  xkoptsub  17639  ptunhmeo  17793  fbun  17825  filcon  17868  fixufil  17907  ufildr  17916  alexsubALTlem2  18032  alexsubALTlem3  18033  alexsubALTlem4  18034  tsmssplit  18134  xrtgioo  18790  reconnlem2  18811  iccpnfcnv  18922  iccpnfhmeo  18923  mbfss  19491  mbfmax  19494  itg2splitlem  19593  itg2split  19594  iblss2  19650  itgsplit  19680  limcdif  19716  ellimc2  19717  limcmpt  19723  limcres  19726  limccnp  19731  limccnp2  19732  limcco  19733  rollelem  19826  dvivthlem1  19845  dvne0  19848  lhop  19853  degltlem1  19948  ply1rem  20039  fta1glem2  20042  plypf1  20084  plyaddlem1  20085  plymullem1  20086  plycj  20148  ofmulrt  20152  taylfval  20228  abelthlem2  20301  abelthlem3  20302  reasinsin  20689  scvxcvx  20777  ppinprm  20888  chtnprm  20890  dchrfi  20992  lgsdir2  21065  usgraexmpl  21373  vdgrf  21622  vdgrun  21625  vdgrfiun  21626  shunssi  22823  atomli  23838  atoml2i  23839  isoun  24042  fzsplit3  24103  eliccioo  24130  xrge0iifcnv  24272  xrge0iifiso  24274  xrge0iifhom  24276  esumsplit  24400  measvuni  24521  sxbrsigalem0  24574  subfacp1lem4  24822  subfacp1lem5  24823  kur14lem7  24851  fprodsplit  25242  dftrpred3g  25450  wfrlem14  25483  wfrlem15  25484  elsymdif  25581  brcup  25692  refssfne  26264  eqfnun  26313  smprngopr  26552  lzunuz  26716  jm2.23  26957  unxpwdom3  27124  hbtlem5  27200  fnchoice  27567  vdgfrgragt2  28132  frgrawopreglem2  28148  undif3VD  28703  bnj1138  28865  bnj1137  29070  lubunNEW  29456  elpadd  30281  paddval0  30292  hdmaplem4  32257  mapdh9a  32273

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-un 3285