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

Theorem eluni2 4092
Description: Membership in class union. Restricted quantifier version. (Contributed by NM, 31-Aug-1999.)
Assertion
Ref Expression
eluni2  |-  ( A  e.  U. B  <->  E. x  e.  B  A  e.  x )
Distinct variable groups:    x, A    x, B

Proof of Theorem eluni2
StepHypRef Expression
1 exancom 1643 . 2  |-  ( E. x ( A  e.  x  /\  x  e.  B )  <->  E. x
( x  e.  B  /\  A  e.  x
) )
2 eluni 4091 . 2  |-  ( A  e.  U. B  <->  E. x
( A  e.  x  /\  x  e.  B
) )
3 df-rex 2719 . 2  |-  ( E. x  e.  B  A  e.  x  <->  E. x ( x  e.  B  /\  A  e.  x ) )
41, 2, 33bitr4i 277 1  |-  ( A  e.  U. B  <->  E. x  e.  B  A  e.  x )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369   E.wex 1591    e. wcel 1761   E.wrex 2714   U.cuni 4088
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rex 2719  df-v 2972  df-uni 4089
This theorem is referenced by:  uni0b  4113  intssuni  4147  iuncom4  4175  inuni  4451  cnvuni  5022  chfnrn  5811  ssorduni  6396  unon  6441  limuni3  6462  onfununi  6798  oarec  6997  uniinqs  7176  fissuni  7612  finsschain  7614  r1sdom  7977  rankuni2b  8056  cflm  8415  coflim  8426  axdc3lem2  8616  fpwwe2lem12  8804  uniwun  8903  tskr1om2  8931  tskuni  8946  axgroth3  8994  inaprc  8999  tskmval  9002  tskmcl  9004  suplem1pr  9217  lbsextlem2  17218  lbsextlem3  17219  isbasis3g  18513  eltg2b  18523  unitg  18531  tgcl  18533  ppttop  18570  epttop  18572  neiptoptop  18694  tgcmp  18963  1stckgenlem  19085  txuni2  19097  txcmplem1  19173  tgqtop  19244  filuni  19417  alexsubALTlem4  19581  ptcmplem3  19585  ptcmplem4  19586  utoptop  19768  icccmplem1  20358  icccmplem3  20360  cnheibor  20486  bndth  20489  lebnumlem1  20492  bcthlem4  20797  ovolicc2lem5  20963  dyadmbllem  21038  itg2gt0  21197  rexunirn  25810  unipreima  25896  ddemeas  26588  dya2iocuni  26634  cvmsss2  27093  cvmseu  27095  untuni  27289  dfon2lem3  27527  dfon2lem7  27531  dfon2lem8  27532  brbigcup  27858  heicant  28351  mblfinlem1  28353  locfincmp  28501  comppfsc  28504  neibastop1  28505  neibastop2lem  28506  cover2  28532  heiborlem9  28643  unichnidl  28756  prtlem16  28939  prter2  28951  prter3  28952  bnj1379  31658
  Copyright terms: Public domain W3C validator