Theorem elun 3630

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 3104	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 3104	. . 3 |- ( A e. B -> A e. _V )
3		elex 3104	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 379	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2515	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2515	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
7	5, 6	orbi12d 709	. . 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 3234	. 2 |- ( A e. _V -> ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) ) )
10	1, 4, 9	pm5.21nii 353	1 |- ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) )

Syntax hints:   <-> wb 184   \/ wo 368   = wceq 1383   e. wcel 1804   _Vcvv 3095   u. cun 3459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-un 3466

This theorem is referenced by:  uneqri  3631  uncom  3633  uneq1  3636  unass  3646  ssun1  3652  unss1  3658  ssequn1  3659  unss  3663  rexun  3669  ralunb  3670  indi  3729  undi  3730  unineq  3733  undif3  3744  symdif2  3749  rabun2  3762  reuun2  3766  undif4  3869  ssundif  3897  dfpr2  4029  elpwunsn  4055  eltpg  4056  pwpr  4230  pwtp  4231  uniun  4253  intun  4304  iinun2  4381  iunun  4396  iunxun  4397  iinuni  4399  brun  4485  pwunss  4775  pwssun  4776  elsuci  4934  elsucg  4935  elsuc2g  4936  opthprc  5037  xpundi  5042  xpundir  5043  difxp  5421  sossfld  5444  funun  5620  mptun  5702  unpreima  5998  suceloni  6633  ordsucun  6645  fnse  6902  reldmtpos  6965  dftpos4  6976  tpostpos  6977  oarec  7213  brdom2  7547  unxpdomlem3  7728  domunfican  7795  dfsup2  7904  dfsup2OLD  7905  wemapso2OLD  7980  wemapso2lem  7981  unwdomg  8013  unxpwdom2  8017  sucprcregOLD  8029  cantnfp1lem3  8102  cantnfp1lem3OLD  8128  rankunb  8271  iscard3  8477  kmlem2  8534  ssfin4  8693  dffin7-2  8781  fin1a2lem11  8793  fin1a2lem12  8794  cfpwsdom  8962  elgch  9003  fpwwe2lem13  9023  canthp1lem2  9034  gch2  9056  elnn0  10803  un0addcl  10835  un0mulcl  10836  ltxr  11333  elxr  11334  xrsupexmnf  11505  xrinfmexpnf  11506  supxrun  11516  ixxun  11554  difreicc  11661  iccsplit  11662  fzsplit2  11719  elfzp1  11739  uzsplit  11759  elfzp12  11766  fzosplit  11837  fzouzsplit  11839  elfzonlteqm1  11870  fzosplitsni  11899  hashnn0pnf  12394  hashf1lem2  12484  hash2pwpr  12498  pr2pwpr  12499  ccatrn  12585  cats1un  12680  fsumsplit  13541  sumsplit  13562  rpnnen2  13836  saddisjlem  13991  nnnn0modprm0  14208  vdwapun  14369  ramubcl  14413  xpsfrnel2  14839  mreexmrid  14917  lubun  15627  symgextf1  16320  gsumzsplit  16818  gsumzsplitOLD  16819  gsumzunsnd  16856  gsumunsnfd  16857  dprddisj2  16961  dprddisj2OLD  16962  dmdprdsplit2lem  16968  dmdprdsplit2  16969  dprdsplit  16971  mplcoe1  18001  mplcoe5  18005  mplcoe2OLD  18007  evlslem4OLD  18047  evlslem4  18048  mdetunilem9  18995  maducoeval2  19015  madugsum  19018  clslp  19522  islpi  19523  restntr  19556  pnfnei  19594  mnfnei  19595  iuncon  19802  refun0  19889  xkoptsub  20028  ptunhmeo  20182  fbun  20214  filcon  20257  fixufil  20296  ufildr  20305  alexsubALTlem2  20421  alexsubALTlem3  20422  alexsubALTlem4  20423  tsmssplit  20527  xrtgioo  21184  reconnlem2  21205  iccpnfcnv  21317  iccpnfhmeo  21318  rrxcph  21697  rrxdstprj1  21709  mbfss  21926  mbfmax  21929  itg2splitlem  22028  itg2split  22029  iblss2  22085  itgsplit  22115  limcdif  22153  ellimc2  22154  limcmpt  22160  limcres  22163  limccnp  22168  limccnp2  22169  limcco  22170  rollelem  22263  dvivthlem1  22282  dvne0  22285  lhop  22290  degltlem1  22345  ply1rem  22437  fta1glem2  22440  plypf1  22482  plyaddlem1  22483  plymullem1  22484  plycj  22546  ofmulrt  22550  taylfval  22626  abelthlem2  22699  abelthlem3  22700  reasinsin  23099  scvxcvx  23187  ppinprm  23298  chtnprm  23300  dchrfi  23402  lgsdir2  23475  usgraexmpl  24273  vdgrf  24770  vdgrun  24773  vdgrfiun  24774  vdgfrgragt2  24899  frgrawopreglem2  24917  shunssi  26158  atomli  27173  atoml2i  27174  isoun  27392  fzsplit3  27471  eliccioo  27500  ordtconlem1  27779  xrge0iifcnv  27788  xrge0iifiso  27790  xrge0iifhom  27792  esumsplit  27936  measvuni  28058  sxbrsigalem0  28115  subfacp1lem4  28500  subfacp1lem5  28501  kur14lem7  28529  mrsubcv  28743  mclsax  28802  fprodsplit  29070  dftrpred3g  29291  wfrlem14  29331  wfrlem15  29332  elsymdif  29448  brcup  29564  tan2h  30022  ftc1anclem1  30065  ftc1anclem5  30069  dvasin  30078  dvacos  30079  refssfne  30151  eqfnun  30187  smprngopr  30424  lzunuz  30676  jm2.23  30913  unxpwdom3  31016  hbtlem5  31052  radcnvrat  31171  fnchoice  31358  elunnel1  31368  elunnel2  31369  unima  31391  limciccioolb  31535  limcicciooub  31551  icccncfext  31597  cncfiooicclem1  31603  fourierdlem70  31848  fourierdlem80  31858  fourierdlem93  31871  fourierdlem101  31879  undif3VD  33415  iunconlem2  33468  bnj1138  33580  bnj1137  33784  bj-eltag  34283  bj-0eltag  34284  bj-sngltag  34289  bj-projun  34300  elpadd  35263  paddval0  35274  hdmaplem4  37241  mapdh9a  37257  rp-fakeinunass  37443