Theorem elun 3631

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 377	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2526	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2526	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
7	5, 6	orbi12d 707	. . 3 |- ( x = A -> ( ( x e. B \/ x e. C ) <-> ( A e. B \/ A e. C ) ) )
8		df-un 3466	. . 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 351	1 |- ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) )

Syntax hints:   <-> wb 184   \/ wo 366   = wceq 1398   e. wcel 1823   _Vcvv 3106   u. cun 3459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-un 3466

This theorem is referenced by:  uneqri  3632  uncom  3634  uneq1  3637  unass  3647  ssun1  3653  unss1  3659  ssequn1  3660  unss  3664  rexun  3670  ralunb  3671  elsymdif  3720  symdif2  3723  indi  3741  undi  3742  unineq  3745  undif3  3756  rabun2  3774  reuun2  3778  undif4  3871  ssundif  3899  dfpr2  4031  elpwunsn  4057  eltpg  4058  pwpr  4231  pwtp  4232  uniun  4254  intun  4304  iinun2  4381  iunun  4399  iunxun  4400  iinuni  4402  brun  4487  pwunss  4774  pwssun  4775  elsuci  4933  elsucg  4934  elsuc2g  4935  opthprc  5036  xpundi  5041  xpundir  5042  difxp  5416  sossfld  5438  funun  5612  mptun  5694  unpreima  5989  suceloni  6621  ordsucun  6633  fnse  6890  reldmtpos  6955  dftpos4  6966  tpostpos  6967  oarec  7203  brdom2  7538  unxpdomlem3  7719  domunfican  7785  dfsup2  7894  dfsup2OLD  7895  wemapso2OLD  7969  wemapso2lem  7970  unwdomg  8002  unxpwdom2  8006  cantnfp1lem3  8090  cantnfp1lem3OLD  8116  rankunb  8259  iscard3  8465  kmlem2  8522  ssfin4  8681  dffin7-2  8769  fin1a2lem11  8781  fin1a2lem12  8782  cfpwsdom  8950  elgch  8989  fpwwe2lem13  9009  canthp1lem2  9020  gch2  9042  elnn0  10793  un0addcl  10825  un0mulcl  10826  ltxr  11327  elxr  11328  xrsupexmnf  11499  xrinfmexpnf  11500  supxrun  11510  ixxun  11548  difreicc  11655  iccsplit  11656  fzsplit2  11713  elfzp1  11734  uzsplit  11754  elfzp12  11761  fzosplit  11835  fzouzsplit  11837  elfzonlteqm1  11872  fzosplitsni  11901  hashnn0pnf  12397  hashf1lem2  12489  hash2pwpr  12503  pr2pwpr  12504  ccatrn  12595  cats1un  12692  fsumsplit  13644  sumsplit  13665  fprodsplit  13852  rpnnen2  14043  saddisjlem  14198  nnnn0modprm0  14415  vdwapun  14576  ramubcl  14620  xpsfrnel2  15054  mreexmrid  15132  lubun  15952  symgextf1  16645  gsumzsplit  17143  gsumzsplitOLD  17144  gsumzunsnd  17178  gsumunsnfd  17179  dprddisj2  17282  dprddisj2OLD  17283  dmdprdsplit2lem  17289  dmdprdsplit2  17290  dprdsplit  17292  mplcoe1  18322  mplcoe5  18326  mplcoe2OLD  18328  evlslem4OLD  18368  evlslem4  18369  mdetunilem9  19289  maducoeval2  19309  madugsum  19312  clslp  19816  islpi  19817  restntr  19850  pnfnei  19888  mnfnei  19889  iuncon  20095  refun0  20182  xkoptsub  20321  ptunhmeo  20475  fbun  20507  filcon  20550  fixufil  20589  ufildr  20598  alexsubALTlem2  20714  alexsubALTlem3  20715  alexsubALTlem4  20716  tsmssplit  20820  xrtgioo  21477  reconnlem2  21498  iccpnfcnv  21610  iccpnfhmeo  21611  rrxcph  21990  rrxdstprj1  22002  mbfss  22219  mbfmax  22222  itg2splitlem  22321  itg2split  22322  iblss2  22378  itgsplit  22408  limcdif  22446  ellimc2  22447  limcmpt  22453  limcres  22456  limccnp  22461  limccnp2  22462  limcco  22463  rollelem  22556  dvivthlem1  22575  dvne0  22578  lhop  22583  degltlem1  22638  ply1rem  22730  fta1glem2  22733  plypf1  22775  plyaddlem1  22776  plymullem1  22777  plycj  22840  ofmulrt  22844  taylfval  22920  abelthlem2  22993  abelthlem3  22994  reasinsin  23424  scvxcvx  23513  ppinprm  23624  chtnprm  23626  dchrfi  23728  lgsdir2  23801  usgraexmpl  24603  vdgrf  25100  vdgrun  25103  vdgrfiun  25104  vdgfrgragt2  25229  frgrawopreglem2  25247  shunssi  26484  atomli  27499  atoml2i  27500  isoun  27748  fzsplit3  27833  eliccioo  27861  ordtconlem1  28141  xrge0iifcnv  28150  xrge0iifiso  28152  xrge0iifhom  28154  esumsplit  28282  esumpad2  28285  measvuni  28422  sxbrsigalem0  28479  subfacp1lem4  28891  subfacp1lem5  28892  kur14lem7  28920  mrsubcv  29134  mclsax  29193  dftrpred3g  29556  wfrlem14  29596  wfrlem15  29597  brcup  29817  tan2h  30287  ftc1anclem1  30330  ftc1anclem5  30334  dvasin  30343  dvacos  30344  refssfne  30416  eqfnun  30452  smprngopr  30689  lzunuz  30940  jm2.23  31177  unxpwdom3  31280  hbtlem5  31318  radcnvrat  31436  bccbc  31491  fnchoice  31644  elunnel1  31654  elunnel2  31655  unima  31681  limciccioolb  31866  limcicciooub  31882  icccncfext  31929  cncfiooicclem1  31935  fourierdlem70  32198  fourierdlem80  32208  fourierdlem93  32221  fourierdlem101  32229  undif3VD  34083  iunconlem2  34136  bnj1138  34248  bnj1137  34452  bj-eltag  34936  bj-0eltag  34937  bj-sngltag  34942  bj-projun  34953  elpadd  35920  paddval0  35931  hdmaplem4  37898  mapdh9a  37914  rp-fakeinunass  38154