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

Theorem elun 3187
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 2671 . 2  |-  ( A  e.  ( B  u.  C )  ->  A  e.  _V )
2 elex 2671 . . 3  |-  ( A  e.  B  ->  A  e.  _V )
3 elex 2671 . . 3  |-  ( A  e.  C  ->  A  e.  _V )
42, 3jaoi 690 . 2  |-  ( ( A  e.  B  \/  A  e.  C )  ->  A  e.  _V )
5 eleq1 2180 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
6 eleq1 2180 . . . 4  |-  ( x  =  A  ->  (
x  e.  C  <->  A  e.  C ) )
75, 6orbi12d 767 . . 3  |-  ( x  =  A  ->  (
( x  e.  B  \/  x  e.  C
)  <->  ( A  e.  B  \/  A  e.  C ) ) )
8 df-un 3045 . . 3  |-  ( B  u.  C )  =  { x  |  ( x  e.  B  \/  x  e.  C ) }
97, 8elab2g 2804 . 2  |-  ( A  e.  _V  ->  ( A  e.  ( B  u.  C )  <->  ( A  e.  B  \/  A  e.  C ) ) )
101, 4, 9pm5.21nii 678 1  |-  ( A  e.  ( B  u.  C )  <->  ( A  e.  B  \/  A  e.  C ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 104    \/ wo 682    = wceq 1316    e. wcel 1465   _Vcvv 2660    u. cun 3039
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 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-v 2662  df-un 3045
This theorem is referenced by:  uneqri  3188  uncom  3190  uneq1  3193  unass  3203  ssun1  3209  unss1  3215  ssequn1  3216  unss  3220  rexun  3226  ralunb  3227  unssdif  3281  unssin  3285  inssun  3286  indi  3293  undi  3294  difundi  3298  difindiss  3300  undif3ss  3307  symdifxor  3312  rabun2  3325  reuun2  3329  undif4  3395  ssundifim  3416  dcun  3443  dfpr2  3516  eltpg  3539  pwprss  3702  pwtpss  3703  uniun  3725  intun  3772  iunun  3861  iunxun  3862  iinuniss  3865  brun  3949  undifexmid  4087  exmidundif  4099  exmidundifim  4100  pwunss  4175  elsuci  4295  elsucg  4296  elsuc2g  4297  ordsucim  4386  sucprcreg  4434  opthprc  4560  xpundi  4565  xpundir  4566  funun  5137  mptun  5224  unpreima  5513  reldmtpos  6118  dftpos4  6128  tpostpos  6129  onunsnss  6773  unfidisj  6778  undifdcss  6779  fidcenumlemrks  6809  djulclb  6908  eldju  6921  eldju2ndl  6925  eldju2ndr  6926  ctssdccl  6964  elnn0  8937  un0addcl  8968  un0mulcl  8969  elxnn0  9000  ltxr  9517  elxr  9518  fzsplit2  9785  elfzp1  9807  uzsplit  9827  elfzp12  9834  fz01or  9846  fzosplit  9909  fzouzsplit  9911  elfzonlteqm1  9942  fzosplitsni  9967  hashinfuni  10478  hashennnuni  10480  hashunlem  10505  zfz1isolemiso  10537  summodclem3  11104  fsumsplit  11131  fsumsplitsn  11134  sumsplitdc  11156  reopnap  12618  djulclALT  12904  djurclALT  12905  bj-nntrans  13045  bj-nnelirr  13047  exmid1stab  13091
  Copyright terms: Public domain W3C validator