MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elun Unicode version

Theorem elun 3329
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.
StepHypRef Expression
1 elex 2809 . 2  |-  ( A  e.  ( B  u.  C )  ->  A  e.  _V )
2 elex 2809 . . 3  |-  ( A  e.  B  ->  A  e.  _V )
3 elex 2809 . . 3  |-  ( A  e.  C  ->  A  e.  _V )
42, 3jaoi 368 . 2  |-  ( ( A  e.  B  \/  A  e.  C )  ->  A  e.  _V )
5 eleq1 2356 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
6 eleq1 2356 . . . 4  |-  ( x  =  A  ->  (
x  e.  C  <->  A  e.  C ) )
75, 6orbi12d 690 . . 3  |-  ( x  =  A  ->  (
( x  e.  B  \/  x  e.  C
)  <->  ( A  e.  B  \/  A  e.  C ) ) )
8 df-un 3170 . . 3  |-  ( B  u.  C )  =  { x  |  ( x  e.  B  \/  x  e.  C ) }
97, 8elab2g 2929 . 2  |-  ( A  e.  _V  ->  ( A  e.  ( B  u.  C )  <->  ( A  e.  B  \/  A  e.  C ) ) )
101, 4, 9pm5.21nii 342 1  |-  ( A  e.  ( B  u.  C )  <->  ( A  e.  B  \/  A  e.  C ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    \/ wo 357    = wceq 1632    e. wcel 1696   _Vcvv 2801    u. cun 3163
This theorem is referenced by:  uneqri  3330  uncom  3332  uneq1  3335  unass  3345  ssun1  3351  unss1  3357  ssequn1  3358  unss  3362  rexun  3368  ralunb  3369  indi  3428  undi  3429  unineq  3432  undif3  3442  symdif2  3447  rabun2  3460  reuun2  3464  undif4  3524  ssundif  3550  dfpr2  3669  eltpg  3689  pwpr  3839  pwtp  3840  uniun  3862  intun  3910  iinun2  3984  iunun  3998  iunxun  3999  iinuni  4001  brun  4085  pwunss  4314  pwssun  4315  pwundifOLD  4317  elsuci  4474  elsucg  4475  elsuc2g  4476  trsuc2OLD  4493  elpwunsn  4584  suceloni  4620  ordsucun  4632  opthprc  4752  xpundi  4757  xpundir  4758  sossfld  5136  funun  5312  mptun  5390  unpreima  5667  difxp  6169  fnse  6248  reldmtpos  6258  dftpos4  6269  tpostpos  6270  oarec  6576  brdom2  6907  unxpdomlem3  7085  domunfican  7145  dfsup2  7211  dfsup2OLD  7212  wemapso2  7283  unwdomg  7314  unxpwdom2  7318  sucprcreg  7329  cantnfp1lem3  7398  rankunb  7538  iscard3  7736  kmlem2  7793  ssfin4  7952  dffin7-2  8040  fin1a2lem11  8052  fin1a2lem12  8053  cfpwsdom  8222  elgch  8260  fpwwe2lem13  8280  canthp1lem2  8291  gch2  8317  elnn0  9983  un0addcl  10013  un0mulcl  10014  ltxr  10473  elxr  10474  xrsupexmnf  10639  xrinfmexpnf  10640  supxrun  10650  ixxun  10688  difreicc  10783  iccsplit  10784  fzsplit2  10831  elfzp1  10852  uzsplit  10871  elfzp12  10877  fzosplit  10915  fzouzsplit  10917  fzosplitsni  10937  hashf1lem2  11410  cats1un  11492  fsumsplit  12228  sumsplit  12247  rpnnen2  12520  saddisjlem  12671  vdwapun  13037  ramubcl  13081  xpsfrnel2  13483  mreexmrid  13561  lubun  14243  gsumzsplit  15222  gsumunsn  15237  dprddisj2  15290  dmdprdsplit2lem  15296  dmdprdsplit2  15297  dprdsplit  15299  mplcoe1  16225  mplcoe2  16227  evlslem4  16261  clslp  16895  islpi  16896  restntr  16928  pnfnei  16966  mnfnei  16967  iuncon  17170  xkoptsub  17364  ptunhmeo  17515  fbun  17551  filcon  17594  fixufil  17633  ufildr  17642  alexsubALTlem2  17758  alexsubALTlem3  17759  alexsubALTlem4  17760  tsmssplit  17850  xrtgioo  18328  reconnlem2  18348  iccpnfcnv  18458  iccpnfhmeo  18459  mbfss  19017  mbfmax  19020  itg2splitlem  19119  itg2split  19120  iblss2  19176  itgsplit  19206  limcdif  19242  ellimc2  19243  limcmpt  19249  limcres  19252  limccnp  19257  limccnp2  19258  limcco  19259  rollelem  19352  dvivthlem1  19371  dvne0  19374  lhop  19379  degltlem1  19474  ply1rem  19565  fta1glem2  19568  plypf1  19610  plyaddlem1  19611  plymullem1  19612  plycj  19674  ofmulrt  19678  taylfval  19754  abelthlem2  19824  abelthlem3  19825  reasinsin  20208  scvxcvx  20296  ppinprm  20406  chtnprm  20408  dchrfi  20510  lgsdir2  20583  shunssi  21963  atomli  22978  atoml2i  22979  fzsplit3  23047  eliccioo  23131  isoun  23257  xrge0iifcnv  23330  xrge0iifiso  23332  xrge0iifhom  23334  esumsplit  23446  measvuni  23557  subfacp1lem4  23729  subfacp1lem5  23730  kur14lem7  23758  vdgrun  23908  dftrpred3g  24307  wfrlem14  24340  wfrlem15  24341  elsymdif  24438  brcup  24549  domrngref  25163  basexre  25625  intvconlem1  25806  vtarsuelt  25998  fnckle  26148  pfsubkl  26150  pgapspf2  26156  refssfne  26397  eqfnun  26490  smprngopr  26780  lzunuz  26950  jm2.23  27192  unxpwdom3  27359  hbtlem5  27435  fnchoice  27803  usgraex0elv  28262  usgraex1elv  28263  usgraex2elv  28264  usgraex3elv  28265  usgraexmpl  28267  undif3VD  28974  bnj1138  29136  bnj1137  29341  lubunNEW  29785  elpadd  30610  paddval0  30621  hdmaplem4  32586  mapdh9a  32602
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170
  Copyright terms: Public domain W3C validator