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

Theorem eluni 3707
Description: Membership in class union. (Contributed by NM, 22-May-1994.)
Assertion
Ref Expression
eluni  |-  ( A  e.  U. B  <->  E. x
( A  e.  x  /\  x  e.  B
) )
Distinct variable groups:    x, A    x, B

Proof of Theorem eluni
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 elex 2669 . 2  |-  ( A  e.  U. B  ->  A  e.  _V )
2 elex 2669 . . . 4  |-  ( A  e.  x  ->  A  e.  _V )
32adantr 272 . . 3  |-  ( ( A  e.  x  /\  x  e.  B )  ->  A  e.  _V )
43exlimiv 1560 . 2  |-  ( E. x ( A  e.  x  /\  x  e.  B )  ->  A  e.  _V )
5 eleq1 2178 . . . . 5  |-  ( y  =  A  ->  (
y  e.  x  <->  A  e.  x ) )
65anbi1d 458 . . . 4  |-  ( y  =  A  ->  (
( y  e.  x  /\  x  e.  B
)  <->  ( A  e.  x  /\  x  e.  B ) ) )
76exbidv 1779 . . 3  |-  ( y  =  A  ->  ( E. x ( y  e.  x  /\  x  e.  B )  <->  E. x
( A  e.  x  /\  x  e.  B
) ) )
8 df-uni 3705 . . 3  |-  U. B  =  { y  |  E. x ( y  e.  x  /\  x  e.  B ) }
97, 8elab2g 2802 . 2  |-  ( A  e.  _V  ->  ( A  e.  U. B  <->  E. x
( A  e.  x  /\  x  e.  B
) ) )
101, 4, 9pm5.21nii 676 1  |-  ( A  e.  U. B  <->  E. x
( A  e.  x  /\  x  e.  B
) )
Colors of variables: wff set class
Syntax hints:    /\ wa 103    <-> wb 104    = wceq 1314   E.wex 1451    e. wcel 1463   _Vcvv 2658   U.cuni 3704
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-uni 3705
This theorem is referenced by:  eluni2  3708  elunii  3709  eluniab  3716  uniun  3723  uniin  3724  uniss  3725  unissb  3734  dftr2  3996  unidif0  4059  unipw  4107  uniex2  4326  uniuni  4340  limom  4495  dmuni  4717  fununi  5159  nfvres  5420  elunirn  5633  tfrlem7  6180  tfrexlem  6197  tfrcldm  6226  fiuni  6832  isbasis2g  12118  tgval2  12126  ntreq0  12207  bj-uniex2  12948
  Copyright terms: Public domain W3C validator