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

Theorem eluni2 3847
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 1576 . 2  |-  ( E. x ( A  e.  x  /\  x  e.  B )  <->  E. x
( x  e.  B  /\  A  e.  x
) )
2 eluni 3846 . 2  |-  ( A  e.  U. B  <->  E. x
( A  e.  x  /\  x  e.  B
) )
3 df-rex 2562 . 2  |-  ( E. x  e.  B  A  e.  x  <->  E. x ( x  e.  B  /\  A  e.  x ) )
41, 2, 33bitr4i 268 1  |-  ( A  e.  U. B  <->  E. x  e.  B  A  e.  x )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   E.wex 1531    e. wcel 1696   E.wrex 2557   U.cuni 3843
This theorem is referenced by:  uni0b  3868  intssuni  3900  iuncom4  3928  inuni  4189  ssorduni  4593  unon  4638  limuni3  4659  cnvuni  4882  chfnrn  5652  onfununi  6374  oarec  6576  fissuni  7176  finsschain  7178  r1sdom  7462  rankuni2b  7541  cflm  7892  coflim  7903  axdc3lem2  8093  fpwwe2lem12  8279  uniwun  8378  tskr1om2  8406  tskuni  8421  axgroth3  8469  inaprc  8474  tskmval  8477  tskmcl  8479  suplem1pr  8692  lbsextlem2  15928  lbsextlem3  15929  isbasis3g  16703  eltg2b  16713  unitg  16721  tgcl  16723  ppttop  16760  epttop  16762  tgcmp  17144  1stckgenlem  17264  txuni2  17276  txcmplem1  17351  tgqtop  17419  filuni  17596  alexsubALTlem4  17760  ptcmplem3  17764  ptcmplem4  17765  icccmplem1  18343  icccmplem3  18345  cnheibor  18469  bndth  18472  lebnumlem1  18475  bcthlem4  18765  ovolicc2lem5  18896  dyadmbllem  18970  itg2gt0  19131  rexunirn  23156  unipreima  23224  cvmsss2  23820  cvmseu  23822  untuni  24070  dfon2lem3  24212  dfon2lem7  24216  dfon2lem8  24217  brbigcup  24509  uninqs  25142  locfincmp  26407  comppfsc  26410  neibastop1  26411  neibastop2lem  26412  cover2  26461  heiborlem9  26646  unichnidl  26759  prtlem16  26840  prter2  26852  prter3  26853  bnj1379  29179
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562  df-v 2803  df-uni 3844
  Copyright terms: Public domain W3C validator