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

Theorem elun 3226
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
StepHypRef Expression
1 elex 2735 . 2  |-  ( A  e.  ( B  u.  C )  ->  A  e.  _V )
2 elex 2735 . . 3  |-  ( A  e.  B  ->  A  e.  _V )
3 elex 2735 . . 3  |-  ( A  e.  C  ->  A  e.  _V )
42, 3jaoi 370 . 2  |-  ( ( A  e.  B  \/  A  e.  C )  ->  A  e.  _V )
5 eleq1 2313 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
6 eleq1 2313 . . . 4  |-  ( x  =  A  ->  (
x  e.  C  <->  A  e.  C ) )
75, 6orbi12d 693 . . 3  |-  ( x  =  A  ->  (
( x  e.  B  \/  x  e.  C
)  <->  ( A  e.  B  \/  A  e.  C ) ) )
8 df-un 3083 . . 3  |-  ( B  u.  C )  =  { x  |  ( x  e.  B  \/  x  e.  C ) }
97, 8elab2g 2853 . 2  |-  ( A  e.  _V  ->  ( A  e.  ( B  u.  C )  <->  ( A  e.  B  \/  A  e.  C ) ) )
101, 4, 9pm5.21nii 344 1  |-  ( A  e.  ( B  u.  C )  <->  ( A  e.  B  \/  A  e.  C ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    \/ wo 359    = wceq 1619    e. wcel 1621   _Vcvv 2727    u. cun 3076
This theorem is referenced by:  uneqri  3227  uncom  3229  uneq1  3232  unass  3242  ssun1  3248  unss1  3254  ssequn1  3255  unss  3259  rexun  3263  ralunb  3264  indi  3322  undi  3323  unineq  3326  undif3  3336  symdif2  3341  rabun2  3354  reuun2  3358  undif4  3418  ssundif  3443  dfpr2  3560  eltpg  3580  pwpr  3723  pwtp  3724  uniun  3746  intun  3792  iinun2  3866  iunun  3880  iunxun  3881  iinuni  3883  brun  3966  pwunss  4191  pwssun  4192  pwundifOLD  4194  elsuci  4351  elsucg  4352  elsuc2g  4353  trsuc2OLD  4370  elpwunsn  4459  suceloni  4495  ordsucun  4507  opthprc  4643  xpundi  4648  xpundir  4649  sossfld  5027  funun  5153  mptun  5231  unpreima  5503  difxp  6005  fnse  6084  reldmtpos  6094  dftpos4  6105  tpostpos  6106  oarec  6446  brdom2  6777  unxpdomlem3  6954  domunfican  7014  dfsup2  7079  dfsup2OLD  7080  wemapso2  7151  unwdomg  7182  unxpwdom2  7186  sucprcreg  7197  cantnfp1lem3  7266  rankunb  7406  iscard3  7604  kmlem2  7661  ssfin4  7820  dffin7-2  7908  fin1a2lem11  7920  fin1a2lem12  7921  cfpwsdom  8086  elgch  8124  fpwwe2lem13  8144  canthp1lem2  8155  gch2  8181  elnn0  9846  un0addcl  9876  un0mulcl  9877  ltxr  10336  elxr  10337  xrsupexmnf  10501  xrinfmexpnf  10502  supxrun  10512  ixxun  10550  difreicc  10645  iccsplit  10646  fzsplit2  10693  elfzp1  10714  uzsplit  10733  elfzp12  10739  fzosplit  10777  fzouzsplit  10779  fzosplitsni  10799  hashf1lem2  11271  cats1un  11353  fsumsplit  12089  sumsplit  12108  rpnnen2  12378  saddisjlem  12529  vdwapun  12895  ramubcl  12939  xpsfrnel2  13341  lubun  14071  gsumzsplit  15041  gsumunsn  15056  dprddisj2  15109  dmdprdsplit2lem  15115  dmdprdsplit2  15116  dprdsplit  15118  mplcoe1  16041  mplcoe2  16043  evlslem4  16077  clslp  16711  islpi  16712  restntr  16744  pnfnei  16782  mnfnei  16783  iuncon  16986  xkoptsub  17180  ptunhmeo  17331  fbun  17367  filcon  17410  fixufil  17449  ufildr  17458  alexsubALTlem2  17574  alexsubALTlem3  17575  alexsubALTlem4  17576  tsmssplit  17666  xrtgioo  18144  reconnlem2  18164  iccpnfcnv  18274  iccpnfhmeo  18275  mbfss  18833  mbfmax  18836  itg2splitlem  18935  itg2split  18936  iblss2  18992  itgsplit  19022  limcdif  19058  ellimc2  19059  limcmpt  19065  limcres  19068  limccnp  19073  limccnp2  19074  limcco  19075  rollelem  19168  dvivthlem1  19187  dvne0  19190  lhop  19195  degltlem1  19290  ply1rem  19381  fta1glem2  19384  plypf1  19426  plyaddlem1  19427  plymullem1  19428  plycj  19490  ofmulrt  19494  taylfval  19570  abelthlem2  19640  abelthlem3  19641  reasinsin  20024  scvxcvx  20112  ppinprm  20222  chtnprm  20224  dchrfi  20326  lgsdir2  20399  shunssi  21777  atomli  22792  atoml2i  22793  subfacp1lem4  22885  subfacp1lem5  22886  kur14lem7  22914  vdgrun  23064  dftrpred3g  23404  wfrlem14  23437  wfrlem15  23438  elsymdif  23542  brcup  23652  domrngref  24225  basexre  24688  intvconlem1  24869  vtarsuelt  25061  fnckle  25211  pfsubkl  25213  pgapspf2  25219  refssfne  25460  eqfnun  25553  smprngopr  25843  lzunuz  26013  jm2.23  26255  unxpwdom3  26422  hbtlem5  26498  undif3VD  27348  bnj1138  27509  bnj1137  27714  lubunNEW  27852  elpadd  28677  paddval0  28688  hdmaplem4  30653  mapdh9a  30669
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-un 3083
  Copyright terms: Public domain W3C validator