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

Theorem elun 3316
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 2796 . 2  |-  ( A  e.  ( B  u.  C )  ->  A  e.  _V )
2 elex 2796 . . 3  |-  ( A  e.  B  ->  A  e.  _V )
3 elex 2796 . . 3  |-  ( A  e.  C  ->  A  e.  _V )
42, 3jaoi 368 . 2  |-  ( ( A  e.  B  \/  A  e.  C )  ->  A  e.  _V )
5 eleq1 2343 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
6 eleq1 2343 . . . 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 3157 . . 3  |-  ( B  u.  C )  =  { x  |  ( x  e.  B  \/  x  e.  C ) }
97, 8elab2g 2916 . 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 1623    e. wcel 1684   _Vcvv 2788    u. cun 3150
This theorem is referenced by:  uneqri  3317  uncom  3319  uneq1  3322  unass  3332  ssun1  3338  unss1  3344  ssequn1  3345  unss  3349  rexun  3355  ralunb  3356  indi  3415  undi  3416  unineq  3419  undif3  3429  symdif2  3434  rabun2  3447  reuun2  3451  undif4  3511  ssundif  3537  dfpr2  3656  eltpg  3676  pwpr  3823  pwtp  3824  uniun  3846  intun  3894  iinun2  3968  iunun  3982  iunxun  3983  iinuni  3985  brun  4069  pwunss  4298  pwssun  4299  pwundifOLD  4301  elsuci  4458  elsucg  4459  elsuc2g  4460  trsuc2OLD  4477  elpwunsn  4568  suceloni  4604  ordsucun  4616  opthprc  4736  xpundi  4741  xpundir  4742  sossfld  5120  funun  5296  mptun  5374  unpreima  5651  difxp  6153  fnse  6232  reldmtpos  6242  dftpos4  6253  tpostpos  6254  oarec  6560  brdom2  6891  unxpdomlem3  7069  domunfican  7129  dfsup2  7195  dfsup2OLD  7196  wemapso2  7267  unwdomg  7298  unxpwdom2  7302  sucprcreg  7313  cantnfp1lem3  7382  rankunb  7522  iscard3  7720  kmlem2  7777  ssfin4  7936  dffin7-2  8024  fin1a2lem11  8036  fin1a2lem12  8037  cfpwsdom  8206  elgch  8244  fpwwe2lem13  8264  canthp1lem2  8275  gch2  8301  elnn0  9967  un0addcl  9997  un0mulcl  9998  ltxr  10457  elxr  10458  xrsupexmnf  10623  xrinfmexpnf  10624  supxrun  10634  ixxun  10672  difreicc  10767  iccsplit  10768  fzsplit2  10815  elfzp1  10836  uzsplit  10855  elfzp12  10861  fzosplit  10899  fzouzsplit  10901  fzosplitsni  10921  hashf1lem2  11394  cats1un  11476  fsumsplit  12212  sumsplit  12231  rpnnen2  12504  saddisjlem  12655  vdwapun  13021  ramubcl  13065  xpsfrnel2  13467  mreexmrid  13545  lubun  14227  gsumzsplit  15206  gsumunsn  15221  dprddisj2  15274  dmdprdsplit2lem  15280  dmdprdsplit2  15281  dprdsplit  15283  mplcoe1  16209  mplcoe2  16211  evlslem4  16245  clslp  16879  islpi  16880  restntr  16912  pnfnei  16950  mnfnei  16951  iuncon  17154  xkoptsub  17348  ptunhmeo  17499  fbun  17535  filcon  17578  fixufil  17617  ufildr  17626  alexsubALTlem2  17742  alexsubALTlem3  17743  alexsubALTlem4  17744  tsmssplit  17834  xrtgioo  18312  reconnlem2  18332  iccpnfcnv  18442  iccpnfhmeo  18443  mbfss  19001  mbfmax  19004  itg2splitlem  19103  itg2split  19104  iblss2  19160  itgsplit  19190  limcdif  19226  ellimc2  19227  limcmpt  19233  limcres  19236  limccnp  19241  limccnp2  19242  limcco  19243  rollelem  19336  dvivthlem1  19355  dvne0  19358  lhop  19363  degltlem1  19458  ply1rem  19549  fta1glem2  19552  plypf1  19594  plyaddlem1  19595  plymullem1  19596  plycj  19658  ofmulrt  19662  taylfval  19738  abelthlem2  19808  abelthlem3  19809  reasinsin  20192  scvxcvx  20280  ppinprm  20390  chtnprm  20392  dchrfi  20494  lgsdir2  20567  shunssi  21947  atomli  22962  atoml2i  22963  fzsplit3  23031  eliccioo  23115  isoun  23242  xrge0iifcnv  23315  xrge0iifiso  23317  xrge0iifhom  23319  esumsplit  23431  measvuni  23542  subfacp1lem4  23714  subfacp1lem5  23715  kur14lem7  23743  vdgrun  23893  dftrpred3g  24236  wfrlem14  24269  wfrlem15  24270  elsymdif  24367  brcup  24478  domrngref  25060  basexre  25522  intvconlem1  25703  vtarsuelt  25895  fnckle  26045  pfsubkl  26047  pgapspf2  26053  refssfne  26294  eqfnun  26387  smprngopr  26677  lzunuz  26847  jm2.23  27089  unxpwdom3  27256  hbtlem5  27332  fnchoice  27700  usgraex0elv  28128  usgraex1elv  28129  usgraex2elv  28130  usgraex3elv  28131  usgraexmpl  28133  undif3VD  28658  bnj1138  28820  bnj1137  29025  lubunNEW  29163  elpadd  29988  paddval0  29999  hdmaplem4  31964  mapdh9a  31980
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157
  Copyright terms: Public domain W3C validator