Theorem elun 3574

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 3054	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 3054	. . 3 |- ( A e. B -> A e. _V )
3		elex 3054	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 381	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2517	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2517	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
7	5, 6	orbi12d 716	. . 3 |- ( x = A -> ( ( x e. B \/ x e. C ) <-> ( A e. B \/ A e. C ) ) )
8		df-un 3409	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 3187	. 2 |- ( A e. _V -> ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) ) )
10	1, 4, 9	pm5.21nii 355	1 |- ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) )

Syntax hints:   <-> wb 188   \/ wo 370   = wceq 1444   e. wcel 1887   _Vcvv 3045   u. cun 3402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-v 3047  df-un 3409

This theorem is referenced by:  elunnel1  3575  uneqri  3576  uncom  3578  uneq1  3581  unass  3591  ssun1  3597  unss1  3603  ssequn1  3604  unss  3608  rexun  3614  ralunb  3615  elsymdif  3668  symdif2  3671  indi  3689  undi  3690  unineq  3693  undif3  3704  rabun2  3722  reuun2  3726  undif4  3821  ssundif  3851  dfpr2  3983  elpwunsn  4012  eltpg  4014  pwpr  4194  pwtp  4195  uniun  4217  intun  4267  iinun2  4344  iunun  4362  iunxun  4363  iinuni  4365  brun  4451  pwunss  4739  pwssun  4740  opthprc  4882  xpundi  4887  xpundir  4888  difxp  5261  sossfld  5283  elsuci  5489  elsucg  5490  elsuc2g  5491  funun  5624  mptun  5709  unpreima  6006  suceloni  6640  ordsucun  6652  fnse  6913  reldmtpos  6981  dftpos4  6992  tpostpos  6993  wfrlem14  7049  wfrlem15  7050  oarec  7263  brdom2  7599  unxpdomlem3  7778  domunfican  7844  dfsup2  7958  wemapso2lem  8067  unwdomg  8099  unxpwdom2  8103  cantnfp1lem3  8185  rankunb  8321  iscard3  8524  kmlem2  8581  ssfin4  8740  dffin7-2  8828  fin1a2lem11  8840  fin1a2lem12  8841  cfpwsdom  9009  elgch  9047  fpwwe2lem13  9067  canthp1lem2  9078  gch2  9100  elnn0  10871  un0addcl  10903  un0mulcl  10904  ltxr  11415  elxr  11416  xrsupexmnf  11590  xrinfmexpnf  11591  supxrun  11601  ixxun  11651  difreicc  11764  iccsplit  11765  fzsplit2  11824  elfzp1  11846  uzsplit  11866  elfzp12  11873  fzosplit  11951  fzouzsplit  11953  elfzonlteqm1  11989  fzosplitsni  12019  hashnn0pnf  12525  hashf1lem2  12619  hash2pwpr  12635  pr2pwpr  12636  ccatrn  12733  cats1un  12832  fsumsplit  13806  sumsplit  13829  fprodsplit  14020  rpnnen2  14278  saddisjlem  14438  lcmfunsnlem1  14610  lcmfunsnlem2lem1  14611  lcmfunsnlem2lem2  14612  lcmfunsnlem2  14613  coprmprod  14678  coprmproddvdslem  14679  nnnn0modprm0  14757  vdwapun  14924  ramubcl  14976  xpsfrnel2  15471  mreexmrid  15549  lubun  16369  symgextf1  17062  gsumzsplit  17560  gsumzunsnd  17588  gsumunsnfd  17589  dprddisj2  17672  dmdprdsplit2lem  17678  dmdprdsplit2  17679  dprdsplit  17681  mplcoe1  18689  mplcoe5  18692  evlslem4  18731  mdetunilem9  19645  maducoeval2  19665  madugsum  19668  clslp  20164  islpi  20165  restntr  20198  pnfnei  20236  mnfnei  20237  iuncon  20443  refun0  20530  xkoptsub  20669  ptunhmeo  20823  fbun  20855  filcon  20898  fixufil  20937  ufildr  20946  alexsubALTlem2  21063  alexsubALTlem3  21064  alexsubALTlem4  21065  tsmssplit  21166  xrtgioo  21824  reconnlem2  21845  iccpnfcnv  21972  iccpnfhmeo  21973  rrxcph  22351  rrxdstprj1  22363  mbfss  22602  mbfmax  22605  itg2splitlem  22706  itg2split  22707  iblss2  22763  itgsplit  22793  limcdif  22831  ellimc2  22832  limcmpt  22838  limcres  22841  limccnp  22846  limccnp2  22847  limcco  22848  rollelem  22941  dvivthlem1  22960  dvne0  22963  lhop  22968  degltlem1  23021  ply1rem  23114  fta1glem2  23117  plypf1  23166  plyaddlem1  23167  plymullem1  23168  plycj  23231  ofmulrt  23235  taylfval  23314  abelthlem2  23387  abelthlem3  23388  reasinsin  23822  scvxcvx  23911  ppinprm  24079  chtnprm  24081  dchrfi  24183  lgsdir2  24256  usgraexmplef  25128  vdgrf  25626  vdgrun  25629  vdgrfiun  25630  vdgfrgragt2  25755  frgrawopreglem2  25773  shunssi  27021  atomli  28035  atoml2i  28036  isoun  28282  fzsplit3  28370  eliccioo  28400  ordtconlem1  28730  xrge0iifcnv  28739  xrge0iifiso  28741  xrge0iifhom  28743  esumsplit  28874  esumpad2  28877  measvuni  29036  sxbrsigalem0  29093  bnj1138  29600  bnj1137  29804  subfacp1lem4  29906  subfacp1lem5  29907  kur14lem7  29935  mrsubcv  30148  mclsax  30207  dftrpred3g  30474  brcup  30706  refssfne  31014  bj-eltag  31571  bj-0eltag  31572  bj-sngltag  31577  bj-projun  31588  tan2h  31937  poimirlem2  31942  poimirlem8  31948  poimirlem18  31958  poimirlem21  31961  poimirlem22  31962  poimirlem23  31963  poimirlem24  31964  poimirlem25  31965  poimirlem27  31967  poimirlem29  31969  poimirlem31  31971  poimirlem32  31972  ftc1anclem1  32017  ftc1anclem5  32021  dvasin  32028  dvacos  32029  eqfnun  32048  smprngopr  32285  elpadd  33364  paddval0  33375  hdmaplem4  35342  mapdh9a  35358  lzunuz  35610  jm2.23  35851  unxpwdom3  35953  hbtlem5  35987  rp-fakeinunass  36160  frege133d  36357  frege83  36542  frege131  36590  frege133  36592  radcnvrat  36663  bccbc  36694  undif3VD  37279  iunconlem2  37332  fnchoice  37350  elunnel2  37360  unima  37429  limciccioolb  37701  limcicciooub  37717  icccncfext  37765  cncfiooicclem1  37771  fourierdlem70  38040  fourierdlem80  38050  fourierdlem93  38063  fourierdlem101  38071  sge0split  38251  el1fzopredsuc  38722  iccpartltu  38739  iccpartgtl  38740  iccpartgt  38741  iccpartleu  38742  iccpartgel  38743  nnsum4primeseven  38895  nnsum4primesevenALTV  38896  wtgoldbnnsum4prm  38897  bgoldbnnsum3prm  38899  bgoldbtbndlem3  38902  bgoldbtbnd  38904  elxnn0  39072  vtxduhgrun  39538