Theorem elun 3607

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 3091	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 3091	. . 3 |- ( A e. B -> A e. _V )
3		elex 3091	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 381	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2495	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2495	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
7	5, 6	orbi12d 715	. . 3 |- ( x = A -> ( ( x e. B \/ x e. C ) <-> ( A e. B \/ A e. C ) ) )
8		df-un 3442	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 3221	. 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 1438   e. wcel 1869   _Vcvv 3082   u. cun 3435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-v 3084  df-un 3442

This theorem is referenced by:  elunnel1  3608  uneqri  3609  uncom  3611  uneq1  3614  unass  3624  ssun1  3630  unss1  3636  ssequn1  3637  unss  3641  rexun  3647  ralunb  3648  elsymdif  3699  symdif2  3702  indi  3720  undi  3721  unineq  3724  undif3  3735  rabun2  3753  reuun2  3757  undif4  3850  ssundif  3880  dfpr2  4012  elpwunsn  4038  eltpg  4040  pwpr  4213  pwtp  4214  uniun  4236  intun  4286  iinun2  4363  iunun  4381  iunxun  4382  iinuni  4384  brun  4470  pwunss  4756  pwssun  4757  opthprc  4899  xpundi  4904  xpundir  4905  difxp  5278  sossfld  5300  elsuci  5506  elsucg  5507  elsuc2g  5508  funun  5641  mptun  5725  unpreima  6019  suceloni  6652  ordsucun  6664  fnse  6922  reldmtpos  6987  dftpos4  6998  tpostpos  6999  wfrlem14  7055  wfrlem15  7056  oarec  7269  brdom2  7604  unxpdomlem3  7782  domunfican  7848  dfsup2  7962  wemapso2lem  8071  unwdomg  8103  unxpwdom2  8107  cantnfp1lem3  8188  rankunb  8324  iscard3  8526  kmlem2  8583  ssfin4  8742  dffin7-2  8830  fin1a2lem11  8842  fin1a2lem12  8843  cfpwsdom  9011  elgch  9049  fpwwe2lem13  9069  canthp1lem2  9080  gch2  9102  elnn0  10873  un0addcl  10905  un0mulcl  10906  ltxr  11417  elxr  11418  xrsupexmnf  11592  xrinfmexpnf  11593  supxrun  11603  ixxun  11653  difreicc  11766  iccsplit  11767  fzsplit2  11826  elfzp1  11848  uzsplit  11868  elfzp12  11875  fzosplit  11953  fzouzsplit  11955  elfzonlteqm1  11990  fzosplitsni  12020  hashnn0pnf  12526  hashf1lem2  12618  hash2pwpr  12633  pr2pwpr  12634  ccatrn  12731  cats1un  12828  fsumsplit  13799  sumsplit  13822  fprodsplit  14013  rpnnen2  14271  saddisjlem  14431  lcmfunsnlem1  14603  lcmfunsnlem2lem1  14604  lcmfunsnlem2lem2  14605  lcmfunsnlem2  14606  coprmprod  14671  coprmproddvdslem  14672  nnnn0modprm0  14750  vdwapun  14917  ramubcl  14969  xpsfrnel2  15464  mreexmrid  15542  lubun  16362  symgextf1  17055  gsumzsplit  17553  gsumzunsnd  17581  gsumunsnfd  17582  dprddisj2  17665  dmdprdsplit2lem  17671  dmdprdsplit2  17672  dprdsplit  17674  mplcoe1  18682  mplcoe5  18685  evlslem4  18724  mdetunilem9  19637  maducoeval2  19657  madugsum  19660  clslp  20156  islpi  20157  restntr  20190  pnfnei  20228  mnfnei  20229  iuncon  20435  refun0  20522  xkoptsub  20661  ptunhmeo  20815  fbun  20847  filcon  20890  fixufil  20929  ufildr  20938  alexsubALTlem2  21055  alexsubALTlem3  21056  alexsubALTlem4  21057  tsmssplit  21158  xrtgioo  21816  reconnlem2  21837  iccpnfcnv  21964  iccpnfhmeo  21965  rrxcph  22343  rrxdstprj1  22355  mbfss  22594  mbfmax  22597  itg2splitlem  22698  itg2split  22699  iblss2  22755  itgsplit  22785  limcdif  22823  ellimc2  22824  limcmpt  22830  limcres  22833  limccnp  22838  limccnp2  22839  limcco  22840  rollelem  22933  dvivthlem1  22952  dvne0  22955  lhop  22960  degltlem1  23013  ply1rem  23106  fta1glem2  23109  plypf1  23158  plyaddlem1  23159  plymullem1  23160  plycj  23223  ofmulrt  23227  taylfval  23306  abelthlem2  23379  abelthlem3  23380  reasinsin  23814  scvxcvx  23903  ppinprm  24071  chtnprm  24073  dchrfi  24175  lgsdir2  24248  usgraexmplef  25120  vdgrf  25618  vdgrun  25621  vdgrfiun  25622  vdgfrgragt2  25747  frgrawopreglem2  25765  shunssi  27013  atomli  28027  atoml2i  28028  isoun  28278  fzsplit3  28370  eliccioo  28401  ordtconlem1  28732  xrge0iifcnv  28741  xrge0iifiso  28743  xrge0iifhom  28745  esumsplit  28876  esumpad2  28879  measvuni  29038  sxbrsigalem0  29095  bnj1138  29602  bnj1137  29806  subfacp1lem4  29908  subfacp1lem5  29909  kur14lem7  29937  mrsubcv  30150  mclsax  30209  dftrpred3g  30475  brcup  30705  refssfne  31013  bj-eltag  31533  bj-0eltag  31534  bj-sngltag  31539  bj-projun  31550  tan2h  31895  poimirlem2  31900  poimirlem8  31906  poimirlem18  31916  poimirlem21  31919  poimirlem22  31920  poimirlem23  31921  poimirlem24  31922  poimirlem25  31923  poimirlem27  31925  poimirlem29  31927  poimirlem31  31929  poimirlem32  31930  ftc1anclem1  31975  ftc1anclem5  31979  dvasin  31986  dvacos  31987  eqfnun  32006  smprngopr  32243  elpadd  33327  paddval0  33338  hdmaplem4  35305  mapdh9a  35321  lzunuz  35573  jm2.23  35815  unxpwdom3  35917  hbtlem5  35951  rp-fakeinunass  36124  frege133d  36261  frege83  36444  frege131  36492  frege133  36494  radcnvrat  36565  bccbc  36596  undif3VD  37184  iunconlem2  37237  fnchoice  37255  elunnel2  37265  unima  37322  limciccioolb  37565  limcicciooub  37581  icccncfext  37629  cncfiooicclem1  37635  fourierdlem70  37904  fourierdlem80  37914  fourierdlem93  37927  fourierdlem101  37935  sge0split  38083  el1fzopredsuc  38478  iccpartltu  38495  iccpartgtl  38496  iccpartgt  38497  iccpartleu  38498  iccpartgel  38499  nnsum4primeseven  38651  nnsum4primesevenALTV  38652  wtgoldbnnsum4prm  38653  bgoldbnnsum3prm  38655  bgoldbtbndlem3  38658  bgoldbtbnd  38660