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

Theorem eluni2 3831
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 1573 . 2  |-  ( E. x ( A  e.  x  /\  x  e.  B )  <->  E. x
( x  e.  B  /\  A  e.  x
) )
2 eluni 3830 . 2  |-  ( A  e.  U. B  <->  E. x
( A  e.  x  /\  x  e.  B
) )
3 df-rex 2549 . 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 1528    e. wcel 1684   E.wrex 2544   U.cuni 3827
This theorem is referenced by:  uni0b  3852  intssuni  3884  iuncom4  3912  inuni  4173  ssorduni  4577  unon  4622  limuni3  4643  cnvuni  4866  chfnrn  5636  onfununi  6358  oarec  6560  fissuni  7160  finsschain  7162  r1sdom  7446  rankuni2b  7525  cflm  7876  coflim  7887  axdc3lem2  8077  fpwwe2lem12  8263  uniwun  8362  tskr1om2  8390  tskuni  8405  axgroth3  8453  inaprc  8458  tskmval  8461  tskmcl  8463  suplem1pr  8676  lbsextlem2  15912  lbsextlem3  15913  isbasis3g  16687  eltg2b  16697  unitg  16705  tgcl  16707  ppttop  16744  epttop  16746  tgcmp  17128  1stckgenlem  17248  txuni2  17260  txcmplem1  17335  tgqtop  17403  filuni  17580  alexsubALTlem4  17744  ptcmplem3  17748  ptcmplem4  17749  icccmplem1  18327  icccmplem3  18329  cnheibor  18453  bndth  18456  lebnumlem1  18459  bcthlem4  18749  ovolicc2lem5  18880  dyadmbllem  18954  itg2gt0  19115  rexunirn  23140  unipreima  23209  cvmsss2  23805  cvmseu  23807  untuni  24055  dfon2lem3  24141  dfon2lem7  24145  dfon2lem8  24146  brbigcup  24438  uninqs  25039  locfincmp  26304  comppfsc  26307  neibastop1  26308  neibastop2lem  26309  cover2  26358  heiborlem9  26543  unichnidl  26656  prtlem16  26737  prter2  26749  prter3  26750  bnj1379  28863
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-v 2790  df-uni 3828
  Copyright terms: Public domain W3C validator