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

Theorem elun 3081
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 2563 . 2  |-  ( A  e.  ( B  u.  C )  ->  A  e.  _V )
2 elex 2563 . . 3  |-  ( A  e.  B  ->  A  e.  _V )
3 elex 2563 . . 3  |-  ( A  e.  C  ->  A  e.  _V )
42, 3jaoi 636 . 2  |-  ( ( A  e.  B  \/  A  e.  C )  ->  A  e.  _V )
5 eleq1 2100 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
6 eleq1 2100 . . . 4  |-  ( x  =  A  ->  (
x  e.  C  <->  A  e.  C ) )
75, 6orbi12d 707 . . 3  |-  ( x  =  A  ->  (
( x  e.  B  \/  x  e.  C
)  <->  ( A  e.  B  \/  A  e.  C ) ) )
8 df-un 2919 . . 3  |-  ( B  u.  C )  =  { x  |  ( x  e.  B  \/  x  e.  C ) }
97, 8elab2g 2686 . 2  |-  ( A  e.  _V  ->  ( A  e.  ( B  u.  C )  <->  ( A  e.  B  \/  A  e.  C ) ) )
101, 4, 9pm5.21nii 620 1  |-  ( A  e.  ( B  u.  C )  <->  ( A  e.  B  \/  A  e.  C ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 98    \/ wo 629    = wceq 1243    e. wcel 1393   _Vcvv 2554    u. cun 2912
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-v 2556  df-un 2919
This theorem is referenced by:  uneqri  3082  uncom  3084  uneq1  3087  unass  3097  ssun1  3103  unss1  3109  ssequn1  3110  unss  3114  rexun  3120  ralunb  3121  unssdif  3169  unssin  3173  inssun  3174  indi  3181  undi  3182  difundi  3186  difindiss  3188  undif3ss  3195  symdifxor  3200  rabun2  3213  reuun2  3217  undif4  3281  ssundifim  3303  dfpr2  3391  eltpg  3413  pwprss  3573  pwtpss  3574  uniun  3596  intun  3643  iunun  3731  iunxun  3732  iinuniss  3734  brun  3807  pwunss  4017  elsuci  4127  elsucg  4128  elsuc2g  4129  ordsucim  4213  sucprcreg  4258  opthprc  4369  xpundi  4374  xpundir  4375  funun  4922  mptun  5007  unpreima  5270  reldmtpos  5846  dftpos4  5856  tpostpos  5857  elnn0  8146  un0addcl  8178  un0mulcl  8179  ltxr  8653  elxr  8654  fzsplit2  8872  elfzp1  8892  uzsplit  8912  elfzp12  8919  fzosplit  8991  fzouzsplit  8993  elfzonlteqm1  9024  fzosplitsni  9049  bj-nntrans  9940  bj-nnelirr  9942
  Copyright terms: Public domain W3C validator