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

Theorem elun 3317
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 ) )
Dummy variable  x is distinct from all other variables.

Proof of Theorem elun
StepHypRef Expression
1 elex 2797 . 2  |-  ( A  e.  ( B  u.  C )  ->  A  e.  _V )
2 elex 2797 . . 3  |-  ( A  e.  B  ->  A  e.  _V )
3 elex 2797 . . 3  |-  ( A  e.  C  ->  A  e.  _V )
42, 3jaoi 370 . 2  |-  ( ( A  e.  B  \/  A  e.  C )  ->  A  e.  _V )
5 eleq1 2344 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
6 eleq1 2344 . . . 4  |-  ( x  =  A  ->  (
x  e.  C  <->  A  e.  C ) )
75, 6orbi12d 692 . . 3  |-  ( x  =  A  ->  (
( x  e.  B  \/  x  e.  C
)  <->  ( A  e.  B  \/  A  e.  C ) ) )
8 df-un 3158 . . 3  |-  ( B  u.  C )  =  { x  |  ( x  e.  B  \/  x  e.  C ) }
97, 8elab2g 2917 . 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 1624    e. wcel 1685   _Vcvv 2789    u. cun 3151
This theorem is referenced by:  uneqri  3318  uncom  3320  uneq1  3323  unass  3333  ssun1  3339  unss1  3345  ssequn1  3346  unss  3350  rexun  3356  ralunb  3357  indi  3416  undi  3417  unineq  3420  undif3  3430  symdif2  3435  rabun2  3448  reuun2  3452  undif4  3512  ssundif  3538  dfpr2  3657  eltpg  3677  pwpr  3824  pwtp  3825  uniun  3847  intun  3895  iinun2  3969  iunun  3983  iunxun  3984  iinuni  3986  brun  4070  pwunss  4297  pwssun  4298  pwundifOLD  4300  elsuci  4457  elsucg  4458  elsuc2g  4459  trsuc2OLD  4476  elpwunsn  4567  suceloni  4603  ordsucun  4615  opthprc  4735  xpundi  4740  xpundir  4741  sossfld  5119  funun  5261  mptun  5339  unpreima  5612  difxp  6114  fnse  6193  reldmtpos  6203  dftpos4  6214  tpostpos  6215  oarec  6555  brdom2  6886  unxpdomlem3  7064  domunfican  7124  dfsup2  7190  dfsup2OLD  7191  wemapso2  7262  unwdomg  7293  unxpwdom2  7297  sucprcreg  7308  cantnfp1lem3  7377  rankunb  7517  iscard3  7715  kmlem2  7772  ssfin4  7931  dffin7-2  8019  fin1a2lem11  8031  fin1a2lem12  8032  cfpwsdom  8201  elgch  8239  fpwwe2lem13  8259  canthp1lem2  8270  gch2  8296  elnn0  9962  un0addcl  9992  un0mulcl  9993  ltxr  10452  elxr  10453  xrsupexmnf  10617  xrinfmexpnf  10618  supxrun  10628  ixxun  10666  difreicc  10761  iccsplit  10762  fzsplit2  10809  elfzp1  10830  uzsplit  10849  elfzp12  10855  fzosplit  10893  fzouzsplit  10895  fzosplitsni  10915  hashf1lem2  11388  cats1un  11470  fsumsplit  12206  sumsplit  12225  rpnnen2  12498  saddisjlem  12649  vdwapun  13015  ramubcl  13059  xpsfrnel2  13461  mreexmrid  13539  lubun  14221  gsumzsplit  15200  gsumunsn  15215  dprddisj2  15268  dmdprdsplit2lem  15274  dmdprdsplit2  15275  dprdsplit  15277  mplcoe1  16203  mplcoe2  16205  evlslem4  16239  clslp  16873  islpi  16874  restntr  16906  pnfnei  16944  mnfnei  16945  iuncon  17148  xkoptsub  17342  ptunhmeo  17493  fbun  17529  filcon  17572  fixufil  17611  ufildr  17620  alexsubALTlem2  17736  alexsubALTlem3  17737  alexsubALTlem4  17738  tsmssplit  17828  xrtgioo  18306  reconnlem2  18326  iccpnfcnv  18436  iccpnfhmeo  18437  mbfss  18995  mbfmax  18998  itg2splitlem  19097  itg2split  19098  iblss2  19154  itgsplit  19184  limcdif  19220  ellimc2  19221  limcmpt  19227  limcres  19230  limccnp  19235  limccnp2  19236  limcco  19237  rollelem  19330  dvivthlem1  19349  dvne0  19352  lhop  19357  degltlem1  19452  ply1rem  19543  fta1glem2  19546  plypf1  19588  plyaddlem1  19589  plymullem1  19590  plycj  19652  ofmulrt  19656  taylfval  19732  abelthlem2  19802  abelthlem3  19803  reasinsin  20186  scvxcvx  20274  ppinprm  20384  chtnprm  20386  dchrfi  20488  lgsdir2  20561  shunssi  21939  atomli  22954  atoml2i  22955  fzsplit3  23023  subfacp1lem4  23118  subfacp1lem5  23119  kur14lem7  23147  vdgrun  23297  dftrpred3g  23637  wfrlem14  23670  wfrlem15  23671  elsymdif  23775  brcup  23885  domrngref  24458  basexre  24921  intvconlem1  25102  vtarsuelt  25294  fnckle  25444  pfsubkl  25446  pgapspf2  25452  refssfne  25693  eqfnun  25786  smprngopr  26076  lzunuz  26246  jm2.23  26488  unxpwdom3  26655  hbtlem5  26731  fnchoice  27099  undif3VD  27926  bnj1138  28087  bnj1137  28292  lubunNEW  28430  elpadd  29255  paddval0  29266  hdmaplem4  31231  mapdh9a  31247
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-un 3158
  Copyright terms: Public domain W3C validator