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

Theorem elun 3291
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 2771 . 2  |-  ( A  e.  ( B  u.  C )  ->  A  e.  _V )
2 elex 2771 . . 3  |-  ( A  e.  B  ->  A  e.  _V )
3 elex 2771 . . 3  |-  ( A  e.  C  ->  A  e.  _V )
42, 3jaoi 370 . 2  |-  ( ( A  e.  B  \/  A  e.  C )  ->  A  e.  _V )
5 eleq1 2318 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
6 eleq1 2318 . . . 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 3132 . . 3  |-  ( B  u.  C )  =  { x  |  ( x  e.  B  \/  x  e.  C ) }
97, 8elab2g 2891 . 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 2763    u. cun 3125
This theorem is referenced by:  uneqri  3292  uncom  3294  uneq1  3297  unass  3307  ssun1  3313  unss1  3319  ssequn1  3320  unss  3324  rexun  3330  ralunb  3331  indi  3390  undi  3391  unineq  3394  undif3  3404  symdif2  3409  rabun2  3422  reuun2  3426  undif4  3486  ssundif  3512  dfpr2  3630  eltpg  3650  pwpr  3797  pwtp  3798  uniun  3820  intun  3868  iinun2  3942  iunun  3956  iunxun  3957  iinuni  3959  brun  4043  pwunss  4270  pwssun  4271  pwundifOLD  4273  elsuci  4430  elsucg  4431  elsuc2g  4432  trsuc2OLD  4449  elpwunsn  4540  suceloni  4576  ordsucun  4588  opthprc  4724  xpundi  4729  xpundir  4730  sossfld  5108  funun  5234  mptun  5312  unpreima  5585  difxp  6087  fnse  6166  reldmtpos  6176  dftpos4  6187  tpostpos  6188  oarec  6528  brdom2  6859  unxpdomlem3  7037  domunfican  7097  dfsup2  7163  dfsup2OLD  7164  wemapso2  7235  unwdomg  7266  unxpwdom2  7270  sucprcreg  7281  cantnfp1lem3  7350  rankunb  7490  iscard3  7688  kmlem2  7745  ssfin4  7904  dffin7-2  7992  fin1a2lem11  8004  fin1a2lem12  8005  cfpwsdom  8174  elgch  8212  fpwwe2lem13  8232  canthp1lem2  8243  gch2  8269  elnn0  9934  un0addcl  9964  un0mulcl  9965  ltxr  10424  elxr  10425  xrsupexmnf  10589  xrinfmexpnf  10590  supxrun  10600  ixxun  10638  difreicc  10733  iccsplit  10734  fzsplit2  10781  elfzp1  10802  uzsplit  10821  elfzp12  10827  fzosplit  10865  fzouzsplit  10867  fzosplitsni  10887  hashf1lem2  11359  cats1un  11441  fsumsplit  12177  sumsplit  12196  rpnnen2  12466  saddisjlem  12617  vdwapun  12983  ramubcl  13027  xpsfrnel2  13429  mreexmrid  13507  lubun  14189  gsumzsplit  15168  gsumunsn  15183  dprddisj2  15236  dmdprdsplit2lem  15242  dmdprdsplit2  15243  dprdsplit  15245  mplcoe1  16171  mplcoe2  16173  evlslem4  16207  clslp  16841  islpi  16842  restntr  16874  pnfnei  16912  mnfnei  16913  iuncon  17116  xkoptsub  17310  ptunhmeo  17461  fbun  17497  filcon  17540  fixufil  17579  ufildr  17588  alexsubALTlem2  17704  alexsubALTlem3  17705  alexsubALTlem4  17706  tsmssplit  17796  xrtgioo  18274  reconnlem2  18294  iccpnfcnv  18404  iccpnfhmeo  18405  mbfss  18963  mbfmax  18966  itg2splitlem  19065  itg2split  19066  iblss2  19122  itgsplit  19152  limcdif  19188  ellimc2  19189  limcmpt  19195  limcres  19198  limccnp  19203  limccnp2  19204  limcco  19205  rollelem  19298  dvivthlem1  19317  dvne0  19320  lhop  19325  degltlem1  19420  ply1rem  19511  fta1glem2  19514  plypf1  19556  plyaddlem1  19557  plymullem1  19558  plycj  19620  ofmulrt  19624  taylfval  19700  abelthlem2  19770  abelthlem3  19771  reasinsin  20154  scvxcvx  20242  ppinprm  20352  chtnprm  20354  dchrfi  20456  lgsdir2  20529  shunssi  21907  atomli  22922  atoml2i  22923  fzsplit3  22991  subfacp1lem4  23086  subfacp1lem5  23087  kur14lem7  23115  vdgrun  23265  dftrpred3g  23605  wfrlem14  23638  wfrlem15  23639  elsymdif  23743  brcup  23853  domrngref  24426  basexre  24889  intvconlem1  25070  vtarsuelt  25262  fnckle  25412  pfsubkl  25414  pgapspf2  25420  refssfne  25661  eqfnun  25754  smprngopr  26044  lzunuz  26214  jm2.23  26456  unxpwdom3  26623  hbtlem5  26699  fnchoice  27068  undif3VD  27708  bnj1138  27869  bnj1137  28074  lubunNEW  28330  elpadd  29155  paddval0  29166  hdmaplem4  31131  mapdh9a  31147
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 1927  ax-ext 2239
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 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-un 3132
  Copyright terms: Public domain W3C validator