ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elun Unicode version

Theorem elun 3185
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 2669 . 2  |-  ( A  e.  ( B  u.  C )  ->  A  e.  _V )
2 elex 2669 . . 3  |-  ( A  e.  B  ->  A  e.  _V )
3 elex 2669 . . 3  |-  ( A  e.  C  ->  A  e.  _V )
42, 3jaoi 688 . 2  |-  ( ( A  e.  B  \/  A  e.  C )  ->  A  e.  _V )
5 eleq1 2178 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
6 eleq1 2178 . . . 4  |-  ( x  =  A  ->  (
x  e.  C  <->  A  e.  C ) )
75, 6orbi12d 765 . . 3  |-  ( x  =  A  ->  (
( x  e.  B  \/  x  e.  C
)  <->  ( A  e.  B  \/  A  e.  C ) ) )
8 df-un 3043 . . 3  |-  ( B  u.  C )  =  { x  |  ( x  e.  B  \/  x  e.  C ) }
97, 8elab2g 2802 . 2  |-  ( A  e.  _V  ->  ( A  e.  ( B  u.  C )  <->  ( A  e.  B  \/  A  e.  C ) ) )
101, 4, 9pm5.21nii 676 1  |-  ( A  e.  ( B  u.  C )  <->  ( A  e.  B  \/  A  e.  C ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 104    \/ wo 680    = wceq 1314    e. wcel 1463   _Vcvv 2658    u. cun 3037
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-v 2660  df-un 3043
This theorem is referenced by:  uneqri  3186  uncom  3188  uneq1  3191  unass  3201  ssun1  3207  unss1  3213  ssequn1  3214  unss  3218  rexun  3224  ralunb  3225  unssdif  3279  unssin  3283  inssun  3284  indi  3291  undi  3292  difundi  3296  difindiss  3298  undif3ss  3305  symdifxor  3310  rabun2  3323  reuun2  3327  undif4  3393  ssundifim  3414  dcun  3441  dfpr2  3514  eltpg  3537  pwprss  3700  pwtpss  3701  uniun  3723  intun  3770  iunun  3859  iunxun  3860  iinuniss  3863  brun  3947  undifexmid  4085  exmidundif  4097  exmidundifim  4098  pwunss  4173  elsuci  4293  elsucg  4294  elsuc2g  4295  ordsucim  4384  sucprcreg  4432  opthprc  4558  xpundi  4563  xpundir  4564  funun  5135  mptun  5222  unpreima  5511  reldmtpos  6116  dftpos4  6126  tpostpos  6127  onunsnss  6771  unfidisj  6776  undifdcss  6777  fidcenumlemrks  6807  djulclb  6906  eldju  6919  eldju2ndl  6923  eldju2ndr  6924  ctssdccl  6962  elnn0  8930  un0addcl  8961  un0mulcl  8962  elxnn0  8993  ltxr  9502  elxr  9503  fzsplit2  9770  elfzp1  9792  uzsplit  9812  elfzp12  9819  fz01or  9831  fzosplit  9894  fzouzsplit  9896  elfzonlteqm1  9927  fzosplitsni  9952  hashinfuni  10463  hashennnuni  10465  hashunlem  10490  zfz1isolemiso  10522  summodclem3  11089  fsumsplit  11116  fsumsplitsn  11119  sumsplitdc  11141  reopnap  12602  djulclALT  12819  djurclALT  12820  bj-nntrans  12960  bj-nnelirr  12962  exmid1stab  13006
  Copyright terms: Public domain W3C validator