Theorem elun 3565

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 3040	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 3040	. . 3 |- ( A e. B -> A e. _V )
3		elex 3040	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 386	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2537	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2537	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
7	5, 6	orbi12d 724	. . 3 |- ( x = A -> ( ( x e. B \/ x e. C ) <-> ( A e. B \/ A e. C ) ) )
8		df-un 3395	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 3175	. 2 |- ( A e. _V -> ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) ) )
10	1, 4, 9	pm5.21nii 360	1 |- ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) )

Syntax hints:   <-> wb 189   \/ wo 375   = wceq 1452   e. wcel 1904   _Vcvv 3031   u. cun 3388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-un 3395

This theorem is referenced by:  elunnel1  3566  uneqri  3567  uncom  3569  uneq1  3572  unass  3582  ssun1  3588  unss1  3594  ssequn1  3595  unss  3599  rexun  3605  ralunb  3606  elsymdif  3659  symdif2  3662  indi  3680  undi  3681  unineq  3684  undif3  3695  rabun2  3713  reuun2  3717  undif4  3825  ssundif  3842  dfpr2  3974  elpwunsn  4003  eltpg  4005  pwpr  4186  pwtp  4187  uniun  4209  intun  4258  iinun2  4335  iunun  4353  iunxun  4354  iinuni  4358  brun  4444  pwunss  4744  pwssun  4745  opthprc  4887  xpundi  4892  xpundir  4893  difxp  5267  sossfld  5289  elsuci  5496  elsucg  5497  elsuc2g  5498  funun  5631  mptun  5719  unpreima  6021  suceloni  6659  ordsucun  6671  fnse  6932  reldmtpos  6999  dftpos4  7010  tpostpos  7011  wfrlem14  7067  wfrlem15  7068  oarec  7281  brdom2  7617  unxpdomlem3  7796  domunfican  7862  dfsup2  7976  wemapso2lem  8085  unwdomg  8117  unxpwdom2  8121  cantnfp1lem3  8203  rankunb  8339  iscard3  8542  kmlem2  8599  ssfin4  8758  dffin7-2  8846  fin1a2lem11  8858  fin1a2lem12  8859  cfpwsdom  9027  elgch  9065  fpwwe2lem13  9085  canthp1lem2  9096  gch2  9118  elnn0  10895  un0addcl  10927  un0mulcl  10928  ltxr  11438  elxr  11439  xrsupexmnf  11615  xrinfmexpnf  11616  supxrun  11626  ixxun  11676  difreicc  11790  iccsplit  11791  fzsplit2  11850  elfzp1  11872  uzsplit  11892  elfzp12  11899  fzosplit  11978  fzouzsplit  11980  elfzonlteqm1  12018  fzosplitsni  12050  hashnn0pnf  12563  hashf1lem2  12660  hash2pwpr  12676  pr2pwpr  12677  ccatrn  12784  cats1un  12886  fsumsplit  13883  sumsplit  13906  fprodsplit  14097  rpnnen2  14355  saddisjlem  14517  lcmfunsnlem1  14689  lcmfunsnlem2lem1  14690  lcmfunsnlem2lem2  14691  lcmfunsnlem2  14692  coprmprod  14757  coprmproddvdslem  14758  nnnn0modprm0  14836  vdwapun  15003  ramubcl  15055  xpsfrnel2  15549  mreexmrid  15627  lubun  16447  symgextf1  17140  gsumzsplit  17638  gsumzunsnd  17666  gsumunsnfd  17667  dprddisj2  17750  dmdprdsplit2lem  17756  dmdprdsplit2  17757  dprdsplit  17759  mplcoe1  18766  mplcoe5  18769  evlslem4  18808  mdetunilem9  19722  maducoeval2  19742  madugsum  19745  clslp  20241  islpi  20242  restntr  20275  pnfnei  20313  mnfnei  20314  iuncon  20520  refun0  20607  xkoptsub  20746  ptunhmeo  20900  fbun  20933  filcon  20976  fixufil  21015  ufildr  21024  alexsubALTlem2  21141  alexsubALTlem3  21142  alexsubALTlem4  21143  tsmssplit  21244  xrtgioo  21902  reconnlem2  21923  iccpnfcnv  22050  iccpnfhmeo  22051  rrxcph  22429  rrxdstprj1  22441  mbfss  22681  mbfmax  22684  itg2splitlem  22785  itg2split  22786  iblss2  22842  itgsplit  22872  limcdif  22910  ellimc2  22911  limcmpt  22917  limcres  22920  limccnp  22925  limccnp2  22926  limcco  22927  rollelem  23020  dvivthlem1  23039  dvne0  23042  lhop  23047  degltlem1  23100  ply1rem  23193  fta1glem2  23196  plypf1  23245  plyaddlem1  23246  plymullem1  23247  plycj  23310  ofmulrt  23314  taylfval  23393  abelthlem2  23466  abelthlem3  23467  reasinsin  23901  scvxcvx  23990  ppinprm  24158  chtnprm  24160  dchrfi  24262  lgsdir2  24335  usgraexmplef  25207  vdgrf  25705  vdgrun  25708  vdgrfiun  25709  vdgfrgragt2  25834  frgrawopreglem2  25852  shunssi  27102  atomli  28116  atoml2i  28117  isoun  28357  fzsplit3  28445  eliccioo  28475  ordtconlem1  28804  xrge0iifcnv  28813  xrge0iifiso  28815  xrge0iifhom  28817  esumsplit  28948  esumpad2  28951  measvuni  29110  sxbrsigalem0  29166  bnj1138  29672  bnj1137  29876  subfacp1lem4  29978  subfacp1lem5  29979  kur14lem7  30007  mrsubcv  30220  mclsax  30279  dftrpred3g  30545  brcup  30777  refssfne  31085  bj-eltag  31641  bj-0eltag  31642  bj-sngltag  31647  bj-projun  31658  tan2h  32001  poimirlem2  32006  poimirlem8  32012  poimirlem18  32022  poimirlem21  32025  poimirlem22  32026  poimirlem23  32027  poimirlem24  32028  poimirlem25  32029  poimirlem27  32031  poimirlem29  32033  poimirlem31  32035  poimirlem32  32036  ftc1anclem1  32081  ftc1anclem5  32085  dvasin  32092  dvacos  32093  eqfnun  32112  smprngopr  32349  elpadd  33435  paddval0  33446  hdmaplem4  35413  mapdh9a  35429  lzunuz  35681  jm2.23  35922  unxpwdom3  36024  hbtlem5  36058  rp-fakeinunass  36231  frege133d  36428  frege83  36613  frege131  36661  frege133  36663  radcnvrat  36733  bccbc  36764  undif3VD  37342  iunconlem2  37395  fnchoice  37413  elunnel2  37423  unima  37502  limciccioolb  37798  limcicciooub  37814  icccncfext  37862  cncfiooicclem1  37868  fourierdlem70  38152  fourierdlem80  38162  fourierdlem93  38175  fourierdlem101  38183  sge0split  38365  el1fzopredsuc  38867  iccpartltu  38884  iccpartgtl  38885  iccpartgt  38886  iccpartleu  38887  iccpartgel  38888  nnsum4primeseven  39040  nnsum4primesevenALTV  39041  wtgoldbnnsum4prm  39042  bgoldbnnsum3prm  39044  bgoldbtbndlem3  39047  bgoldbtbnd  39049  elfzr  39212  elfzo0l  39213  elfzlmr  39214  elxnn0  39222  vtxdun  39704  eucrct2eupth  40157